avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Reciprocal of 1 minus Cosine of x

:$\ds \int \frac {\d x} {1 - \cos x} = -\cot \frac x 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \tan \frac x 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 - \cos x}
      | r = \int \frac {\dfrac {2 \rd u} {1 + u^2} } {1 - \dfrac {1 - u^2} {1 + u^2} }
      | c = Weierstrass Substitution
}}
{{eqn | r = \int \frac {2 \rd u} {1 + u^2 - \paren {1 - u^2} }
      | c = multiplying top and bottom by $1 + u^2$
}}
{{eqn | r = \int \frac {\d u} {u^2}
      | c = simplifying
}}
{{eqn | r = \frac {-1} u + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {-1} {\tan \dfrac x 2} + C
      | c = substituting for $u$
}}
{{eqn | r = -\cot \frac x 2 + C
      | c = Cotangent is Reciprocal of Tangent
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Sine of x by Cosine of x

:$\ds \int \frac {\d x} {\sin x \cos x} = \ln \size {\tan x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin x \cos x}
      | r = \int \frac {\sec x \rd x} {\sin x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \int \frac {\sec^2 x \rd x} {\sin x \sec x}
      | c = multiplying top and bottom by $\sec x$
}}
{{eqn | r = \int \frac {\sec^2 x \rd x} {\frac {\sin x} {\cos x} }
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \int \frac {\sec^2 x \rd x} {\tan x}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \ln \size {\tan x} + C
      | c = Primitive of $\dfrac {\sec^2 a x} {\tan a x}$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arcsine Function

:$\ds \int \arcsin x \rd x = x \arcsin x + \sqrt {1 - x^2} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsin x
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin u 
      | r = x
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \cos u 
      | r = \sqrt {1 - x^2}
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arcsin x \rd x
      | r = \int u \cos u \rd u
      | c = Primitive of Function of Arcsine
}}
{{eqn | r = \cos u + u \sin u + C
      | c = Primitive of $x \cos a x$
}}
{{eqn | r = \cos u + u x + C
      | c = Substitution for $\sin u$ from $\paren 1$
}}
{{eqn | r = \sqrt {1 - x^2} + u x + C
      | c = Substitution for $\cos u$ from $\paren 2$
}}
{{eqn | r = x \arcsin x + \sqrt {1 - x^2} + C
      | c = Substitution for $u$ and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent Function

:$\ds \int \arctan x \rd x = x \arctan x - \frac {\map \ln {x^2 + 1} } 2 + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan x
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \tan u 
      | r = x
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sec u 
      | r = \sqrt {1 + x^2}
      | c = Difference of Squares of Secant and Tangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arctan x \rd x
      | r = \int u \sec^2 u \rd u
      | c = Primitive of Function of Arctangent
}}
{{eqn | r = u \tan u + \ln \size {\cos u} + C
      | c = Primitive of $x \sec^2 a x$ with $a = 1$
}}
{{eqn | r = u \tan u - \ln \size {\sec u} + C
      | c = Logarithm of Reciprocal and Secant is Reciprocal of Cosine
}}
{{eqn | r = u x - \ln \size {\sec u} + C
      | c = Substitution for $\tan u$ from $\paren 1$
}}
{{eqn | r = u x - \ln \size {\sqrt {1 + x^2} } + C
      | c = Substitution for $\sec u$ from $\paren 2$
}}
{{eqn | r = x \arctan x - \ln \size {\sqrt {1 + x^2} } + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arctan x - \frac {\ln \size {x^2 + 1} } 2 + C
      | c = Logarithm of Power
}}
{{eqn | r = x \arctan x - \frac {\map \ln {x^2 + 1} } 2 + C
      | c = $x^2 + 1$ always positive
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccotangent Function

:$\ds \int \arccot x \rd x = x \arccot x + \frac {\map \ln {x^2 + 1} } 2 + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccot x
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cot u 
      | r = x
      | c = {{Defof|Arccotangent}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \csc u 
      | r = \sqrt {1 + x^2}
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arccot x \rd x
      | r = -\int u \csc^2 u \rd u
      | c = Primitive of Function of Arccotangent
}}
{{eqn | r = -\paren {-u \cot u + \ln \size {\sin u} } + C
      | c = Primitive of $x \csc^2 a x$ with $a := 1$
}}
{{eqn | r = u \cot u - \ln \size {\sin u} + C
      | c = simplifying
}}
{{eqn | r = u \cot u + \ln \size {\csc u} + C
      | c = Logarithm of Reciprocal and Cosecant is Reciprocal of Sine
}}
{{eqn | r = u x + a \ln \size {\csc u} + C
      | c = Substitution for $\cot u$ from $(1)$
}}
{{eqn | r = x u + a \ln \size {\sqrt {1 + x^2} } + C
      | c = Substitution for $\csc u$ from $(2)$
}}
{{eqn | r = x \arccot x + \ln \size {\sqrt {1 + x^2} } + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arccot x + \frac 1 2 \ln \size {x^2 + 1} + C
      | c = Logarithm of Power and simplifying
}}
{{eqn | r = x \arccot x + \frac {\map \ln {x^2 + 1} } 2 + C
      | c = $x^2 + 1$ always positive
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of x squared minus a squared/Arcsine Form

:$\ds \int \frac {\d x} {x \sqrt {x^2 - a^2} } = -\frac 1 a \arcsin \size {\frac a x} + C$
for $0 < a < \size x$.

Proof:
We have that $\sqrt {x^2 - a^2}$ is defined only when $x^2 > a^2$, that is, either:
:$x > a$
or:
:$x < -a$
where it is assumed that $a > 0$.
Hence:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 - a^2} }
      | r = \frac 1 a \arccos \size {\frac a x} + C
      | c = Primitive of $\dfrac 1 {x \sqrt {x^2 - a^2} }$: Arccosine Form
}}
{{eqn | r = \dfrac \pi 2 - \frac 1 a \arcsin \size {\frac a x} + C
      | c = Sum of Arcsine and Arccosine
}}
{{eqn | r = -\frac 1 a \arcsin \size {\frac a x} + C
      | c = subsuming $\dfrac \pi 2$ into arbitrary constant $C$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of x squared plus a squared/Inverse Hyperbolic Sine Form

:$\ds \int \frac {\d x} {x \sqrt {x^2 + a^2} } = -\frac 1 a \sinh^{-1} {\frac a x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 + a^2} }
      | r = -\frac 1 a \csch^{-1} {\frac x a} + C
      | c = Primitive of $\dfrac 1 {x \sqrt {x^2 + a^2} }$: Inverse Hyperbolic Cosecant Form
}}
{{eqn | r = -\frac 1 a \sinh^{-1} {\frac a x} + C
      | c = Real Area Hyperbolic Sine of Reciprocal equals Real Area Hyperbolic Cosecant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of a squared minus x squared/Arccosine Form

:$\ds \int \sqrt {a^2 - x^2} \rd x = \frac {x \sqrt {a^2 - x^2} } 2 - \frac {a^2} 2 \arccos \frac x a + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \int \sqrt {a^2 - x^2} \rd x
      | r = \frac {x \sqrt {a^2 - x^2} } 2 + \frac {a^2} 2 \arcsin \frac x a + C
}}
{{eqn | r = \frac {x \sqrt {a^2 - x^2} } 2 + \paren {\dfrac \pi 2 - \frac {a^2} 2 \arcsin \frac x a} + C
      | c = Sum of Arcsine and Arccosine
}}
{{eqn | r = \frac {x \sqrt {a^2 - x^2} } 2 - \frac {a^2} 2 \arccos \frac x a + C
      | c = subsuming $\dfrac \pi 2$ into arbitrary constant $C$
}}
{{end-eqn}}
{{qed}}
Theorem: Isomorphisms between Additive Group of Integers Modulo 4 and Reduced Residue System Modulo 5 under Multiplication

