avewright/proofwiki-math huggingface dataset:
Theorem: Modulus of Complex Number equals its Distance from Origin

The modulus of a complex number equals its distance from the origin on the complex plane.

Proof:
Let $z = x + y i$ be a complex number and $O = 0 + 0 i$ be the origin on the complex plane.
We have its modulus:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = \cmod {x + y i}
      | c =
}}
{{eqn | r = \sqrt {x^2 + y^2}
      | c = {{Defof|Complex Modulus}}
}}
{{end-eqn}}
and its distance from the origin on the complex plane:
{{begin-eqn}}
{{eqn | l = \map d {z, O}
      | r = \map d {\tuple {x, y}, \tuple {0, 0} }
      | c =
}}
{{eqn | r = \sqrt {\paren {x - 0}^2 + \paren {y - 0}^2}
      | c = Distance Formula
}}
{{eqn | r = \sqrt {x^2 + y^2}
      | c =
}}
{{end-eqn}}
The two are seen to be equal.
{{qed}}
{{link wanted|There may be a more directly relevant link to the distance formula based on the fact (which we've proved somewhere) that the complex plane is a metric space, and that the distance formula is that metric.}}
Category:Complex Analysis
capgddz9khm99yqpv7bxzcbukstqw85
Theorem: Empty Set is Countable

The empty set $\O$ is countable.

Proof:
By Peano's Axioms, $\N_0 \sim \O$, where $\N_n$ denotes the initial segment of natural number $n$.
By definition, $\O$ is finite.
By definition, $\O$ is a countable set.
{{qed}}
Category:Set Theory
Category:Empty Set
Category:Countable Sets
ly0tg8512aadn5cgyxnqkjdd9niomfe
Theorem: Lindelöf's Lemma

Let $C$ be a set of open real sets.
Let $S \subseteq \R$ be a subset of the real numbers that is covered by $C$.
Then there exists a countable subset of $C$ that covers $S$.

Proof:
=== Lemma $1$ ===
{{:Lindelöf's Lemma/Lemma 1}}{{qed|lemma}}
We have that $S$ is covered by $C$.
This means that $S$ is a subset of $\ds \bigcup_{O \mathop \in C} O$.
From {{Lemma|Lindelöf's Lemma|1}}:
:$\ds \bigcup_{O \mathop \in D} O = \bigcup_{O \mathop \in C} O$
where $D$ is a countable subset of $C$.
Hence $S$ is also a subset of $\ds \bigcup_{O \mathop \in D} O$.
In other words, $S$ is covered by $D$.
That is, $S$ is covered by a countable subset of $C$.
Hence the result.
{{qed}}
{{Namedfor|Ernst Leonard Lindelöf|cat = Lindelöf}}
Category:Lindelöf's Lemma
Category:Real Analysis
4ndsb7hd9qm2g4w68q2agum01652ynp
Theorem: Area of Isosceles Triangle in terms of Sides

Let $\triangle ABC$ be an isosceles triangle whose apex is $A$.
Let $r$ be the length of a leg of $\triangle ABC$.
Let $b$ be the length of the base of $\triangle ABC$.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \dfrac b 4 \sqrt {4 r^2 - b^2}$

Proof:
:300px
Let $h$ be the height of $\triangle ABC$.
{{begin-eqn}}
{{eqn | l = \AA
      | r = \frac 1 2 b h
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | r = \frac b 2 \sqrt {r^2 - \paren {\frac b 2}^2}
      | c = Pythagoras's Theorem
}}
{{eqn | r = \frac b 2 \sqrt {\frac {4 r^2 - b^2} 4}
      | c = simplification
}}
{{eqn | r = \frac b 4 \sqrt {4 r^2 - b^2}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Category:Areas of Triangles
Category:Isosceles Triangles
grhsmqdwmbtq4dwcleuf6wv21o0j4jf
Theorem: Even Function Times Even Function is Even

Let $X \subset \R$ be a symmetric set of real numbers:
:$\forall x \in X: -x \in X$
Let $f, g: X \to \R$ be two even functions.
Let $f \cdot g$ denote the pointwise product of $f$ and $g$.
Then $\paren {f \cdot g}: X \to \R$ is also an even function.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \cdot g} } {-x}
      | r = \map f {-x} \cdot \map g {-x}
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{eqn | r = \map f x \cdot \map g x
      | c = {{Defof|Even Function}}
}}
{{eqn | r = \map {\paren {f \cdot g} } x
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{end-eqn}}
Thus, by definition, $\paren {f \cdot g}$ is an even function.
{{qed}}
Theorem: Odd Function Times Even Function is Odd

Let $X \subset \R$ be a symmetric set of real numbers:
:$\forall x \in X: -x \in X$
Let $f: X \to \R$ be an odd function.
Let $g: X \to \R$ be an even function.
Let $f \cdot g$ denote the pointwise product of $f$ and $g$.
Then $\paren {f \cdot g}: X \to \R$ is an odd function.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \cdot g} } {-x}
      | r = \map f {-x} \cdot \map g {-x}
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{eqn | r = \paren {-\map f x} \cdot \map g x
      | c = {{Defof|Odd Function}} and {{Defof|Even Function}}
}}
{{eqn | r = -\map f x \cdot \map g x
      | c = 
}}
{{eqn | r = -\map {\paren {f \cdot g} } x
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{end-eqn}}
Thus, by definition, $\paren {f \cdot g}$ is an odd function.
{{qed}}
Theorem: Odd Function Times Odd Function is Even

Let $S \subset \R$ be a symmetric set of real numbers:
:$\forall x \in S: -x \in X$
Let $f, g: X \to \R$ be two odd functions.
Let $f \cdot g$ denote the pointwise product of $f$ and $g$.
Then $\paren {f \cdot g}: S \to \R$ is an even function.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \cdot g} } {-x}
      | r = \map f {-x} \cdot \map g {-x}
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{eqn | r = \paren {-\map f x} \cdot \paren {-\map g x}
      | c = {{Defof|Odd Function}}
}}
{{eqn | r = \map f x \cdot \map g x
      | c = 
}}
{{eqn | r = \map {\paren {f \cdot g} } x
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{end-eqn}}
Thus, by definition, $\paren {f \cdot g}$ is an even function.
{{qed}}
Theorem: Mellin Transform of Exponential

Let $a$ be a complex constant and $e^t$ be the complex exponential.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {e^{-a t} } } s = a^{-s} \, \map \Gamma s$
where $\map \Re a, \map \Re s > 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {e^{-a t} } } s
      | r = \int_0^{\to +\infty} t^{s - 1} e^{-a t} \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_0^{\to +\infty} \paren {\dfrac t a}^{s - 1} e^{-a \paren {\frac t a} } \frac {\d t} a
      | c = Integration by Substitution, $t \mapsto \dfrac t a$, $\d t \mapsto \dfrac {\d t} a$
}}
{{eqn | r = a^{-s} \int_0^{\to +\infty} t^{s - 1} e^{-t} \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^{-s} \, \map \Gamma s
      | c = {{Defof|Integral Form of Gamma Function|Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mellin Transform of Dirac Delta Function

Let $c \in \R_{>0}$ be a (strictly) positive real number.
Let $\map {\delta_c} t$ be the Dirac delta function.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {\map {\delta_c} t} } s = c^{s - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {\map {\delta_c} t} } s
      | r = \int_0^{\to +\infty} t^{s - 1} \map {\delta_c} t \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_{c^-}^{c^+} t^{s - 1} \map {\delta_c} t \rd t
      | c = {{Defof|Dirac Delta Function}}: integrand is elsewhere zero
}}
{{eqn | r = \int_{c^-}^{c^+} c^{s - 1} \map {\delta_c} t \rd t
      | c = $t$ is constant in interval $\closedint {c^-} {c^+}$
}}
{{eqn | r = c^{s - 1} \int_{c^-}^{c^+} \map {\delta_c} t \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = c^{s - 1}
      | c = {{Defof|Dirac Delta Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mellin Transform of Heaviside Step Function

Let $c$ be a constant real number.
Let $\map {u_c} t$ be the Heaviside step function.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {\map {u_c} t} } s = -\dfrac {c^s} s$
for $c > 0, \map \Re s < 0$.

Proof:
=== Lemma ===
{{:Mellin Transform of Heaviside Step Function/Lemma}}
{{begin-eqn}}
{{eqn | l = \map {\MM \set {\map {u_c} t} } s
      | r = \int_0^{\to +\infty} t^{s - 1} \map {u_c} t \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_c^{\to +\infty} t^{s - 1} \rd t
      | c = {{Defof|Heaviside Step Function}}: integrand is elsewhere zero
}}
{{eqn | r = \intlimits {\dfrac {t^s} s} c {+\infty}
      | c = Primitive of Power
}}
{{eqn | r = 0 - \dfrac {c^s} s
      | c = By Lemma
}}
{{eqn | r = - \dfrac {c^s} s
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
Category:Heaviside Step Function
0hfqfdl9gd0j95c7rspdel3dzjqlbex
Theorem: Mellin Transform of Heaviside Step Function/Corollary

:$\map {\MM \set {\map u {c - t} } } s = \dfrac {c^s} s$
for $c > 0, \map \Re s > 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {\map u {c - t} } } s
      | r = \int_0^{\to +\infty} t^{s - 1} \map u {c - t} \rd t
      | c =  {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_0^c t^{s - 1} \rd t
      | c = {{Defof|Heaviside Step Function}}: integrand is elsewhere zero
}}
{{eqn | r = \bigintlimits {\dfrac {t^s} s} {t \mathop = 0} {t \mathop = c}
      | c = Primitive of Power
}}
{{eqn | r = \dfrac {c^s} s - 0
      | c = 
}}
{{eqn | r = \dfrac {c^s} s
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
Category:Heaviside Step Function
64ujeqpk8bhff2oiq6axncdews2ka4d
Theorem: Mellin Transform of Power Times Function

Let $t^n: \R \to \R$ be $t$ to the $n$th power for some $n \in \N_{\ge 0}$.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {t^n \map f t} } s = \map {\MM \set {\map f t} } {s + n}$
given that both transforms exist.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {t^n \map f t} } s
      | r = \int_0^{\to +\infty} t^{s - 1} t^n \map f t \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_0^{\to +\infty} t^{\paren {s + n} - 1} \map f t \rd t
      | c = Exponent Combination Laws
}}
{{eqn | r = \map {\MM \set {\map f t} } {s + n}
      | c = {{Defof|Mellin Transform}}
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
s1qt4pkrapk90rggpczcby46jreqllc
Theorem: Mellin Transform of Dirac Delta Function by Function

Let $f: \R \to \R$ be a function.
Let $c \in \R_{>0}$ be a positive constant real number.
Let $\map {\delta_c} t$ be the Dirac delta function.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {\map {\delta_c} t \map f t} } s = c^{s - 1} \map f c$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {\map {\delta_c} t \map f t} } s
      | r = \int_0^{\to +\infty} t^{s - 1} \map {\delta_c} t \map f t \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_{c^-}^{c^+} t^{s - 1} \map {\delta_c} t \map f t \rd t
      | c = {{Defof|Dirac Delta Function}}: integrand is elsewhere zero
}}
{{eqn | r = \int_{c^-}^{c^+} c^{s - 1} \map {\delta_c} t \map f c \rd t
      | c = $t$ is constant in interval $\closedint {c^-} {c^+}$
}}
{{eqn | r = c^{s - 1} \map f c \int_{c^-}^{c^+} \map {\delta_c} t \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = c^{s - 1} \map f c
      | c = {{Defof|Dirac Delta Function}}
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
Category:Dirac Delta Function
0j0hbf1ng1ujrci6xo223ejszjqlen1
Theorem: Unity of Ring is Idempotent

Let $\left({R, +, \circ}\right)$ be a ring with unity whose unity is $1_R$.
Then $1_R$ is an idempotent element of $R$ under the ring product $\circ$:
:$1_R \circ 1_R = 1_R$

Proof:
By definition of ring with unity, $\left({R, \circ}\right)$ is a monoid whose identity element is $1_R$.
From Identity Element is Idempotent (applied to $1_R$):
:$1_R \circ 1_R = 1_R$
which was to be proven. 
{{qed}}
Category:Ring Theory
sykxawsy95ekov7hb6d6eq70yxiv8oq
Theorem: Mellin Transform of Higher Order Exponential

Let $a$ be a complex constant.
Let $n$ be a natural number.
Let $e^t$ be the complex exponential of $t$.
Let $\MM$ be the Mellin transform.
Then:
:$\map {\MM \set {e^{-a t^n} } } s = \dfrac {a^{-s/n} } n \map \Gamma {\dfrac s n}$
where $\map \Gamma z$ is the Gamma function and $\map \Re a$, $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {e^{-a t^n} } } s
      | r = \int_0^{\to +\infty} t^{s-1} e^{-a t^n} \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \int_0^{\to +\infty} \paren {\dfrac t {\sqrt[n] a} }^{s - 1} e^{-a \paren {\dfrac t {\sqrt[n] {a} } }^n} \dfrac {\d t} {\sqrt[n] a}
      | c = Integration by Substitution, $t \mapsto \dfrac t {\sqrt[n] a}$, $\d t \mapsto \dfrac {\d t} {\sqrt[n] {a} }$
}}
{{eqn | r = a^{-s/n} \int_0^{\to +\infty} t^{s - 1} e^{-t^n} \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^{-s/n} \int_0^{\to +\infty} t^{\paren {s - 1}/n} e^{-t} \dfrac {t^{1 / n - 1} \rd t} n
      | c = Integration by Substitution, $t \mapsto \sqrt[n] t$, $\d t \mapsto \dfrac {t^{1 / n - 1} \rd t} n$
}}
{{eqn | r = \dfrac{a^{-s/n} } n \int_0^{\to +\infty} t^{s/n-1} e^{-t} \rd t
      | c = Primitive of Constant Multiple of Function, Exponent Combination Laws
}}
{{eqn | r = \dfrac{a^{-s/n} } n \map \Gamma {\dfrac s n}
      | c = {{Defof|Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
2yxilpge4j3790l4fznsrij0k2le73c
Theorem: Linear Combination of Mellin Transforms

Let $\MM$ be the Mellin transform.
Let $\map f t$, $g \left({t}\right)$ be functions such that $\MM \left\{ {\map f t}\right\} \left({s}\right)$ and $\MM \left\{ {\map f t}\right\} \left({s}\right)$ exist.
Let $\lambda \in \C$ be a constant.
Then:
:$\map {\MM \set {\lambda \map f t + \map g t} } s = \lambda \map {\MM \set {\map f t} } s + \map {\MM \set {\map g t} } s$
everywhere all the above expressions are defined.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\MM \set {\lambda \map f t + \map g t} } s
      | r = \int_0^{\to +\infty} t^{s - 1} \paren {\lambda \map f t + \map g t} \rd t
      | c = {{Defof|Mellin Transform}}
}}
{{eqn | r = \lambda \int_0^{\to +\infty} t^{s - 1} \map f t \rd t + \int_0^{\to +\infty} t^{s - 1} \map g t \rd t
      | c = distributing $t^{s - 1}$, Linear Combination of Complex Integrals
}}
{{eqn | r = \lambda \map {\MM \set {\map f t} } s + \map {\MM \set {\map g t} } s
      | c = {{Defof|Mellin Transform}}
}}
{{end-eqn}}
{{qed}}
Category:Mellin Transforms
h8r77zw1jaentasj0g0z4fknozpcoid
Theorem: Complex Numbers as External Direct Product

Let $\struct {\C_{\ne 0}, \times}$ be the group of non-zero complex numbers under multiplication.
Let $\struct {\R_{> 0}, \times}$ be the group of positive real numbers under multiplication.
Let $\struct {K, \times}$ be the circle group.
Then:
:$\struct {\C_{\ne 0}, \times} \cong \struct {\R_{> 0}, \times} \times \struct {K, \times}$
{{explain|It is apparent that the second $\times$ is Cartesian product, but this is not obvious.}}

Proof:
Let $\phi: \C_{\ne 0} \to \R_{> 0} \times K$ be the mapping:
:$\map \phi {r e^{i \theta} } = \paren {r, e^{i \theta} }$
$\forall \tuple {a, b} \in \R_{> 0} \times K:\exists z = a \times b \in \C$ such that:
:$\map \phi z = \tuple {a, b}$
by Complex Multiplication is Closed and $\R \subset \C$.
So $\phi$ is surjective.
To prove $\phi$ is injective, let $\map \phi {r_1 e^{i \theta_1} } = \map \phi {r_2 e^{i \theta_2} }$.
{{begin-eqn}}
{{eqn | l = \map \phi {r_1 e^{i \theta_1} }
      | r = \map \phi {r_2 e^{i \theta_2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {r_1, e^{i \theta_1} }
      | r = \paren {r_2, e^{i \theta_2} }
      | c = Definition of $\phi$
}}
{{eqn | ll= \leadsto
      | l = r_1 = r_2
      | o = \land
      | r = e^{i \theta_1} = e^{i \theta_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_1 e^{i \theta_1}
      | r = r_2 e^{i \theta_2}
      | c = 
}}
{{end-eqn}}
So $\phi$ is injective, thus bijective.
Also:
{{begin-eqn}}
{{eqn | l = \map \phi {r_1 e^{i \theta_1} \times r_2 e^{i \theta_2} }
      | r = \map \phi {r_1 r_2 e^{i \theta_1 + i \theta_2} }
      | c = Product of Complex Numbers in Exponential Form
}}
{{eqn | r = \paren {r_1 r_2, e^{i \theta_1 + i \theta_2} }
      | c = Definition of $\phi$
}}
{{eqn | r = \paren {r_1 \times r_2, e^{i \theta_1} \times e^{i \theta_2} }
      | c = Exponential of Sum
}}
{{eqn | r = \paren {r_1, e^{i\theta_1} } \times \paren {r_2, e^{i\theta_2} }
      | c = {{Defof|Operation Induced by Direct Product|subdef = General Definition}}
}}
{{eqn | r = \map \phi {r_1 e^{i \theta_1} } \times \map \phi {r_2 e^{i \theta_2} }
      | c = Definition of $\phi$
}}
{{end-eqn}}
{{explain|It is not clear how $\paren {r_1 \times r_2, e^{i \theta_1} \times e^{i \theta_2} } {{=}} \paren {r_1, e^{\theta_1} } \times \paren {r_2, e^{\theta_2} }$. The first $\times$ is the times of multiplication, real and complex, and the second appears to be the $\times$ of cartesian product. In any case, it needs to be established that $\paren {a \times b, c \times d} {{=}} \tuple {a, c} \times \tuple {b, d}$ and in what context this holds -- and indeed, what it actually means.}}
So $\phi$ is a group homomorphism.
Since it is bijective, it is a group isomorphism.
{{qed}}
Category:Complex Numbers
Category:External Direct Products
4ep7xddeee9p8yv0iibhegvgmdhbly7
Theorem: Quaternion Modulus in Terms of Conjugate

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\size {\mathbf x}$ be the modulus of $\mathbf x$.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
Then:
:$\size {\mathbf x}^2 \mathbf 1 = \mathbf x \overline {\mathbf x}$

Proof:
Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf x \overline {\mathbf x}
      | r = \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1
      | c = Product of Quaternion with Conjugate
}}
{{eqn | r = \size {\mathbf x}^2 \mathbf 1
      | c = {{Defof|Quaternion Modulus}}
}}
{{end-eqn}}
{{qed}}
Category:Quaternion Modulus
e6z89z3bstzik47cq3g6h73d68s8ezq
Theorem: Sufficient Condition for Quaternion Multiplication to Commute

In general, quaternion multiplication does not commute.
But, for $\mathbf x,\mathbf y \in \H$, $\mathbf x \times \mathbf y = \mathbf y \times \mathbf x$ if any one of the following conditions hold:
{{begin-eqn}}
{{eqn | n = 1a
      | l = \mathbf x, \mathbf y
      | o = \in
      | r = \set {a \mathbf 1 + b \mathbf i + 0 \mathbf j + 0 \mathbf k: a, b \in \R}
}}
{{eqn | n = 1b
      | l = \mathbf x, \mathbf y
      | o = \in
      | r = \set {a \mathbf 1 + 0 \mathbf i + c \mathbf j + 0 \mathbf k: a, c \in \R}
}}
{{eqn | n = 1c
      | l = \mathbf x, \mathbf y
      | o = \in
      | r = \set {a \mathbf 1 + 0 \mathbf i + 0 \mathbf j + d \mathbf k: a, d \in \R}
}}
{{eqn | n = 2a
      | l = \mathbf x
      | o = \in
      | r = \set {a \mathbf 1 + 0 \mathbf i + 0 \mathbf j + 0 \mathbf k: a \in \R}
}}
{{eqn | n = 2b
      | l = \mathbf y
      | o = \in
      | r = \set {a \mathbf 1 + 0 \mathbf i + 0 \mathbf j + 0 \mathbf k: a \in \R}
}}
{{eqn | n = 3
      | l = \mathbf x
      | r = \paren {a \mathbf 1 + 0 \mathbf i + 0 \mathbf j + 0 \mathbf k} \times \overline {\mathbf y}: a \in \R
}}
{{end-eqn}}

Proof:
=== Proof of $\paren 1$ ===
It follows directly from Complex Numbers form Subfield of Quaternions and Complex Multiplication is Commutative.
{{qed|lemma}}
Theorem: Complex Conjugation is Involution

Let $z = x + i y$ be a complex number.
Let $\overline z$ denote the complex conjugate of $z$.
Then the operation of complex conjugation is an involution:
:$\overline {\paren {\overline z} } = z$

Proof:
{{begin-eqn}}
{{eqn | l = \overline {\paren {\overline z} }
      | r = \overline {\paren {\overline {x + i y} } }
      | c = Definition of $z$
}}
{{eqn | r = \overline {x - i y}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = x + i y
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = z
      | c = Definition of $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Quaternion Modulus of Conjugate

Let $z = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\overline z$ be the conjugate of $z$.
Let $\cmod z$ be the quaternion modulus of $z$.
Then:
:$\cmod {\overline z} = \cmod z$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = a^2 + b^2 + c^2 + d^2
      | c = {{Defof|Quaternion Modulus}}
}}
{{eqn | l = \cmod {\overline z}
      | r = \cmod {a \mathbf 1 - b \mathbf i - c \mathbf j - d \mathbf k}
      | c = {{Defof|Quaternion Conjugate}}
}}
{{eqn | r = a^2 + \paren {-b}^2 + \paren {-c}^2 + \paren {-d}^2
      | c = {{Defof|Quaternion Modulus}}
}}
{{eqn | r = a^2 + b^2 + c^2 + d^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Quaternion Modulus
dwgpvr41a8er7xqgy28nekav2mi7kdt
Theorem: Quaternion Conjugation is Involution

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\overline {\mathbf x}$ denote the quaternion conjugate of $\mathbf x$.
Then the operation of quaternion conjugation is an involution:
:$\overline {\paren {\overline {\mathbf x} } } = \mathbf x$

Proof:
{{begin-eqn}}
{{eqn | l = \overline {\paren {\overline {\mathbf x} } }
      | r = \overline {\paren {\overline {a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k} } }
      | c = Definition of $\mathbf x$
}}
{{eqn | r = \overline {a \mathbf 1 - b \mathbf i - c \mathbf j - d \mathbf k}
      | c = {{Defof|Quaternion Conjugate}}
}}
{{eqn | r = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k
      | c = {{Defof|Quaternion Conjugate}}
}}
{{eqn | r = \mathbf x
      | c = Definition of $\mathbf x$
}}
{{end-eqn}}
{{qed}}
Category:Complex Conjugates
Category:Involutions
ntszc6votk2rt9orjp6f2atx26i52qa
Theorem: Sum of Quaternion Conjugates

Let $\mathbf x, \mathbf y \in \mathbb H$ be quaternions.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
Then:
:$\overline {\mathbf x + \mathbf y} = \overline {\mathbf x} + \overline {\mathbf y}$

Proof:
Let:
:$\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$
:$\mathbf y = e \mathbf 1 + f \mathbf i + g \mathbf j + h \mathbf k$
Then:
{{begin-eqn}}
{{eqn | l = \overline {\mathbf x + \mathbf y}
      | r = \overline {\paren {a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k} + \paren {e \mathbf 1 + f \mathbf i + g \mathbf j + h \mathbf k} }
      | c = 
}}
{{eqn | r = \overline {\paren {a + e} \mathbf 1 + \paren {b + f} \mathbf i + \paren {c + g} \mathbf j + \paren {d + h} \mathbf k}
      | c = {{Defof|Quaternion Addition}}
}}
{{eqn | r = \paren {a + e} \mathbf 1 - \paren {b + f} \mathbf i - \paren {c + g} \mathbf j - \paren {d + h} \mathbf k
      | c = {{Defof|Quaternion Conjugate}}
}}
{{eqn | r = \paren {a \mathbf 1 - b \mathbf i - c \mathbf j - d \mathbf k} + \paren {e \mathbf 1 - f \mathbf i - g \mathbf j - h \mathbf k}
      | c = {{Defof|Quaternion Addition}}
}}
{{eqn | r = \overline {\mathbf x} + \overline {\mathbf y}
      | c = {{Defof|Quaternion Conjugate}}
}}
{{end-eqn}}
{{qed}}
Category:Quaternions
osfjph590poncxwphvgne964u7ovsaz