avewright/proofwiki-math huggingface dataset:
Theorem: Mapping is Idempotent iff Restriction to Image is Identity Mapping

Let $S$ be a set.
Let $S^S$ denote the set of mappings from $S$ to itself.
Let $f \in S^S$ be a mapping on $S$.
Then:
:$f$ is idempotent
{{iff}}:
:the restriction of $f$ to $\Img f$ is the identity mapping.

Proof:
Recall the definitions:
:$\Img f$ denotes the image set of $f$
:The identity mapping $I_S$ is defined as:
::$\forall x \in f: \map {I_S} x = x$
:An idempotent mapping is a mapping with the property:
::$f \circ f = f$
:where $\circ$ denotes composition of mappings.
Theorem: Non-Cancellable Elements of Semigroup form Subsemigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $T \subseteq S$ be the subset of $S$ containing the elements of $S$ which are specifically not cancellable in $\struct {S, \circ}$.
Then $\struct {T, \circ}$ forms a subsemigroup of $S$.

Proof:
Recall the definition of cancellable element:
An element $x \in \struct {S, \circ}$ is '''cancellable''' {{iff}}:
:$\forall a, b \in S: x \circ a = x \circ b \implies a = b$
:$\forall a, b \in S: a \circ x = b \circ x \implies a = b$
From the Subsemigroup Closure Test it is sufficient to demonstrate that:
:$\forall x, y \in T: x \circ y \in T$
Let $x, y \in T$.
Then:
:$\exists a, b \in S: a \circ y = b \circ y \text { but } a \ne b$
or:
:$\exists a, b \in S: y \circ a = y \circ b \text { but } a \ne b$
{{WLOG}}, suppose that:
:$\exists a, b \in S: y \circ a = y \circ b \text { but } a \ne b$
Hence:
{{begin-eqn}}
{{eqn | l = y \circ a
      | r = y \circ b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \circ \paren {y \circ a}
      | r = x \circ \paren {y \circ b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x \circ y} \circ a
      | r = \paren {x \circ y} \circ b
      | c = 
}}
{{end-eqn}}
So we have:
:$\paren {x \circ y} \circ a = \paren {x \circ y} \circ b$
but $a \ne b$.
Hence $x \circ y$ is not cancellable.
As $x$ and $y$ are arbitrary, the result follows.
{{qed}}
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 6

:$\exists r \in \Q, n \in \Z, y \in \Z_p$:
::$(1) \quad x = r + p^n y$
::$(2) \quad$ the canonical expansion of $y$ is periodic.

Proof:
Let $\ldots d_i \ldots d_2 d_1 d_0 . d_{-1} d_{-2} \ldots d_{-m}$ be the canonical expansion of $x$.
By definition of eventually periodic there exists a finite sequence of $k$ digits of $x$:
:$\tuple {d_{n + k - 1} \ldots d_{n + 1} d_n }$
such that $n \ge 0$ and for all $s \in \Z_{\ge 0}$ and for all $j \in \set {0, 2, \ldots, k - 1}$:
:$d_{n + j + s k} = d_{n + j}$
where $k$ is the smallest $k$ to have this property.
We have:
{{begin-eqn}}
{{eqn | l = x 
      | r = \sum_{i \mathop = -m}^\infty d_i p^i
      | c = {{Defof|Canonical P-adic Expansion}}
}}
{{eqn | r = \begin{cases}
\ds 0 + \paren {\sum_{i \mathop = n}^\infty d_i p^i } & : -m = n \\
\ds \paren {\sum_{i \mathop = -m}^{n - 1} d_i p^i} + \paren {\sum_{i \mathop = n}^\infty d_i p^i } & : -m < n 
\end{cases}
      | c = as $-m \le n$
}}
{{eqn | r = \begin{cases}
\ds 0 + p^n \paren {\sum_{i \mathop = n}^\infty d_i p^{i - n} } & : -m = n \\
\ds \paren {\sum_{i \mathop = -m}^{n - 1} d_i p^i} + p^n \paren {\sum_{i \mathop = n}^\infty d_i p^{i - n} } & : -m < n 
\end{cases}
      | c = extracting common $p^n$ factor from each term
}}
{{end-eqn}}
Let:
:$\ds r = \begin{cases}
0 & : -m = n \\
\ds \sum_{i \mathop = -m}^{n - 1} d_i p^i & : -m < n 
\end{cases}$
:$\ds y = \sum_{i \mathop = n}^\infty d_i p^{i - n}$
Then:
:$x = r + p^n y$
We have {{hypothesis}}that:
:$r \in \Q$
Re-indexing the series for $y$, we have:
:$\ds y = \sum_{i \mathop = 0}^\infty d_{i + n} p^i$
By definition of $p$-adic integer:
:$y \in \Z_p$
By definition of canonical expansion, the canonical expansion of $y$ is:
:$\ldots d_{n + i} \ldots d_{n + 2} d_{n + 1} d_n$
Recall that for all $s \in \Z_{\ge 0}$ and for all $j \in \set {0, 2, \ldots, k - 1}$:
:$d_{n + j + s k} = d_{n + j}$
By definition of periodic:
:the canonical expansion of $y$ is periodic
{{qed}}
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
ck8ntkqgbf59nkx9uj1r9jr8xhwwxc9
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 7