Let $\struct {\Z_4, +_4}$ denote the additive group of integers modulo $4$.
Let $\struct {\Z'_5, \times_5}$ denote the multiplicative group of reduced residues modulo $5$.
There are $2$ (group) isomorphisms from $\struct {\Z_4, +_4}$ onto $\struct {\Z'_5, \times_5}$.

Proof:
Let us recall the Cayley table of $\struct {\Z_4, +_4}$:
{{:Modulo Addition/Cayley Table/Modulo 4}}
and the Cayley Table of $\struct {\Z'_5, \times_5}$:
{{:Multiplicative Group of Reduced Residues Modulo 5/Cayley Table}}
Each of these is the cyclic group of order $4$.
Each has $2$ generators, each of $1$ element.
Hence you can get an isomorphism from $\struct {\Z_4, +_4}$ to $\struct {\Z'_5, \times_5}$ by setting up the mappings:
:$\phi: \struct {\Z_4, +_4} \to \struct {\Z'_5, \times_5}: \forall x \in \Z_4: \map \phi x = \begin {cases} \eqclass 4 0 & : x = \eqclass 5 1 \\ \eqclass 4 1 & : x = \eqclass 5 2 \\ \eqclass 4 2 & : x = \eqclass 5 4 \\ \eqclass 4 3 & : x = \eqclass 5 3 \end {cases}$
:$\psi: \struct {\Z_4, +_4} \to \struct {\Z'_5, \times_5}: \forall x \in \Z_4: \map \psi x = \begin {cases} \eqclass 4 0 & : x = \eqclass 5 1 \\ \eqclass 4 1 & : x = \eqclass 5 3 \\ \eqclass 4 2 & : x = \eqclass 5 4 \\ \eqclass 4 3 & : x = \eqclass 5 2 \end {cases}$
{{qed}}
Theorem: Max and Min Operations on Real Numbers are Isomorphic

Let $\R$ denote the set of real numbers.
Let $\vee$ and $\wedge$ denote the max operation and min operation respectively.
Let $\struct {\R, \vee}$ and $\struct {\R, \wedge}$ denote the algebraic structures formed from the above.
Then $\struct {\R, \vee}$ and $\struct {\R, \wedge}$ are isomorphic.

Proof:
First we note that from:
:Min Operation on Toset forms Semigroup
and:
:Max Operation on Toset forms Semigroup
both $\struct {\R, \vee}$ and $\struct {\R, \wedge}$ are semigroups.
Let $\phi: \R \to \R$ defined as:
:$\forall x \in \R: \map \phi x = -x$
We have that:
:$-x = -y \iff x = y$
which demonstrates that $\phi$ is a bijection.
Then we have:
{{begin-eqn}}
{{eqn | q = \forall x, y \in \R
      | l = \map \phi {x \vee y}
      | r = -\paren {x \vee y}
      | c = 
}}
{{eqn | r = \paren {-x} \wedge \paren {-y}
      | c = 
}}
{{eqn | r = \map \phi x \wedge \map \phi y
      | c = 
}}
{{end-eqn}}
which demonstrates that $\phi$ is a (semigroup) homomorphism.
The result follows by definition of (semigroup) isomorphism.
{{qed}}
Theorem: Mapping on Quadratic Integers over 3 to Conjugate is Automorphism

Let $\Z \sqbrk {\sqrt 3}$ denote the set of quadratic integers over $3$:
:$\Z \sqbrk {\sqrt 3} := \set {a + b \sqrt 3: a, b \in \Z}$
that is, all numbers of the form $a + b \sqrt 3$ where $a$ and $b$ are integers.
Then the mapping $\phi: \Z \sqbrk {\sqrt 3} \to \Z \sqbrk {\sqrt 3}$ defined as:
:$\forall x = a + b \sqrt 3 \in \Z \sqbrk {\sqrt 3}: \map \phi {a + b \sqrt 3} = a - b \sqrt 3$
is a ring automorphism.

Proof:
We have Quadratic Integers over 2 form Subdomain of Reals.
First we note that:
:$\forall x \in \Z \sqbrk {\sqrt 3}: \map \phi x \in \Z \sqbrk {\sqrt 3}$
Theorem: Multiplicative Group of Complex Numbers is not Isomorphic to Multiplicative Group of Real Numbers

Let $\struct {\C_{\ne 0}, \times}$ be the multiplicative group of complex numbers.
Let $\struct {\R_{\ne 0}, \times}$ be the multiplicative group of real numbers.
Then $\struct {\C_{\ne 0}, \times}$ is not isomorphic to $\struct {\R_{\ne 0}, \times}$.

Proof:
{{AimForCont}} $\struct {\C_{\ne 0}, \times}$ is isomorphic to $\struct {\R_{\ne 0}, \times}$.
Let $\phi: \C_{\ne 0} \to \R_{\ne 0}$ be an isomorphism.
Note that $\order i = 4$ in $\struct {\C_{\ne 0}, \times}$.
By Group Isomorphism Preserves Order of Group Element:
:$\order {\map \phi i} = 4$ in $\struct {\R_{\ne 0}, \times}$
Then $\paren {\map \phi i}^4 = 1$.
So $\paren {\map \phi i}^2 = \pm 1$.
In $\R$ we must have $\paren {\map \phi i}^2 \ge 0$.
Hence $\paren {\map \phi i}^2 = 1$.
This gives $\map \phi i = \pm 1$.
However $\order 1 = 1$ and $\order {-1} = 2$ in $\struct {\R_{\ne 0}, \times}$.
Thus there is no order $4$ element in $\struct {\R_{\ne 0}, \times}$, and thus $\map \phi i$ does not exist.
Therefore $\phi$ is not an isomorphism.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Multiplicative Group of Complex Numbers is not Isomorphic to Additive Group of Complex Numbers

Let $\struct {\C_{\ne 0}, \times}$ be the multiplicative group of complex numbers.
Let $\struct {\C, +}$ be the additive group of complex numbers.
Then $\struct {\C_{\ne 0}, \times}$ is not isomorphic to $\struct {\C, +}$.

Proof:
A direct application of Additive Group and Multiplicative Group of Field are not Isomorphic.
{{qed}}
Theorem: Multiplicative Group of Complex Numbers is not Isomorphic to Additive Group of Real Numbers

Let $\struct {\C_{\ne 0}, \times}$ be the multiplicative group of complex numbers.
Let $\struct {\R, +}$ be the additive group of real numbers.
Then $\struct {\C_{\ne 0}, \times}$ is not isomorphic to $\struct {\R, +}$.

Proof:
{{AimForCont}} $\struct {\C_{\ne 0}, \times}$ is isomorphic to $\struct {\R, +}$.
Let $\phi: \C_{\ne 0} \to \R$ be an isomorphism.
Note that $\order i = 4$ in $\struct {\C_{\ne 0}, \times}$.
By Group Isomorphism Preserves Order of Group Element:
:$\order {\map \phi i} = 4$ in $\struct {\R, +}$
Then $4 \map \phi i = 0$.
So $\map \phi i = 0$.
However $\order 0 = 1$.
Thus there is no order $4$ element in $\struct {\R, +}$, and thus $\map \phi i$ does not exist.
Therefore $\phi$ is not an isomorphism.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Additive Group of Rational Numbers is not Isomorphic to Multiplicative Group of Rational Numbers

Let $\struct {\Q, +}$ be the additive group of rational numbers.
Let $\struct {\Q_{\ne 0}, \times}$ be the multiplicative group of rational numbers.
Then $\struct {\Q_{\ne 0}, \times}$ is not isomorphic to $\struct {\Q, +}$.

Proof:
A direct application of Additive Group and Multiplicative Group of Field are not Isomorphic.
{{qed}}
Theorem: Permutation of Set is Automorphism of Set under Left Operation

Let $S$ be a set.
Let $\struct {S, \gets}$ be the algebraic structure formed from $S$ under the left operation.
Let $f$ be a permutation on $S$.
Then $f$ is an automorphism of $f$.

Proof:
We have {{hypothesis}} that $f$ is a permutation and so {{afortiori}} a bijection.
It remains to show that $f$ is a homomorphism.
So, let $a, b \in S$ be arbitrary.
We have:
{{begin-eqn}}
{{eqn | l = \map f {a \gets b}
      | r = \map f a
      | c = {{Defof|Left Operation}}
}}
{{eqn | r = \map f a \gets \map f b
      | c = {{Defof|Left Operation}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Permutation of Set is Automorphism of Set under Right Operation

Let $S$ be a set.
Let $\struct {S, \to}$ be the algebraic structure formed from $S$ under the right operation.
Let $f$ be a permutation on $S$.
Then $f$ is an automorphism of $f$.

Proof:
We have {{hypothesis}} that $f$ is a permutation and so a fortiori a bijection.
It remains to show that $f$ is a homomorphism.
So, let $a, b \in S$ be arbitrary.
We have:
{{begin-eqn}}
{{eqn | l = \map f {a \to b}
      | r = \map f b
      | c = {{Defof|Right Operation}}
}}
{{eqn | r = \map f a \to \map f b
      | c = {{Defof|Right Operation}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Algebraic Structures formed by Left and Right Operations are not Isomorphic for Cardinality Greater than 1

Let $S$ be a set.
Let $\gets$ and $\to$ denote the left operation and right operation respectively.
Let $\card S > 1$.
The algebraic structures $\struct {S, \gets}$ and $\struct {S, \to}$ are not isomorphic.

Proof:
{{AimForCont}} there exists an isomorphism $\phi$ from $\struct {S, \gets}$ to $\struct {S, \to}$.
Because $\card S > 1$ we have that there exist at least $2$ distinct elements of $S$.
Let these be $x$ and $y$.
Hence:
{{begin-eqn}}
{{eqn | l = \map \phi {x \gets y}
      | r = \map \phi x
      | c = {{Defof|Left Operation}}
}}
{{eqn | r = \map \phi x \to \map \phi y
      | c = {{Defof|Isomorphism (Abstract Algebra)}}
}}
{{eqn | r = \map \phi y
      | c = {{Defof|Right Operation}}
}}
{{end-eqn}}
Hence $\map \phi x = \map \phi y$ and so $\phi$ is not an injection.
Hence $\phi$ is not a bijection and so not an isomorphism.
{{qed}}
Theorem: Induced Metric on Surface of Revolution/Corollary

Let $\struct {\R^3, d}$ be the Euclidean space.
Let $S_C \subseteq \R^3$ be the surface of revolution.
Let the smooth local parametrization of $C$ be:
:$\map \gamma t = \tuple {\map x t, \map y t}$
Let $\gamma$ be a unit-speed curve.
Then the induced metric on $S_C$ is:
:$g = d t^2 + \map y t^2 d \theta^2$

Proof:
By definition of the unit-speed curve:
:$\size {\map {\gamma'} t}_g = 1$
In our case we are working with the Euclidean space.
Hence:
:$\sqrt {\map {x'^2} t + \map {y'^2} t} = 1$
or:
:$ \map {x'^2} t + \map {y'^2} t = 1$
Substitution of this into the induced metric of $S_C$ yields the desired result.
{{qed}}
Theorem: Structure of Cardinality 3+ where Every Permutation is Automorphism is Idempotent

Let $S$ be a set whose cardinality is at least $3$.
Let $\struct {S, \circ}$ be an algebraic structure on $S$ such that every permutation on $S$ is an automorphism on $\struct {S, \circ}$.
Then $\circ$ is an idempotent operation.

Proof:
{{AimForCont}} $\circ$ is not idempotent.
Then there exists $x \in S$ such that:
:$\exists y \in S: x \circ x = y$
where $x \ne y$.
Because there are at least $3$ distinct elements of $S$ {{hypothesis}}:
:$\exists z \in S: z \ne x, z \ne y$
Let $f: S \to S$ be a permutation on $S$ such that:
:$\map f x = x$
:$\map f y = z$
We have:
{{begin-eqn}}
{{eqn | l = z
      | r = \map f y
      | c = Definition of $f$
}}
{{eqn | r = \map f {x \circ x}
      | c = {{hypothesis}}: $x \circ x = y$
}}
{{eqn | r = \map f x \circ \map f x
      | c = {{hypothesis}}: $f$ is an automorphism
}}
{{eqn | r = x \circ x
      | c = Definition of $f$
}}
{{eqn | r = y
      | c = {{hypothesis}}: $x \circ x = y$
}}
{{end-eqn}}
This contradicts our assertion that $x$ and $z$ are distinct.
From Proof by Contradiction it follows that our assumption that $\circ$ is not idempotent must have been false.
Hence $\circ$ is idempotent.
{{qed}}
Theorem: Operation on Structure of Cardinality 4+ where Every Permutation is Automorphism is Left or Right Operation

Let $S$ be a set whose cardinality is at least $4$.
Let $\struct {S, \circ}$ be an algebraic structure on $S$ such that every permutation on $S$ is an automorphism on $\struct {S, \circ}$.
Then $\circ$ is either the left operation or the right operation.

Proof:
From Structure of Cardinality 3+ where Every Permutation is Automorphism is Idempotent, we have that $\circ$ is idempotent:
:$\forall a \in S: a \circ a = a$
{{AimForCont}} $\circ$ is such that:
:$x \circ y = z$
for some distinct $x, y, z \in S$.
As $S$ has cardinality of at least $4$, there exists $w \in S$ such that $w \ne x$, $w \ne y$ and $w \ne z$.
Let $f$ be a permutation on $S$ such that:
:$\map f x = x$
:$\map f y = y$
:$\map f z = w$
Then:
{{begin-eqn}}
{{eqn | l = w
      | r = \map f z
      | c = Definition of $f$
}}
{{eqn | r = \map f {x \circ y}
      | c = {{hypothesis}}: $x \circ y = z$
}}
{{eqn | r = \map f x \circ \map f y
      | c = {{hypothesis}}: $f$ is an automorphism
}}
{{eqn | r = x \circ y
      | c = Definition of $f$
}}
{{eqn | r = z
      | c = {{hypothesis}}: $x \circ y = z$
}}
{{end-eqn}}
This contradicts our assertion that $w$ and $z$ are distinct.
Hence we have shown that:
:$\forall x, y \in S: x \circ y = x \lor x \circ y  = y$
{{qed|lemma}}
{{AimForCont}} $\circ$ is neither the left operation nor the right operation.
From the above, that means there exist $w, x, y, z \in S$ such that:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = x
}}
{{eqn | l = w \circ z
      | r = z
}}
{{end-eqn}}
Let $f$ be a permutation on $S$ such that:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = w
}}
{{eqn | l = \map f y
      | r = z
}}
{{eqn | l = \map f z
      | r = x
}}
{{eqn | l = \map f w
      | r = y
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = w
      | r = \map f x
      | c = Definition of $f$
}}
{{eqn | r = \map f {x \circ y}
      | c = {{hypothesis}}: $x \circ y = x$
}}
{{eqn | r = \map f x \circ \map f y
      | c = {{hypothesis}}: $f$ is an automorphism
}}
{{eqn | r = w \circ z
      | c = Definition of $f$
}}
{{eqn | r = z
      | c = {{hypothesis}}: $w \circ z = z$
}}
{{end-eqn}}
This contradicts our assertion that $w$ and $z$ are distinct.
Hence $\circ$ is either the left operation or the right operation.
{{qed}}
Theorem: Unit Sphere as Surface of Revolution

{{WIP|Resolving consistency issues with previous results}}
Let $\struct {\R^3, d}$ be the Euclidean space.
Let $S_C \subseteq \R^3$ be the surface of revolution.
Let $C$ be a semi-circle defined by $x^2 + y^2 = 1$ in the open upper half-plane.
Let the smooth local parametrization of $C$ be:
:$\map \gamma \phi = \tuple {\cos \phi, \sin \phi}$
where $\phi \in \openint 0 \pi$.
Then the induced metric on $S_C$ is:
:$g = \d \phi^2 + \sin^2 \phi \rd \theta^2$

Proof:
By Smooth Local Parametrization of Surface of Revolution, the smooth local parametrization of $S_C$ can be written as:
:$\map X {\phi, \theta} = \tuple {\sin \phi \cos \theta, \sin \phi \sin \theta, \cos \phi}$
By Induced Metric on Surface of Revolution:
{{begin-eqn}}
{{eqn | l = g
      | r = \paren {\paren {\cos' \phi}^2 + \paren {\sin' \phi}^2} \rd \phi^2 + \sin^2 \phi \rd \theta^2
}}
{{eqn | r = \paren {\sin^2 \phi + \cos^2 \phi} \rd \phi^2 + \sin^2 \phi \rd \theta^2
}}
{{eqn | r = \rd \phi^2 + \sin^2 \phi \rd \theta^2
}}
{{end-eqn}}
This is a metric of a unit sphere with the points on the $x$-axis removed.
{{qed}}
Theorem: Product Inverse Operation is Self-Inverse

:$\forall x \in G: x \oplus x = e$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \oplus x
      | r = x \circ x^{-1}
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = e
      | c = {{Group-axiom|3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Group Identity is Right Identity for Product Inverse Operation

:$\forall x \in G: x \oplus e = x$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \oplus e
      | r = x \circ e^{-1}
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = x \circ e
      | c = Inverse of Identity Element is Itself
}}
{{eqn | r = x
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Group Product Inverse Operation with Identity

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\oplus: G \times G \to G$ be the product inverse of $\circ$ on $G$.
Then:
:$\forall x, y \in G: e \oplus \paren {x \oplus y} = y \oplus x$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = e \oplus \paren {x \oplus y}
      | r = e \oplus \paren {x \circ y^{-1} }
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = e \circ \paren {x \circ y^{-1} }^{-1}
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = e \circ \paren {y \circ x^{-1} }
      | c = Inverse of Group Product
}}
{{eqn | r = e \circ \paren {y \oplus x}
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = y \oplus x
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Property of Product Inverse Operator

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\oplus: G \times G \to G$ be the product inverse of $\circ$ on $G$.
Then:
:$\forall x, y, z \in G: \paren {x \oplus z} \oplus \paren {y \oplus z} = x \oplus y$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x, y, z \in G
      | l = \paren {x \oplus z} \oplus \paren {y \oplus z}
      | r = \paren {x \circ z^{-1} } \oplus \paren {y \circ z^{-1} }
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = \paren {x \circ z^{-1} } \circ \paren {y \circ z^{-1} }^{-1}
      | c = {{Defof|Product Inverse Operation}}
}}
{{eqn | r = \paren {x \circ z^{-1} } \circ \paren {z \circ y^{-1} }
      | c = Inverse of Group Product
}}
{{eqn | r = x \circ \paren {z^{-1}  \circ z} \circ y^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = x \circ e \circ y^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = x \circ y^{-1}
      | c = {{Group-axiom|2}}
}}
{{eqn | r = x \oplus y
      | c = {{Defof|Product Inverse Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product Inverse Operation Properties induce Group

Let $\struct {G, \oplus}$ be a closed algebraic structure on which the following properties hold:
{{:Axiom:Product Inverse Operation Axioms}}
Let $\circ$ be the operation on $G$ defined as:
:$\forall x, y \in G: x \circ y = x \oplus \paren {e \oplus y}$
Then $\struct {G, \circ}$ is a group.

Proof:
Taking the group axioms in turn: