avewright/proofwiki-math huggingface dataset:
Theorem: Substitution Property of Equality

Let $\map F z$ be an expression of the variable $z$.
Then:
:$\forall x, y: x = y \implies \map F x = \map F y$.

Proof:
{{BeginTableau|\forall x, y: x {{=}} y \implies \map F x {{=}} \map F y}}
{{TableauLine|n = 1
             |pool = 1
             |f = x = y
             |rlnk = Rule of Assumption
             |rtxt = Assumption
}}
{{TableauLine|n = 2
             |pool = 1
             |f = \map F x = \map F x \iff \map F x = \map F y
             |rlnk = Axiom:Leibniz's Law
             |rtxt = Leibniz's Law
             |dep = 1
             |c = $\map P a := \map F x = \map F a$
}}
{{TableauLine|n = 3
             |pool = 1
             |f = \map F x = \map F x \implies \map F x = \map F y
             |rlnk = Biconditional Elimination
             |rtxt = Biconditional Elimination
             |dep = 2
}}
{{TheoremIntro|4|\forall a: a {{=}} a|Equality is Reflexive}}
{{TableauLine|n = 5
             |f = \map F x = \map F y
             |rlnk = Universal Instantiation
             |rtxt = Universal Instantiation
             |dep = 4
}}
{{TableauLine|n = 6
             |pool = 1
             |f = \map F x = \map F y
             |rlnk = Modus Ponendo Ponens
             |rtxt = Modus Ponendo Ponens
             |dep = 3, 5
}}
{{TableauLine|n = 7
             |f = x = y \implies \map F x = \map F y
             |rlnk = Rule of Implication
             |rtxt = Rule of Implication
             |dep = 1-6
}}
{{TableauLine|n = 8
             |f = \forall x, y: x = y \implies \map F x = \map F y
             |rlnk = Universal Generalization
             |rtxt = Universal Generalization
             |dep = 7
}}
{{EndTableau}}
Category:Equality
jmr3g34cyylird3mh4354vnn7yepxnt
Theorem: Multiplication of Natural Numbers is Provable

Let $x, y \in \N$ be natural numbers.
Then there exists a formal proof of:
:$\sqbrk x \times \sqbrk y = \sqbrk {x \times y}$
in minimal arithmetic, where $\sqbrk a$ is the unary representation of $a$.

Proof:
By Unary Representation of Natural Number, let $\sqbrk a$ denote the term $\map s {\dots \map s 0}$, where there are $a$ applications of the successor mapping to the constant $0$.
Proceed by induction on $y$.
Theorem: Subspace of Metrizable Space is Metrizable Space

Let $\struct {X, \tau}$ be a metrizable topological space.
Let $\struct {Y, \tau_Y}$ be a subspace of $\struct{X, \tau}$.
Then:
:$\struct {Y, \tau_Y}$ is a metrizable topological space

Proof:
By definition of metrizable topological space:
:there exists a metric $d$ on $X$ such that the topology induced by $d$ is $\tau$
From Metric Subspace Induces Subspace Topology:
:$\tau_Y$ is the topology induced by the subspace metric $d_Y$ on $Y$
From Subspace of Metric Space is Metric Space:
:$\struct {Y, d_Y}$ is a metric space
By definition, $\struct {Y, \tau_Y}$ is a metrizable topological space.
{{qed}}
Category:Metrizable Spaces
Category:Topological Subspaces
l14ghmcda10k7bnggxwmn9g3tyfiap1
Theorem: Electric Field Strength from Assemblage of Point Charges

Let $q_1, q_2, \ldots, q_n$ be point charges.
Let $\mathbf r_1, \mathbf r_2, \ldots, \mathbf r_n$ be the position vectors of $q_1, q_2, \ldots, q_n$ respectively.
Let $\map {\mathbf E} {\mathbf r}$ be the electric field strength at a point $P$ whose position vector is $\mathbf r$.
Then:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \epsilon_0} \sum_i \dfrac {q_i} {\size {\mathbf r - \mathbf r_i}^3} \paren {\mathbf r - \mathbf r_i}$
where $\varepsilon_0$ denotes the vacuum permittivity.

Proof:
Let $q$ be a test charge in the vicinity of $q_1, q_2, \ldots, q_n$ at $\map P {\mathbf r}$.
For all $i$ in $\set {1, 2, \ldots, n}$, let $\mathbf F_i$ denote the force exerted on $q$ by $q_i$.
Let $\mathbf F$ be the force exerted on $q$ by the combined action of $q_1, q_2, \ldots, q_n$.
We have:
{{begin-eqn}}
{{eqn | l = \mathbf F
      | r = \dfrac 1 {4 \pi \varepsilon_0} \sum_i \dfrac {q q_i} {\size {\mathbf r - \mathbf r_i}^3} \paren {\mathbf r - \mathbf r_i}
      | c = Total Force on Point Charge from Multiple Point Charges
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\mathbf F} q
      | r = \dfrac 1 {4 \pi \varepsilon_0} \sum_i \dfrac {q_j} {\size {\mathbf r - \mathbf r_i}^3} \paren {\mathbf r - \mathbf r_i}
      | c = dividing both sides by $q$ which is constant
}}
{{eqn | ll= \leadsto
      | l = \map {\mathbf E} {\mathbf r}
      | r = \dfrac 1 {4 \pi \varepsilon_0} \sum_i \dfrac {q_j} {\size {\mathbf r - \mathbf r_i}^3} \paren {\mathbf r - \mathbf r_i}
      | c = {{Defof|Electric Field Strength}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Ampère's Force Law

Let $s_1$ and $s_2$ be wires in a vacuum carrying steady currents $I_1$ and $I_2$.
Then the force on $s_1$ due to the magnetic field generated by $s_2$ is given by:
:$\ds \mathbf F_1 \propto I_1 I_2 \oint_{s_1} \oint_{s_2} \rd \mathbf l_1 \times \paren {\dfrac {\d \mathbf l_2 \times \paren {\mathbf r_1 - \mathbf r_2} } {\size {\mathbf r_1 - \mathbf r_2}^3} }$
where:
:$\d \mathbf l_1$ and $\d \mathbf l_2$ are infinitesimal vectors associated with $s_1$ and $s_2$ respectively
:$\mathbf r_1$ and $\mathbf r_2$ are the position vectors of $\d \mathbf l_1$ and $\d \mathbf l_2$, respectively.

Proof:
Let $\mathbf B_2$ be the magnetic field produced by $I_2$.
The magnetic force felt by $s_1$ is given by
{{begin-eqn}}
{{eqn | l = \mathbf F_1
      | r = \oint_{s_1} \d \mathbf F_1
}}
{{eqn | r = \oint_{s_1} I_1 \d \mathbf l_1 \times \mathbf B_2
      | c = Magnetic Force on Conductor carrying Steady Current
}}
{{eqn | r = \oint_{s_1} I_1 \d \mathbf l_1 \times \frac {\mu_0 I_2} {4 \pi} \oint_{s_2} \frac {\d \mathbf l_2 \times \paren {\mathbf r - \mathbf r'} } {\size {\mathbf r - \mathbf r'}^3}
      | c = Biot-Savart Law
}}
{{eqn | r = \frac {\mu_0 I_1 I_2} {4 \pi} \oint_{s_1} \oint_{s_2} \d \mathbf l_1 \times \frac {\d \mathbf l_2 \times \paren {\mathbf r - \mathbf r'} } {\size {\mathbf r - \mathbf r'}^3}
      | c = Linear Combination of Integrals
}}
{{end-eqn}}
{{qed}}
Theorem: Equality of Terms of Natural Numbers is Provable

Let $A$ and $B$ be terms in the language of arithmetic containing no variables.
Let $A = B$ when interpreted over the natural numbers $\N$.
Then there is a formal proof of $A = B$ in minimal arithmetic.

Proof:
Let $k = A = B$.
By Unary Representation of Natural Number, there is a term $\sqbrk k$ consisting of only the successor mapping and the constant $0$ such that $\sqbrk k = k$.
We want to show that $A = \sqbrk k$ has a formal proof.
Proceed by induction on the structure of the term $A$.
By definition, a term consists of variables and function applications.
By assumption, $A$ contains no variables.
Therefore, $A$ consists of only function applications defined by the language.
Theorem: Value of Vacuum Permeability

The value of the '''vacuum permeability''' is calculated as:
:$\mu_0 = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6} \, \mathrm H \, \mathrm m^{-1}$ (henries per metre)
with a relative uncertainty of $1 \cdotp 5 \times 10^{-10}$.

Proof:
The '''vacuum permeability''' is the physical constant denoted $\mu_0$ defined as:
:$\mu_0:= \dfrac {2 \alpha h} {e^2 c}$
where:
:$e$ is the elementary charge
:$\alpha$ is the fine-structure constant
:$h$ is Planck's constant
:$c$ is the speed of light defined in $\mathrm m \, \mathrm s^{-1}$
$e$ is defined precisely as:
:$e = 1 \cdotp 60217 \, 6634 \times 10^{-19} \, \mathrm C$ (coulombs)
$\alpha$ has the value determined experimentally as:
:$\alpha \approx 0 \cdotp 00729 \, 73525 \, 693 (11)$
$h$ is defined precisely as:
:$h = 6 \cdotp 62607 \, 015 \times 10^{-34} \, \mathrm J \, \mathrm s$ (joule seconds)
$c$ is defined precisely as:
:$c = 299 \, 792 \, 458 \, \mathrm m \, \mathrm s^{-1}$ (metres per second)
Hence $\mu_0$ can be calculated as:
{{begin-eqn}}
{{eqn | l = \mu_0
      | r = \dfrac {2 \alpha h} {e^2 c}
      | rr= \dfrac {\mathrm J \, s} {\mathrm C^2 \times \mathrm m \, \mathrm s^{-1} }
      | c = 
}}
{{eqn | r = \dfrac {0 \cdotp 00729 \, 73525 \, 693 (11) \times 6 \cdotp 62607 \, 015 \times 10^{-34} } {\paren {1 \cdotp 60217 \, 6634 \times 10^{-19} }^2 \times 299 \, 792 \, 458}
      | rr= \dfrac {\paren {\frac {\mathrm {kg} \times \mathrm m^2} {\mathrm s} } } {\paren {\mathrm A \, \mathrm s}^2 \times \mathrm s \times \mathrm m \, \mathrm s^{-1} }
      | c = Base Units of Coulomb, Base Units of Joule
}}
{{eqn | r = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6}
      | rr= \dfrac {\mathrm {kg} \times \mathrm m} {\mathrm A^2 \times \mathrm s^4}
      | c = 
}}
{{eqn | r = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6}
      | rr= \dfrac {\mathrm H} {\mathrm m}
      | c = Base Units of Henry
}}
{{end-eqn}}
{{qed}}
Theorem: Value of Vacuum Permeability

The value of the '''vacuum permeability''' is calculated as:
:$\mu_0 = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6} \, \mathrm H \, \mathrm m^{-1}$ (henries per metre)
with a relative uncertainty of $1 \cdotp 5 \times 10^{-10}$.

Proof:
The '''vacuum permeability''' is the physical constant denoted $\mu_0$ defined as:
:$\mu_0 := \dfrac 1 {\varepsilon_0c^2}$
where:
:$\varepsilon_0$ is the vacuum permittivity defined in $\mathrm F \, \mathrm m^{-1}$ (farads per metre)
:$c$ is the speed of light defined in $\mathrm m \, \mathrm s^{-1}$
$\varepsilon_0$ has the value determined as:
:$\varepsilon_0 \approx 8 \cdotp 85418 \, 78128 (13) \times 10^{-12} \, \mathrm F \, \mathrm m^{-1}$
$c$ is defined precisely as:
:$c = 299 \, 792 \, 458 \, \mathrm m \, \mathrm s^{-1}$
Hence $\mu_0$ can be calculated as:
{{begin-eqn}}
{{eqn | l = \mu_0
      | r = \dfrac 1 {\varepsilon_0 c^2}
      | rr= \dfrac 1 {\mathrm F \, \mathrm m^{-1} \times \paren {\mathrm m \, \mathrm s^{-1} }^2}
      | c = 
}}
{{eqn | r = \dfrac 1 {8 \cdotp 85418 \, 78128 (13) \times 10^{-12} \times \paren {299 \, 792 \, 458}^2}
      | rr= \dfrac 1 {\frac {\mathrm s^4 \, \mathrm A^2} {\mathrm {kg}^{-1} \, \mathrm m^{-3} } \times \paren {\mathrm m \, \mathrm s^{-1} }^2}
      | c = Base Units of Farad
}}
{{eqn | r = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6}
      | rr= \dfrac {\mathrm {kg} \times \mathrm m} {\mathrm A^2 \times \mathrm s^2}
      | c = 
}}
{{eqn | r = 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6}
      | rr= \dfrac {\mathrm H} {\mathrm m}
      | c = Base Units of Henry
}}
{{end-eqn}}
{{qed}}
Theorem: Mean Ergodic Theorem (Hilbert Space)

Let $\GF \in \set {\R, \C}$.
Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\mathbb F$.
Let $U : \HH \to \HH$ be a bounded linear operator such that:
:$\forall f \in \HH : \norm {\map U f} \le \norm f$
Then for each $f \in \HH$:
:$\ds \lim_{N \mathop \to \infty} \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} f = \map P f$
where:
:$U^n$ denotes the $n$ times composition of $U$
:$I := \set {f \in \HH : \map U f = f}$
:$P : \HH \to I$ denotes the orthogonal projection on $I$

Proof:
Note that $I$ is a closed linear subspace of $\HH$, since $U$ is bounded.
Especially, $P : \HH \to I$ is well-defined.
Moreover, by Direct Sum of Subspace and Orthocomplement:
:$\HH = I \oplus I^\perp$
Let $f \in \HH$.
We can write:
:$ f = \map P f + f^\perp$
where $f^\perp \in I^\perp$.
Then we have:
{{begin-eqn}}
{{eqn | l = \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} f
      | r = \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} {\map P f} + \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} {f^\perp}
}}
{{eqn | r = \map P f + \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} {f^\perp}
      | c = as $\map P f \in I$
}}
{{end-eqn}}
Thus we need to show:
:$\ds \lim_{N \mathop \to \infty} \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U^n} {f^\perp} = 0$
Theorem: Lower Section of Natural Number is Provable

Let $x \in \N$ be a natural number.
Then the following WFF:
:$\forall y: y = 0 \lor y = \map s 0 \lor \dotso \lor y = \sqbrk {x - 1} \lor \neg \paren {y < \sqbrk x}$
is a theorem of minimal arithmetic.

Proof:
Proceed by induction on $x$.
Theorem: Ampère-Maxwell Law

Let $\mathbf B$ be a magnetic field due to a steady current $I$ flowing through a wire.
Then:
:$\ds \oint \mathbf B \cdot \rd \mathbf l = \mu_0 I$
where:
:the line integral is taken around a closed path that surrounds the wire
:$\d \mathbf l$ is an infinitesimal vector associated with the closed path
:$\mu_0$ denotes the vacuum permeability.
That is, the line integral of $\mathbf B$ through the area enclosed by the closed path is equal to $\mu_0 I$.