:$1 + p^k + p^{2 k} + p^{3 k} + \cdots = \dfrac 1 {1 - p^k}$

Proof:
Let $S_n$ be the partial sum:
:$\ds S_n = \sum_{j \mathop = 0}^n p^{j k}$
We have:
{{begin-eqn}}
{{eqn | l = \paren {1 - p^k} S_n
      | r = \paren {1 - p^k} \sum_{j \mathop = 0}^n p^{j k}
}}
{{eqn | r = \paren {\sum_{j \mathop = 0}^n p^{j k} } - p^k \paren {\sum_{j \mathop = 0}^n p^{j k} }
      | c = distributing the partial sum across $1 - p^k$
}}
{{eqn | r = \paren {\sum_{j \mathop = 0}^n p^{j k} } - \paren {\sum_{j \mathop = 0}^n p^{\paren {j + 1} k} }
      | c = distributing $p^k$ across the partial sum
}}
{{eqn | r = 1 - p^k + p^k - p^{2 k} + p^{2 k} - \ldots - p^{n k} + p^{n k} - p^{\paren {n + 1} k}
      | c = rearranging terms
}}
{{eqn | r = 1 - p^ {\paren {n + 1} k}
      | c = as the series telescopes
}}
{{eqn | ll= \leadsto
      | l = \norm {\paren {1 - p^k} S_n - 1}_p
      | r = \norm {1 - p^{\paren {n + 1} k} - 1}_p
}}
{{eqn | r = \norm {- p^{\paren {n + 1} k} }_p
      | c = cancelling
}}
{{eqn | r = \norm {p^{\paren {n + 1} k} }_p
      | c = Norm of Negative in Division Ring
}}
{{eqn | r = \dfrac 1 {p^{\paren {n + 1} k} }
      | c = {{Defof|P-adic Norm on Rational Numbers}}
}}
{{eqn | o = \to
      | r = 0
      | c = as $n \to \infty$
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \paren{1 - p^k} S_n
      | r = 1
      | c = {{Defof|Convergent P-adic Sequence}}
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} S_n
      | r = \dfrac 1 {\paren {1 - p^k} }
      | c = Multiple Rule for Sequences in Normed Division Ring 
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 0}^\infty p^{j k}
      | r = \dfrac 1 {\paren {1 - p^k} }
      | c = {{Defof|Series}}
}}
{{end-eqn}}
{{qed}}
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
ju1fch3nzwz74f4oppyv53jg88twofo
Theorem: Smooth Vector Field as Sum of Smooth Horizontal and Vertical Vector Fields

Let $\tilde M, M$ be smooth manifolds.
Let $\pi : \tilde M \to M$ be a smooth submersion.
Let $\tilde g$ be a Riemannian metric on $\tilde M$.
Let $W$ be a smooth vector field on $\tilde M$.
Then $W$ can be uniquely decomposed as a sum:
:$W = W^H + W^V$
where $W^H$ and $W^V$ are smooth horizontal and vertical vector fields.

Proof:
{{ProofWanted|some of the assumptions may be unnecessary}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of C n

:Each of $\CC_1$, $\CC_2$ and $\CC_3$ has $3^4 - 3$ elements.

Proof:
Recall the definition of (group) automorphism:
:$\phi$ is an automorphism on $\struct {S, \circ}$ {{iff}}:
::$\phi$ is a permutation of $S$
::$\phi$ is a homomorphism on $\struct {S, \circ}$: $\forall a, b \in S: \map \phi {a \circ b} = \map \phi a \circ \map \phi b$
From Identity Mapping is Group Automorphism, $I_S$ is always an automorphism on $\struct {S, \circ}$.
Hence it is not necessary to analyse the effect of $I_S$ on $S$.
{{WLOG}}, we will analyse the nature of $\CC_1$.
Let $n$ be the number of operations $\circ$ on $S$ such that $\tuple {a, b}$ is an automorphism of $\struct {S, \circ}$.
Let us denote the permutation $\tuple {a, b}$ as $r: S \to S$, defined as:
:$r = \map r a = b, \map r b = a, \map r c = c$
We select various product elements $x \circ y \in S$ and determine how $r$ constrains other product elements.
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of D

:$\DD$ has $19 \, 422$ elements.

Proof:
Let $n$ denote the cardinality of $\DD$.
Equivalently, $n$ equals the number of operations $\circ$ on $S$ on which the only automorphism is $I_S$.
Recall these definitions:
Let $\AA$, $\BB$, $\CC_1$, $\CC_2$ and $\CC_3$ be respectively the set of all operations $\circ$ on $S$ such that the groups of automorphisms of $\struct {S, \circ}$ are as follows:
{{begin-eqn}}
{{eqn | l = \AA
      | o = :
      | r = \map \Gamma S
      | c = where $\map \Gamma S$ is the symmetric group on $S$
}}
{{eqn | l = \BB
      | o = :
      | r = \set {I_S, \tuple {a, b, c}, \tuple {a, c, b} }
      | c = where $I_S$ is the identity mapping on $S$
}}
{{eqn | l = \CC_1
      | o = :
      | r = \set {I_S, \tuple {a, b} }
}}
{{eqn | l = \CC_2
      | o = :
      | r = \set {I_S, \tuple {a, c} }
}}
{{eqn | l = \CC_3
      | o = :
      | r = \set {I_S, \tuple {b, c} }
}}
{{end-eqn}}
Theorem: Equivalence of Definitions of Quaternion Modulus

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion, where $a, b, c, d \in \R$.
{{TFAE|def = Quaternion Modulus}}

Proof:
Let $\mathbf x = \begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix}$ be the matrix form of quaternion $\mathbf x$.
{{begin-eqn}}
{{eqn | l = \size {\mathbf x}
      | r = \sqrt {\map \det {\mathbf x} }
      | c =
}}
{{eqn | r = \sqrt {\map \det {\begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix} } }
      | c =
}}
{{eqn | r = \sqrt {\paren {a + b i} \paren {a - b i} - \paren {c + d i} \paren {-c + d i} }
      | c = {{Defof|Determinant of Matrix}}
}}
{{eqn | r = \sqrt {\paren {a^2 + b^2} - \paren {-c^2 - d^2} }
      | c =
}}
{{eqn | r = \sqrt {a^2 + b^2 + c^2 + d^2}
      | c =
}}
{{end-eqn}}
{{qed}}
Category:Quaternion Modulus
cef8s76s9qoho9sh4yrt93fr51sokd8
Theorem: Smooth Vector Field has Unique Smooth Horizontal Lift

Let $\tilde M, M$ be smooth manifolds.
Let $\pi : \tilde M \to M$ be a smooth submersion.
Let $\tilde g$ be a Riemannian metric on $\tilde M$.
Let $W$ be a smooth vector field on $M$.
Then $W$ has the unique smooth horizontal lift to $\tilde M$.

Proof:
{{ProofWanted|some of the assumptions may be unnecessary}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of C n/Lemma 1

$c$ is an idempotent element under $\circ$, that is:
:$c \circ c = c$

Proof:
Recall the definition of (group) automorphism:
:$\phi$ is an automorphism on $\struct {S, \circ}$ {{iff}}:
::$\phi$ is a permutation of $S$
::$\phi$ is a homomorphism on $\struct {S, \circ}$: $\forall a, b \in S: \map \phi {a \circ b} = \map \phi a \circ \map \phi b$
Let us denote $\tuple {a, b}$ as the mapping $r: S \to S$:
:$r := \map r a = b, \map r b = a, \map r c = c$
{{AimForCont}} $c$ is not idempotent.
Then $c \circ c = x$, where $x = a$ or $x = b$.
{{begin-eqn}}
{{eqn | l = c \circ c
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map r c \circ \map r c
      | r = \map r x
      | c = 
}}
{{eqn | o = \ne
      | r = x
      | c = 
}}
{{end-eqn}}
So it cannot be the case that $c \circ c = a$ or $c \circ c = b$.
Hence $c \circ c = c$, that is, $c$ is idempotent.
{{qed}}
Category:Sets of Operations on Set of 3 Elements
t96c229oa4i64cqx1ytzwu5vcdyrwmj
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of C n/Lemma 2

{{begin-eqn}}
{{eqn | l = a \circ a = a
      | o = \iff
      | r = b \circ b = b
}}
{{eqn | l = a \circ a = b
      | o = \iff
      | r = b \circ b = a
}}
{{eqn | l = a \circ a = c
      | o = \iff
      | r = b \circ b = c
}}
{{eqn | l = a \circ b = a
      | o = \iff
      | r = b \circ a = b
}}
{{eqn | l = a \circ b = b
      | o = \iff
      | r = b \circ a = a
}}
{{eqn | l = a \circ b = c
      | o = \iff
      | r = b \circ a = c
}}
{{eqn | l = a \circ c = a
      | o = \iff
      | r = b \circ c = b
}}
{{eqn | l = a \circ c = b
      | o = \iff
      | r = b \circ c = a
}}
{{eqn | l = a \circ c = c
      | o = \iff
      | r = b \circ c = c
}}
{{eqn | l = c \circ a = a
      | o = \iff
      | r = c \circ b = b
}}
{{eqn | l = c \circ a = b
      | o = \iff
      | r = c \circ b = a
}}
{{eqn | l = c \circ a = c
      | o = \iff
      | r = c \circ b = c
}}
{{end-eqn}}

Proof:
Recall the definition of (group) automorphism:
:$\phi$ is an automorphism on $\struct {S, \circ}$ {{iff}}:
::$\phi$ is a permutation of $S$
::$\phi$ is a homomorphism on $\struct {S, \circ}$: $\forall a, b \in S: \map \phi {a \circ b} = \map \phi a \circ \map \phi b$
Let us denote $\tuple {a, b}$ as the mapping $r: S \to S$:
:$r := \map r a = b, \map r b = a, \map r c = c$
In Lemma 1 it has been established that:
{{begin-eqn}}
{{eqn | l = a \circ a = a
      | o = \iff
      | r = b \circ b = b
}}
{{eqn | l = a \circ a = b
      | o = \iff
      | r = b \circ b = a
}}
{{eqn | l = a \circ a = c
      | o = \iff
      | r = b \circ b = c
}}
{{end-eqn}}
We select values for $x$ in the expression $a \circ b = x$ and determine how $r$ constrains other product elements.
Thus:
{{begin-eqn}}
{{eqn | l = a \circ x
      | r = a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map r a \circ \map r x
      | r = \map r a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b \circ \map r x
      | r = b
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = a \circ b = a
      | o = \iff
      | r = b \circ a = b
}}
{{eqn | l = a \circ b = b
      | o = \iff
      | r = b \circ a = a
}}
{{eqn | l = a \circ b = c
      | o = \iff
      | r = b \circ a = c
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = x \circ a
      | r = a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map r x \circ \map r a
      | r = \map r a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map r x \circ b
      | r = b
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = c \circ a = a
      | o = \iff
      | r = c \circ b = b
}}
{{eqn | l = c \circ a = b
      | o = \iff
      | r = c \circ b = a
}}
{{eqn | l = c \circ a = c
      | o = \iff
      | r = c \circ b = c
}}
{{end-eqn}}
{{qed}}
Category:Sets of Operations on Set of 3 Elements
591pnlhaeknj6p7y4ghabq3pfbxqzwj
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of A/Isomorphism Classes

:The elements of $\AA$ are each in its own isomorphism class.

Proof:
Recall from Automorphism Group of $\AA$ the elements of $\AA$, expressed in Cayley table form:
:$\begin {array} {c|ccc}
\to & a & b & c \\
\hline
a & a & b & c \\
b & a & b & c \\
c & a & b & c \\
\end {array}
\qquad
\begin {array} {c|ccc}
\gets & a & b & c \\
\hline
a & a & a & a \\
b & b & b & b \\
c & c & c & c \\
\end {array}
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & a & c & b \\
b & c & b & a \\
c & b & a & c \\
\end {array}$
We have from Algebraic Structures formed by Left and Right Operations are not Isomorphic for Cardinality Greater than 1 that $\struct {S, \to}$ and $\struct {S, \gets}$ are not isomorphic.
Observe from the Cayley table $\circ$ that:
:$(1): \quad \forall x, y \in S: x \ne y \implies x \circ y \ne x \land x \circ y \ne y$
{{AimForCont}} there exists an isomorphism $\phi$ from $\struct {S, \to}$ to $\struct {S, \circ}$.
We have:
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {a \to b}
      | r = \map \phi a \circ \map \phi b
      | c = {{Defof|Isomorphism (Abstract Algebra)|Isomorphism}}
}}
{{eqn | r = \map \phi c
      | c = from $(1)$
}}
{{eqn | r = \map \phi b
      | c = {{Defof|Right Operation}}
}}
{{end-eqn}}
Hence:
:$\map \phi c = \map \phi b$
which means $\phi$ is not an injection.
That is, $\phi$ is not a bijection and hence not an isomorphism.
Hence by Proof by Contradiction there exists no isomorphism from $\struct {S, \to}$ to $\struct {S, \circ}$.
In a similar way:
{{AimForCont}} there exists an isomorphism $\phi$ from $\struct {S, \gets}$ to $\struct {S, \circ}$.
We have:
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {a \gets  b}
      | r = \map \phi a \circ \map \phi b
      | c = {{Defof|Isomorphism (Abstract Algebra)|Isomorphism}}
}}
{{eqn | r = \map \phi c
      | c = from $(1)$
}}
{{eqn | r = \map \phi a
      | c = {{Defof|Left Operation}}
}}
{{end-eqn}}
Hence:
:$\map \phi c = \map \phi a$
which means $\phi$ is not an injection.
That is, $\phi$ is not a bijection and hence not an isomorphism.
Hence by Proof by Contradiction there exists no isomorphism from $\struct {S, \gets}$ to $\struct {S, \circ}$.
It has been shown that none of the elements of $\AA$ is isomorphism to any of the others.
The result follows by definition of isomorphism class.
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Isomorphism Classes

Let $\MM$ be the set of all operations $\circ$ on $S$.
Then the elements of $\MM$ are divided in $3330$ isomorphism classes.
That is, up to isomorphism, there are $3330$ operations on $S$.

Proof:
From Automorphism Group of $\AA$: Isomorphism Classes:
:each element of $\AA$ is in its own isomorphism class.
Hence $\AA$ contributes $3$ isomorphism classes.
From Automorphism Group of $\BB$: Isomorphism Classes:
:the $24$ elements of $\BB$ form $12$ isomorphism classes in pairs.
From Automorphism Group of $\CC_n$: Isomorphism Classes:
:the $3 \times 78$ elements of $\CC$ form $78$ isomorphism classes in threes.
From Automorphism Group of $\DD$: Isomorphism Classes:
:the $19 \, 422$ elements of $\DD$ form $3237$ isomorphism classes in sixes.
Thus there are $3 + 12 + 78 + 3237 = 3330$ isomorphism classes.
{{qed}}
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 8

:$\ds \lim_{n \mathop \to \infty} \dfrac a {p^{n+1}} = 0$

Proof:
From Sequence of Powers of Rational Number less than One:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 {p^n} = 0$
From Multiple Rule for Sequences:
:$\ds \lim_{n \mathop \to \infty} \dfrac a p \cdot \paren{\dfrac 1 {p^n} } = \dfrac a p \cdot 0 = 0$
The result follows.
{{qed}}
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
jx8jiwxbzlk9uv64jt97lbqob9xvs6i
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 9

:$\ds \lim_{n \mathop \to \infty} \dfrac {a - \paren{p^{n+1} - 1} b } {p^{n+1}} = -b$

Proof:
From Sequence of Reciprocals is Null Sequence:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 n = 0$
From Combined Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \dfrac {n - 1} n = \lim_{n \mathop \to \infty} 1 - \dfrac 1 n  = 1$ 
From Limit of Subsequence equals Limit of Real Sequence:
:$\ds \lim_{n \mathop \to \infty} \dfrac {p^{n + 1} - 1} {p^{n + 1} } = 1$
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of A/Operations with Identity

:None of the operations of $\AA$ has an identity element.

Proof:
Recall from Automorphism Group of $\AA$ the elements of $\AA$, expressed in Cayley table form:
:$\begin{array}{c|ccc}
\to & a & b & c \\
\hline
a & a & b & c \\
b & a & b & c \\
c & a & b & c \\
\end{array}
\qquad
\begin{array}{c|ccc}
\gets & a & b & c \\
\hline
a & a & a & a \\
b & b & b & b \\
c & c & c & c \\
\end{array}
\qquad
\begin{array}{c|ccc}
\circ & a & b & c \\
\hline
a & a & c & b \\
b & c & b & a \\
c & b & a & c \\
\end{array}$
The result is apparent by inspection.
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of C n/Operations with Identity

:$9$ of the operations of each of $\CC_1$, $\CC_2$ and $\CC_3$ has an identity element.

Proof:
{{WLOG}}, we will analyse the nature of $\CC_1$.
Recall this lemma:
Theorem: Element of Horizontal Space as Horizontal Lift of Vector Field

Let $\tilde M, M$ be smooth manifolds.
Let $\pi : \tilde M \to M$ be a smooth submersion.
Let $\tilde g$ be a Riemannian metric on $\tilde M$.
Let $H_x$ be a horizontal tangent space of $\tilde M$ at $x$.
Let $\map {\mathfrak{X}} M$ be the space of smooth vector fields of $M$.
Then for every $x \in \tilde M$ and every $v \in H_x$ there is a vector field $X \in \map {\mathfrak{X}} M$ whose horizontal lift $\tilde X$ satisfies $\tilde X_x = v$.

Proof:
{{ProofWanted|some of the assumptions may be unnecessary}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of D/Operations with Identity

:$216$ of the operations of $\DD$ has an identity element.

Proof:
Let $n$ denote the number of operations of $\DD$ which have an identity element.
Recall these definitions:
Let $\AA$, $\BB$, $\CC_1$, $\CC_2$ and $\CC_3$ be respectively the set of all operations $\circ$ on $S$ such that the groups of automorphisms of $\struct {S, \circ}$ are as follows:
{{begin-eqn}}
{{eqn | l = \AA
      | o = :
      | r = \map \Gamma S
      | c = where $\map \Gamma S$ is the symmetric group on $S$
}}
{{eqn | l = \BB
      | o = :
      | r = \set {I_S, \tuple {a, b, c}, \tuple {a, c, b} }
      | c = where $I_S$ is the identity mapping on $S$
}}
{{eqn | l = \CC_1
      | o = :
      | r = \set {I_S, \tuple {a, b} }
}}
{{eqn | l = \CC_2
      | o = :
      | r = \set {I_S, \tuple {a, c} }
}}
{{eqn | l = \CC_3
      | o = :
      | r = \set {I_S, \tuple {b, c} }
}}
{{end-eqn}}
Let $N$ be the total number of operations on $S$ which have an identity element.
Let:
:$A$ denote the number of operations in $\AA$ which have an identity element
:$B$ denote the number of operations in $\BB$ which have an identity element
:$C$ denote the total number of operations in $\CC_1$, $\CC_2$ and $\CC_3$ which have an identity element.
From the lemma, and from the Fundamental Principle of Counting:
:$N = A + B + C + D$
From Count of Binary Operations with Identity:
:$N = 3^5 = 243$
Then we have:
:From Automorphism Group of $\AA$: Operations with Identity: $A = 0$
:From Automorphism Group of $\BB$: Operations with Identity: $B = 0$
:From Automorphism Group of $\CC_n$: Operations with Identity: $C = 3 \times 9$
Hence we have:
{{begin-eqn}}
{{eqn | l = n
      | r = N - A - B - C
      | c = 
}}
{{eqn | r = 243 - 0 - 0 - 27
      | c = 
}}
{{eqn | r = 216
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Operations with Identity

Let $\NN$ be the set of all operations $\circ$ on $S$ which have an identity element.
Then the elements of $\NN$ are divided in $45$ isomorphism classes.
That is, up to isomorphism, there are $45$ operations on $S$ which have an identity element.

Proof:
From Automorphism Group of $\AA$: Operations with Identity:
:there are no elements of $\AA$ which have an identity element.
From Automorphism Group of $\BB$: Operations with Identity:
:there are no elements of $\BB$ which have an identity element.
From Automorphism Group of $\CC_n$: Operations with Identity:
:there are $3 \times 9$ elements of $\CC$ which have an identity element.
From Automorphism Group of $\DD$: Operations with Identity:
:there are $216$ elements of $\DD$ which have an identity element.
From Automorphism Group of $\CC_n$: Isomorphism Classes:
:the elements of $\CC$ form isomorphism classes in threes.
From Automorphism Group of $\DD$: Isomorphism Classes:
:the elements of $\DD$ form isomorphism classes in sixes.
Hence there are:
:$\dfrac {3 \times 9} 3 = 9$ isomorphism classes of elements of $\CC$ which have an identity element.
:$\dfrac {216} 6 = 36$ isomorphism classes of elements of $\DD$ which have an identity element.
Thus there are $3 + 36 = 45$ isomorphism classes of operations $\circ$ on $S$ which have an identity element..
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of A/Commutative Operations

:Exactly $1$ of the operations of $\AA$ is commutative.

Proof:
Recall from Automorphism Group of $\AA$ the elements of $\AA$, expressed in Cayley table form:
:<nowiki>$\begin {array} {c|ccc}
\to & a & b & c \\
\hline
a & a & b & c \\
b & a & b & c \\
c & a & b & c \\
\end {array}
\qquad
\begin {array} {c|ccc}
\gets & a & b & c \\
\hline
a & a & a & a \\
b & b & b & b \\
c & c & c & c \\
\end {array}
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & a & c & b \\
b & c & b & a \\
c & b & a & c \\
\end {array}$</nowiki>
From Cayley Table for Commutative Operation is Symmetrical about Main Diagonal, it is apparent by inspection that of the above:
:<nowiki>$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & a & c & b \\
b & c & b & a \\
c & b & a & c \\
\end {array}$</nowiki>
is the only Cayley table of a commutative operation.
{{qed}}