Proof:
Let $R$ be a simply connected region of space.
Let $\partial S$ be a simple closed contour within $R$.
Let $S$ be an open orientable surface bounded by $\partial S$.
Then:
{{begin-eqn}}
{{eqn | l = \oint_{\partial S} \mathbf B \cdot \rd \mathbf l
      | r = \iint_S \paren {\nabla \times \mathbf B} \cdot \mathbf n \rd S
      | c = Kelvin-Stokes Theorem
}}
{{eqn | r = \iint_S \paren {\mu_0 \mathbf J + \varepsilon_0 \frac {\partial \mathbf E} {\partial t} } \cdot \mathbf n \rd S
      | c = Ampère's Law with Maxwell's Addition
}}
{{eqn | r = \mu_0 \iint_S \mathbf J \cdot \mathbf n \rd S
      | c = Current is steady, so the electric field is not changing.
}}
{{eqn | r = \mu_0 I
      | c = {{Defof|Electric Current Density}}
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space

Let $T = \struct {X, \tau}$ be a $T_3$ space.
{{TFAE}}
:$(1): \quad T$ is paracompact
:$(2): \quad$ every open cover of $T$ has a locally finite refinement
:$(3): \quad$ every open cover of $T$ has a closed locally finite refinement
:$(4): \quad$ every open cover of $T$ is even
:$(5): \quad$ every open cover of $T$ has an open $\sigma$-discrete refinement
:$(6): \quad$ every open cover of $T$ has an open $\sigma$-locally finite refinement

Proof:
=== Statement $(1)$ implies Statement $(2)$ ===
{{:Characterization of Paracompactness in T3 Space/Statement 1 implies Statement 2}}{{qed|lemma}}
Theorem: Characterization of Paracompactness in T3 Space/Statement 1 implies Statement 2

Let $T = \struct{X, \tau}$ be a topological space.
If $T$ is paracompact then:
:every open cover of $T$ has a locally finite refinement

Proof:
Let $T$ be paracompact.
By definition of paracompact:
:every open cover of $S$ has an open refinement which is locally finite.
By definition of open refinement:
:every open refinement of a cover is a refinement of the cover.
It follows that:
:every open cover of $T$ has a locally finite refinement.
Theorem: Characterization of Paracompactness in T3 Space/Statement 2 implies Statement 3

Let $T = \struct{X, \tau}$ be a $T_3$ space.
If every open cover of $T$ has a locally finite refinement then:
:every open cover of $T$ has a closed locally finite refinement

Proof:
Let every open cover of $T$ have a locally finite refinement.
Let $\UU$ be an open cover of $T$.
Let $\VV = \set{V \in \tau : \exists U \in \UU : V^- \subseteq U}$ where $V^-$ denotes the closure of $V$ in $T$.
==== Lemma 1 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 1}}{{qed|lemma}}
By assumption:
:there exists a locally finite refinement $\AA$ of $\VV$.
Let:
:$\BB = \set{A^- : A \in \AA}$
From Closures of Elements of Locally Finite Set is Locally Finite:
:$\BB$ is locally finite
==== Lemma 2 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 2}}{{qed|lemma}}
==== Lemma 3 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 3}}{{qed|lemma}}
Since $\UU$ was an arbitrary open cover of $T$ it follows that:
:every open cover of $T$ has a closed locally finite refinement.
Theorem: Characterization of Paracompactness in T3 Space/Statement 3 implies Statement 4

Let $T = \struct{X, \tau}$ be a topological space.
If every open cover of $T$ has a closed locally finite refinement then:
:every open cover of $T$ is even

Proof:
This follows immediately from Open Cover with Closed Locally Finite Refinement is Even Cover.
Theorem: Characterization of Paracompactness in T3 Space/Statement 4 implies Statement 5

Let $T = \struct{X, \tau}$ be a topological space.
If every open cover of $T$ is even then:
:every open cover of $T$ has an open $\sigma$-discrete refinement

Proof:
Let every open cover of $T$ be even.
Let $\UU$ be an open cover of $T$.
==== Lemma 8 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 8}}{{qed|lemma}}
By definition of $\sigma$-discrete set of subsets:
:$\AA = \ds \bigcup_{n \in \N} \AA_n$ where $\AA_n$ is a discrete set of subsets for each $n \in \N$.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\tau_{X \times X}$ denote the product topology on $X \times X$.
Let $T \times T$ denote the product space $\struct {X \times X, \tau_{X \times X} }$. 
==== Lemma 9 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 9}}{{qed|lemma}}
From {{Lemma|Characterization of Paracompactness in T3 Space|9}}:
:$\forall n \in \N$ there exists a neighborhood $V_n$ of the diagonal $\Delta_X$ of $X \times X$ in $T \times T$:
::$\forall x \in X : \card {\set{A \in \AA_n : \map {V_n} x \cap V_n \sqbrk A \ne \O}} \le 1$
By definition of refinement:
:$\forall A \in \AA : \exists U_A \in U : A \subseteq U_A$
For each $n \in \N$, let:
:$\WW_n = \set{U_A \cap V_n \sqbrk A : A \in \AA_n}$
Let:
:$\WW = \ds \bigcup_{n \in \N} \WW_n$
==== Lemma 10 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 10}}{{qed|lemma}}
Since $\UU$ was arbitrary, then every open cover of $T$ has an open $\sigma$-discrete refinement
Theorem: Characterization of Paracompactness in T3 Space/Statement 5 implies Statement 6

Let $T = \struct{X, \tau}$ be a topological space.
If every open cover of $T$ has an open $\sigma$-discrete refinement then:
:every open cover of $T$ has an open $\sigma$-locally finite refinement

Proof:
Follows immediately from Sigma-Discrete Set of Subsets is Sigma-Locally Finite.
Theorem: Characterization of Paracompactness in T3 Space/Statement 6 implies Statement 2

Let $T = \struct{X, \tau}$ be a topological space.
If every open cover of $T$ has an open $\sigma$-locally finite refinement then:
:every open cover of $T$ has a locally finite refinement

Proof:
Let every open cover of $T$ have an open $\sigma$-locally finite refinement.
Let $\UU$ be an open cover of $T$.
Let $\VV$ be an open $\sigma$-locally finite refinement of $\UU$ {{Hypothesis}}.
From Sigma-Locally Finite Cover has Locally Finite Refinement:
:there exists a locally finite refinement $\AA$ of $\VV$
From Refinement of a Refinement is Refinement of Cover:
:$\AA$ is a locally finite refinement of $\UU$
Since $\UU$ was arbitrary, it follows that:
:every open cover of $T$ has a locally finite refinement
Theorem: Addition of Natural Numbers is Provable/General Form

Let $y \in \N$ be a natural number.
Let $s^a$ denote the application of the successor mapping $a$ times.
Let $\sqbrk a$ denote $\map {s^a} 0$.
Then there exists a formal proof of:
:$\forall x: x + \sqbrk y = \map {s^y} x$
in minimal arithmetic.

Proof:
Proceed by induction on $y$.
Theorem: Electric Field caused by Point Charge

Let $q$ be a point charge.
Let $\mathbf r_q$ be the position vector of $q$.
Let $\map {\mathbf E} {\mathbf r}$ be the electric field strength due to $q$ at a point $P$ whose position vector is $\mathbf r$.
Then:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {q \paren {\mathbf r - \mathbf r_q} } {\size {\mathbf r - \mathbf r_q}^3}$
where $\varepsilon_0$ denotes the vacuum permittivity.

Proof:
A specific application of Electric Field Strength from Assemblage of Point Charges for $1$ point charge.
{{qed}}
Theorem: Magnitude of Electric Field caused by Point Charge

Let $q$ be a point charge.
Let $\map {\mathbf E} {\mathbf r}$ be the electric field strength due to $q$ at a point $P$ whose position vector is $\mathbf r$.
The magnitude of the electric field strength due to $q$ at $P$ is given by:
Then:
:$\size {\map {\mathbf E} {\mathbf r} } = \dfrac {\size q} {4 \pi \epsilon_0 r^2}$
where:
:$r$ is the distance $P$ is from $q$
:$\varepsilon_0$ denotes the vacuum permittivity.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\mathbf E} {\mathbf r}
      | r = \dfrac 1 {4 \pi \epsilon_0} \dfrac {q \paren {\mathbf r - \mathbf r_q} } {\size {\mathbf r - \mathbf r_q}^3}
      | c = Electric Field caused by Point Charge
}}
{{eqn | ll= \leadsto
      | l = \size {\map {\mathbf E} {\mathbf r} }
      | r = \size {\dfrac 1 {4 \pi \epsilon_0} \dfrac {q \paren {\mathbf r - \mathbf r_q} } {\size {\mathbf r - \mathbf r_q}^3} }
      | c = 
}}
{{eqn | r = \dfrac {\size q} {4 \pi \epsilon_0} \size {\dfrac {\mathbf r - \mathbf r_q} {\size {\mathbf r - \mathbf r_q}^3} }
      | c = 
}}
{{eqn | r = \dfrac {\size q} {4 \pi \epsilon_0} \dfrac {\size {\mathbf r - \mathbf r_q} } {\size {\mathbf r - \mathbf r_q}^3}
      | c = 
}}
{{eqn | r = \dfrac {\size q} {4 \pi \epsilon_0} \dfrac 1 {\size {\mathbf r - \mathbf r_q}^2}
      | c = 
}}
{{eqn | r = \dfrac {\size q} {4 \pi \epsilon_0 r^2}
      | c = 
}}
{{end-eqn}}
The following diagram shows the points of equal magnitude of $\map {\mathbf E} {\mathbf r}$ as dotted circles:
:480px
{{qed}}
Theorem: Invertibility of Identity Transformation Plus Product of Two Continuous Linear Transformations

Let $\struct {X, \norm{, \cdot ,} }$ be the normed vector space.
Let $I : X \to X$ be the identity mapping.
Let $\map {CL} X := \map {CL} {X, X}$ be the continuous linear transformation space on $X$.
Suppose $I + A \circ B$ is invertible, where $\circ$ denotes the composition of mappings.
Then $I + B \circ A$ is invertible, with the inverse given by:
:$\paren {I + B \circ A}^{-1} = I - B \circ \paren {I + A \circ B}^{-1} \circ A$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {I + B \circ A} \circ \paren {I - B \circ \paren {I + A \circ B}^{-1} \circ A}
      | r = I - B \circ \paren {I + A \circ B}^{-1} \circ A + B \circ A - B \circ A \circ B \circ \paren {I + A \circ B}^{-1} \circ A
}}
{{eqn | r = I - B \circ \paren {I + A \circ B}^{-1} \circ A + B \circ A - B \circ \paren {I + A \circ B - I} \circ \paren {I + A \circ B}^{-1} \circ A
}}
{{eqn | r = I - B \circ \paren {I + A \circ B}^{-1} \circ A + B \circ A - B \circ \paren {I + A \circ B} \circ \paren {I + A \circ B}^{-1} \circ A + B \circ \paren {I + A \circ B}^{-1} \circ A
}}
{{eqn | r = I + B \circ A - B \circ A
}}
{{eqn | r = I
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {I - B \circ \paren {I + A \circ B}^{-1} \circ A} \circ \paren {I + B \circ A}
      | r = I + B \circ A - B \circ \paren {I + A \circ B}^{-1} \circ A - B \circ \paren {I + A \circ B}^{-1} \circ A \circ B \circ A
}}
{{eqn | r = I + B \circ A - B \circ \paren {I + A \circ B}^{-1} \circ A - B \circ \paren {I + A \circ B}^{-1} \circ \paren{I + A \circ B - I} \circ A
}}
{{eqn | r = I + B \circ A - B \circ \paren {I + A \circ B}^{-1} \circ A - B \circ \paren {I + A \circ B}^{-1} \circ \paren{I + A \circ B} \circ A +  B \circ \paren {I + A \circ B}^{-1} \circ A
}}
{{eqn | r = I + B \circ A - B \circ A
}}
{{eqn | r = I
}}
{{end-eqn}}
{{qed}}
Theorem: Direction of Electric Field caused by Point Charge

Let $q$ be a point charge.
Let $\map {\mathbf E} {\mathbf r}$ be the electric field strength due to $q$ at a point $P$ whose position vector is $\mathbf r$.
The direction of the electric field due to $q$ at $P$ is:
:for positive $q$, directly away from $q$ 
:for negative $q$, directly towards $q$.

Proof:
From Electric Field caused by Point Charge:
{{begin-eqn}}
{{eqn | q = 
      | l = \map {\mathbf E} {\mathbf r}
      | r = \dfrac 1 {4 \pi \epsilon_0} \dfrac {q \paren {\mathbf r - \mathbf r_q} } {\size {\mathbf r - \mathbf r_q}^3}
      | c = Electric Field caused by Point Charge
}}
{{end-eqn}}
By definition of vector subtraction, $\mathbf r - \mathbf r_q$ is the vector from $\mathbf r_q$ to $\mathbf r$.
Hence if $q$ is positive, the direction of $\map {\mathbf E} {\mathbf r}$ is towards $\mathbf r$, which is directly away from $q$.
Similarly, if $q$ is negative, the direction of $\map {\mathbf E} {\mathbf r}$ is $-\paren {\mathbf r - \mathbf r_q}$.
That is, the direction of $\map {\mathbf E} {\mathbf r}$ is $\mathbf r_q - \mathbf r$.
By definition of vector subtraction, $\mathbf r_q - \mathbf r$ is the vector from $\mathbf r$ to $\mathbf r_q$.
This is directly towards $q$.
The following diagram shows the lines of force of $\map {\mathbf E} {\mathbf r}$ as arrows, pointing away from $+q$:
:480px
The following diagram shows the lines of force of $\map {\mathbf E} {\mathbf r}$ as arrows, pointing towards $-q$:
:480px
{{qed}}