avewright/proofwiki-math huggingface dataset:
Theorem: Normal Subgroup induced by Congruence Relation defines that Congruence

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\RR$ be a congruence relation for $\circ$.
Let $\eqclass e \RR$ be the equivalence class of $e$ under $\RR$.
Let $N = \eqclass e \RR$ be the normal subgroup induced by $\RR$.
Then $\RR$ is the equivalence relation $\RR_N$ defined by $N$.

Proof:
Let $\RR_N$ be the equivalence defined by $N$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \RR
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \RR
      | r = \paren {x^{-1} \circ y}
      | c = $\RR$ is compatible with $\circ$
}}
{{eqn | ll= \leadsto
      | l = \paren {e \circ e}
      | o = \RR
      | r = \paren {x^{-1} \circ y}
      | c = Group properties
}}
{{eqn | ll= \leadsto
      | l = x^{-1} \circ y
      | o = \in
      | r = N
      | c = Definition of $N$
}}
{{end-eqn}}
But from Congruence Class Modulo Subgroup is Coset:
:$x \mathrel {\RR_N} y \iff x^{-1} \circ y \in N$
Thus:
:$\RR = \RR_N$
{{Qed}}
Theorem: Quotient Structure on Group defined by Congruence equals Quotient Group

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\RR$ be a congruence relation for $\circ$.
Let $\struct {G / \RR, \circ_\RR}$ be the quotient structure defined by $\RR$.
Let $N = \eqclass e \RR$ be the normal subgroup induced by $\RR$.
Let $\struct {G / N, \circ_N}$ be the quotient group of $G$ by $N$.
Then $\struct {G / \RR, \circ_\RR}$ is the subgroup $\struct {G / N, \circ_N}$ of the semigroup $\struct {\powerset G, \circ_\PP}$.

Proof:
Let $\eqclass x \RR \in G / \RR$.
By Congruence Relation on Group induces Normal Subgroup:
:$\eqclass x \RR = x N$
where $x N$ is the (left) coset of $N$ in $G$.
Similarly, let:
:$y N \in G / N$
Then from Normal Subgroup induced by Congruence Relation defines that Congruence:
:$y N = \eqclass x \RR$
where:
:$\eqclass x \RR$ is the equivalence class of $y$ under $\RR$
:$\RR$ is the equivalence relation defined by $N$.
Hence the result.
{{qed}}
Theorem: Vector Scaled by Zero is Zero Vector

Let $F$ be a field whose zero is $0_F$.
Let $\struct {\mathbf V, +, \ast}_F$ be a vector space over $F$, as defined by the vector space axioms.
Then:
:$\forall \mathbf v \in \mathbf V: 0_F \ast \mathbf v = \bszero$

Proof:
{{begin-eqn}}
{{eqn | l = 0_F \circ \mathbf v
      | r = \paren {0_F + 0_F} \ast  \mathbf v
      | c = {{Field-axiom|A3}}
}}
{{eqn | r = 0_F \ast \mathbf v + 0_F \ast \mathbf v
      | c = {{Vector-space-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = 0_F \ast \mathbf v + \paren {-0_F \ast \mathbf v}
      | r = \paren {0_F \ast \mathbf v + 0_F \ast \mathbf v} + \paren {-0_F \ast \mathbf v}
      | c = adding $-0_F \ast \mathbf v$ to both sides
}}
{{eqn | r = 0_F \ast \mathbf v + \paren {0_F \ast \mathbf v + \paren {-0_F \ast \mathbf v} }
      | c = {{Abelian-group-axiom|1||underlying}}
}}
{{eqn | ll= \leadsto
      | l = \bszero
      | r = 0_F \ast \mathbf v + \bszero
      | c = {{Abelian-group-axiom|3||underlying}}
}}
{{eqn | r = 0_F \ast \mathbf v
      | c = {{Abelian-group-axiom|2||underlying}}
}}
{{end-eqn}}
{{qed}}
Theorem: Zero Vector Scaled is Zero Vector

Let $\struct {\mathbf V, +, \ast}_K$ be a vector space over a division ring $K$, as defined by the vector space axioms.
Then:
:$\forall \lambda \in K: \lambda \ast \bszero = \bszero$
where $\bszero \in \mathbf V$ is the zero vector.

Proof:
{{begin-eqn}}
{{eqn | l = \lambda \ast \bszero
      | r = \lambda \ast \paren {\bszero + \bszero}
      | c = {{Abelian-group-axiom|2||underlying}}
}}
{{eqn | r = \lambda \ast \bszero + \lambda \ast \bszero
      | c = {{Vector-space-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = \lambda \ast \bszero + \paren {-\lambda \ast \bszero}
      | r = \paren {\lambda \ast \bszero + \lambda \ast \bszero} + \paren {-\lambda \ast \bszero}
      | c = adding $-\lambda \ast \bszero$ to both sides
}}
{{eqn | r = \lambda \ast \bszero + \paren {\lambda \ast \bszero + \paren {-\lambda \ast \bszero} }
      | c = {{Abelian-group-axiom|1||underlying}}
}}
{{eqn | ll= \leadsto
      | l = \bszero
      | r = \lambda \ast \bszero + \bszero
      | c = {{Abelian-group-axiom|3||underlying}}
}}
{{eqn | r = \lambda \ast \bszero
      | c = {{Abelian-group-axiom|2||underlying}}
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Product is Zero only if Factor is Zero

Let $F$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\struct {\mathbf V, +, \ast}_F$ be a vector space over $F$, as defined by the vector space axioms.
Then:
:$\forall \lambda \in F: \forall \mathbf v \in \mathbf V: \lambda \ast \mathbf v = \bszero \implies \paren {\lambda = 0_F \lor \mathbf v = \mathbf 0}$
where $\bszero \in \mathbf V$ is the zero vector.

Proof:
{{AimForCont}} that:
:$\exists \lambda \in F: \exists \mathbf v \in \mathbf V: \lambda \ast \mathbf v = \bszero \land \lambda \ne 0_F \land \mathbf v \ne \bszero$
which is the negation of the exposition of the theorem.
Utilizing the vector space axioms:
{{begin-eqn}}
{{eqn | l = \lambda \ast \mathbf v
      | r = \bszero
}}
{{eqn | ll= \leadsto
      | l = \lambda^{-1} \ast \paren {\lambda \ast \mathbf v}
      | r = \lambda^{-1} \ast \mathbf 0
      | c = multiplying both sides by $\lambda^{-1}$
}}
{{eqn | ll= \leadsto
      | l = \bszero
      | r = \lambda^{-1} \ast \paren {\lambda \ast \mathbf v}
      | c = Zero Vector Scaled is Zero Vector
}} 
{{eqn | r = \paren {\lambda^{-1} \cdot \lambda} \ast \mathbf v
      | c = {{Vector-space-axiom|3}}
}}
{{eqn | r = 1_F \ast \mathbf v
}}
{{eqn | r = \mathbf v
      | c = {{Vector-space-axiom|4}}
}}
{{end-eqn}}
which contradicts the assumption that $\mathbf v \ne \mathbf 0$.
{{qed}}
Theorem: Baire-Osgood Theorem

Let $X$ be a Baire space.
Let $Y$ be a metrizable topological space
Let $f: X \to Y$ be a mapping which is the pointwise limit of a sequence $\sequence {f_n}$ in $\map C {X, Y}$.
{{explain|$\map C {X, Y}$}}
Let $\map D f$ be the set of points where $f$ is discontinuous.
Then $\map D f$ is a meager subset of $X$.

Proof:
Let $d$ be a metric on $Y$ generating its topology.
Let $\map {\omega_f} x$ denote the oscillation of $f$ at $x$.
We have:
:$\ds \map D f = \bigcup_{n \mathop = 1}^\infty \set {x \in X: \map {\omega_f} x \ge \frac 1 n}$
which is a countable union of closed sets.
Since we have this expression for $\map D f$, the claim follows if we can prove that for all $\epsilon \in \R_{>0}$ the closed set:
:$F_\epsilon = \set {x \in X: \map {\omega_f} x \ge 5 \epsilon}$
is nowhere dense.
Let $\epsilon \in \R_{>0}$ be given and consider the sets:
:$\ds A_n = \bigcap_{i, j \mathop \ge n} \set {x \in X: \map d {\map {f_i} x, \map {f_j} x} \le \epsilon}$
which are closed because $d$ and the $f_i$ are continuous.
Because $\sequence {f_n}$ is pointwise convergent, it is pointwise Cauchy with respect to any metric generating the topology on $Y$, so $\ds \bigcup_{n \mathop = 1}^\infty A_n = X$.
Given a nonempty open $U \subseteq X$ we wish to show that $U \nsubseteq F_\epsilon$.
Consider the sequence $\sequence {A_n \cap U}$ of closed subsets of $U$.
The union of these is all of $U$.
As $U$ is an open subspace of a Baire space, it is a Baire space.
So one of the elements of $\sequence {A_n \cap U}$, say $A_k$, must have an interior point, so there is an open $V \subseteq A_k \cap U$.
Because $U$ is open in $X$, $V$ is open in $X$ as well.  
We will show that:
:$V \subseteq F_\epsilon^c = \set {x \in X: \map {\omega_f} x < 5 \epsilon}$
This will show that:
:$V \nsubseteq F_\epsilon$ and thus that $U \nsubseteq F_\epsilon$
Since $V \subseteq A_k$:
:$\map d {\map {f_i} x, \map {f_j} x} \le \epsilon$
for all $x \in V$ and all $i, j \ge k$.
Pointwise convergence of $\sequence {f_n}$ gives that:
:$\map d {\map f x, \map {f_k} x} \le \epsilon$
for all $x \in V$.
By continuity of $f_k$ we have for every $x_0 \in V$ an open $V_{x_0} \subseteq V$ such that:
:$\map d {\map {f_k} x, \map {f_k} {x_0} } \le \epsilon$
for all $x \in V_{x_0}$.
By the triangle inequality:
:$\map d {\map f x, \map {f_k} {x_0} } \le 2 \epsilon$ 
for all $x \in V_{x_0}$.
Applying the triangle inequality again:
:$\map d {\map f x, \map f y} \le 4 \epsilon$
for all $x, y \in V_{x_0}$.
Thus we have the bound:
:$\map {\omega_f} {x_0} \le \map {\omega_f} {V_{x_0} } \le  4 \epsilon$
showing that $x_0 \notin F_\epsilon$ as desired.
{{qed}}
{{Namedfor|René-Louis Baire|name2 = William Fogg Osgood|cat = Baire|cat2 = Osgood}}
Theorem: Null Ring is Ideal

Let $\struct {R, +, \circ}$ be a ring whose zero is $0_R$.
Then the null ring $\struct {\set {0_R}, +, \circ}$ is an ideal of $\struct {R, +, \circ}$.

Proof:
From Null Ring is Subring of Ring, $\struct {\set {0_R}, +, \circ}$ is a subring of $\struct {R, +, \circ}$.
Also, from Ring Product with Zero:
:$\forall x \in R: x \circ 0_R = 0_R = 0_R \circ x \in \set {0_R}$
thus fulfilling the condition for $\struct {\set {0_R}, +, \circ}$ to be an ideal of $\struct {R, +, \circ}$.
{{qed}}
Theorem: Ring Epimorphism Preserves Subrings

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring epimorphism.
Let $S$ be a subring of $R_1$.
Then $\phi \sqbrk S$ is a subring of $R_2$.

Proof:
A direct application of Ring Homomorphism Preserves Subrings.
{{qed}}
Theorem: Preimage of Image of Ideal under Ring Homomorphism

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring homomorphism.
Let $K = \map \ker \phi$, be the kernel of $\phi$. 
Let $J$ be an ideal of $R_1$.
Then:
:$\phi^{-1} \sqbrk {\phi \sqbrk J} = J + K$

Proof:
As an ideal is a subring, the result Preimage of Image of Subring under Ring Homomorphism applies directly.
{{Qed}}
Theorem: Image of Preimage of Ideal under Ring Epimorphism

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring epimorphism.
Let $S_2$ be an ideal of $R_2$.
Then:
:$\phi \sqbrk {\phi^{-1} \sqbrk {S_2} } = S_2$

Proof:
As an ideal is a subring, the result Image of Preimage of Subring under Ring Epimorphism applies directly.
{{Qed}}
Theorem: Vectors are Right Cancellable

Let $\struct {\mathbf V, +, \circ}$ be a vector space over $\GF$, as defined by the vector space axioms.
Then every $\mathbf v \in \struct {\mathbf V, +}$ is right cancellable:
:$\forall \mathbf a, \mathbf b, \mathbf c \in \mathbf V: \mathbf a + \mathbf c = \mathbf b + \mathbf c \implies \mathbf a = \mathbf b$

Proof:
Utilizing the vector space axioms:
{{begin-eqn}}
{{eqn | l = \mathbf a + \mathbf c
      | r = \mathbf b + \mathbf c
}}
{{eqn | ll= \leadsto
      | l = \paren {\mathbf a + \mathbf c} - \mathbf c
      | r = \paren {\mathbf b + \mathbf c} - \mathbf c
}}
{{eqn | ll= \leadsto
      | l = \mathbf a + \paren {\mathbf c - \mathbf c}
      | r = \mathbf b + \paren {\mathbf c - \mathbf c}
}}
{{eqn | ll= \leadsto
      | l = \mathbf a + \bszero
      | r = \mathbf b + \bszero
}}
{{eqn | ll= \leadsto
      | l = \mathbf a
      | r = \mathbf b
}}
{{end-eqn}}
{{qed}}
Theorem: Vectors are Left Cancellable

Let $\struct {\mathbf V, +, \circ}$ be a vector space over $\GF$, as defined by the vector space axioms.
Then every $\mathbf v \in \struct {\mathbf V, +}$ is left cancellable:
:$\forall \mathbf a, \mathbf b, \mathbf c \in \mathbf V: \mathbf c + \mathbf a = \mathbf c + \mathbf b \implies \mathbf a = \mathbf b$

Proof:
Utilizing the vector space axioms:
{{begin-eqn}}
{{eqn | l = \mathbf c + \mathbf a
      | r = \mathbf c + \mathbf b
}}
{{eqn | ll= \leadsto
      | l = \mathbf a + \mathbf c
      | r = \mathbf b + \mathbf c
}}
{{eqn | ll= \leadsto
      | l = \mathbf a
      | r = \mathbf b
      | c = Vectors are Right Cancellable
}}
{{end-eqn}}
{{qed}}
Category:Vector Algebra
eubmf55s3838csahz7b1zjjuzzqohny
Theorem: Zero Vector is Unique

Let $\struct {\mathbf V, +, \circ}_{\mathbb F}$ be a vector space over $\mathbb F$, as defined by the vector space axioms.
Then the zero vector in $\mathbf V$ is unique:
:$\exists! \mathbf 0 \in \mathbf V: \forall \mathbf x \in \mathbf V: \mathbf x + \mathbf 0 = \mathbf x$

Proof:
=== Proof of Existence ===
Follows from the vector space axioms.
{{qed|lemma}}
Theorem: Additive Inverse in Vector Space is Unique

Let $\struct {\mathbf V, +, \circ}_F$ be a vector space over a field $F$, as defined by the vector space axioms.
Then for every $\mathbf v \in \mathbf V$, the additive inverse of $\mathbf v$ is unique:
:$\forall \mathbf v \in \mathbf V: \exists! \paren {-\mathbf v} \in \mathbf V: \mathbf v + \paren {-\mathbf v} = \mathbf 0$

Proof:
=== Proof of Existence ===
Follows from the vector space axioms.
{{qed|lemma}}
Theorem: Vector Inverse is Negative Vector

Let $F$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\struct {\mathbf V, +, \ast}_F$ be a vector space over $F$, as defined by the vector space axioms.
Then:
:$\forall \mathbf v \in \mathbf V: -\mathbf v = -1_F \ast \mathbf v$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf v + \paren {-1_F \ast \mathbf v}
      | r = \paren {1_F \ast \mathbf v} + \paren {-1_F \ast \mathbf v}
      | c = {{Field-axiom|M3}}
}}
{{eqn | r = \paren {1_F + \paren {-1_F} } \ast \mathbf v
      | c = {{Vector-space-axiom|2}}
}}
{{eqn | r = 0_F \ast \mathbf v
      | c = {{Field-axiom|A4}}
}}
{{eqn | r = \mathbf 0
      | c = Vector Scaled by Zero is Zero Vector
}}
{{end-eqn}}
so $-1_F \ast \mathbf v$ is an additive inverse of $\mathbf v$.
From Additive Inverse in Vector Space is Unique:
:$-1_F \ast \mathbf v = -\mathbf v$
{{qed}}
Theorem: Non-Trivial Commutative Division Ring is Field

Let $\struct {R, +, \circ}$ be a non-trivial division ring such that $\circ$ is commutative.
Then $\struct {R, +, \circ}$ is a field.
Similarly, let $\struct {F, +, \circ}$ be a field.
Then $\struct {F, +, \circ}$ is a non-trivial  division ring such that $\circ$ is commutative.

Proof:
Suppose $\struct {R, +, \circ}$ is a non-trivial division ring such that $\circ$ is commutative.
By definition $\struct {R, +}$ is an abelian group.
Thus {{Field-axiom|A}} are satisfied.
Also by definition, $\struct {R, \circ}$ is a semigroup such that $\circ$ is commutative.
Thus {{Field-axiom|M0}} to {{Field-axiom|M2}} are satisfied.
As $\struct {R, +, \circ}$ is a ring with unity, {{Field-axiom|M3}} is satisfied.
{{Field-axiom|D}} is satisfied by dint of $\struct {R, +, \circ}$ being a ring.
Finally note that by definition of division ring, {{Field-axiom|M4}} is satisfied.
Thus all the field axioms are satisfied, and so $\struct {R, +, \circ}$ is a field.
{{qed|lemma}}
Suppose $\struct {F, +, \circ}$ is a field.
Then by definition $\struct {F, +, \circ}$ is a non-trivial division ring such that $\circ$ is commutative.
{{qed}}
Theorem: Division Ring has No Proper Zero Divisors

Let $\struct {R, +, \circ}$ be a division ring.
Then $\struct {R, +, \circ}$ has no proper zero divisors.

Proof:
Let $\struct {R, +, \circ}$ be a division ring whose zero is $0_R$ and whose unity is $1_R$.
By definition of division ring, every element $x$ of $R^* = R \setminus \set {0_R}$ has an element $y$ such that:
:$y \circ x = x \circ y = 1_R$
That is, by definition, every element of $R^*$ is a unit of $R$.
The result follows from Unit of Ring is not Zero Divisor.
{{qed}}
Theorem: Maximal Element need not be Greatest Element

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $M \in S$ be a maximal element of $S$.
Then $M$ is not necessarily the greatest element of $S$.

Proof:
Proof by Counterexample:
Let $S = \set {a, b, c}$.
Let $\preccurlyeq$ be defined as:
:$x \preccurlyeq y \iff \tuple {x, y} \in \set {\tuple {a, a}, \tuple {b, b}, \tuple {c, c}, \tuple {a, b}, \tuple {a, c} }$
A straightforward but laborious process determines that $\preccurlyeq$ is a partial ordering on $S$.
We have that:
:$c \preccurlyeq x \implies c = x$
and:
:$b \preccurlyeq x \implies b = x$
and so by definition, both $b$ and $c$ are maximal elements of $S$.
Suppose $b$ is the greatest element of $S$.
Then from Greatest Element is Unique it follows that $c$ can not be the greatest element of $S$.
Hence the result.
In fact, from the definition of the greatest element of $S$:
:$x$ is the greatest element of $S$ {{iff}} $\forall y \in S: y \preccurlyeq x$
it can be seen directly that neither $b$ nor $c$ is the greatest element of $S$.
{{qed}}
Theorem: Maximal Ideal of Division Ring

Let $\struct {D, +, \circ}$ be a Division Ring whose zero is $0$.
Let $\struct {J, +, \circ}$ be a maximal ideal of $D$.
Then:
:$J = \set 0$

Proof:
From Ideals of Division Ring, the only ideals of a Division Ring $\struct {D, +, \circ}$ are $\struct {D, +, \circ}$ and $\struct {\set 0, +, \circ}$.
Hence the result by definition of maximal ideal.
{{qed}}
Theorem: Linear Transformation is Injective iff Kernel Contains Only Zero

Let $\mathbf V, \mathbf V'$ be vector spaces, with respective zeroes $\mathbf 0, \mathbf 0'$.
Let $T: \mathbf V \to \mathbf V'$ be a linear transformation.
Then:
:$T$ is injective {{iff}} $\map \ker T = \set {\mathbf 0}$
where:
:$\mathbf 0$ is the zero of the domain of $T$
:$\map \ker T$ is the kernel of $T$.

Proof:
=== Sufficient Condition ===
That $\mathbf 0 \in \map \ker T$ follows from Kernel of Linear Transformation contains Zero Vector.
That $\map \ker T$ is a singleton follows from the definition of injection.
{{qed|lemma}}
Theorem: Diagonal Relation on Ring is Ordering Compatible with Ring Structure

Let $\struct {R, +, \circ, \preceq}$ be a ring whose zero is $0_R$.
Then the diagonal relation $\Delta_R$ on $R$ is an ordering compatible with the ring structure of $R$.

Proof:
From Diagonal Relation is Ordering and Equivalence, we have that $\Delta_R$ is actually an ordering on $R$.
From the definition of the diagonal relation:
:$\tuple {x, y} \in \Delta_R \iff x = y$
Thus:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + z
      | r = y + z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x + z, y + z}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z + x
      | r = z + y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {z + x, z + y}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{end-eqn}}
So $\Delta_R$ is compatible with $+$.
Then note that:
{{begin-eqn}}
{{eqn | l = \tuple {0_R, x}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{eqn | lo= \land
      | l = \tuple {0_R, y}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0_R
      | r = x
      | c = 
}}
{{eqn | lo= \land
      | l = 0_R
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0_R
      | r = x \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {0_R, x \circ y}
      | o = \in
      | r = \Delta_R
      | c = 
}}
{{end-eqn}}
Hence the result, from the definition of an ordering compatible with the ring structure of $R$.
{{qed}}
Theorem: Nagata-Smirnov Metrization Theorem

A topological space $T = \struct {S, \tau}$ is metrizable {{iff}} $T$ is regular and has a basis that is $\sigma$-locally finite.

Proof:
=== Necessary Condition ===
Let $T$ be metrizable.
{{:Nagata-Smirnov Metrization Theorem/Necessary Condition}}{{qed|lemma}}
Theorem: Smirnov Metrization Theorem

Let $T = \struct {S, \tau}$ be a topological space.
Then:
:$T$ is metrizable {{iff}} $T$ is paracompact and locally metrizable.

Proof:
{{proof wanted}}
{{Namedfor|Yurii Mikhailovich Smirnov|cat = Smirnov Y M}}
Theorem: Identity Mapping is Automorphism/Semigroups

Let $\struct {S, \circ}$ be a semigroup.
Then $I_S: \struct {S, \circ} \to \struct {S, \circ}$ is a semigroup automorphism.

Proof:
The main result Identity Mapping is Automorphism holds directly.
{{qed}}
Category:Semigroup Automorphisms
Category:Identity Mappings
7spug7di6v6w2vjjaft8wwmd7e58u1f
Theorem: Identity Mapping is Ordered Ring Automorphism

Let $\struct {S, +, \circ, \preceq}$ be an ordered ring.
Then the identity mapping $I_S: S \to S$ is an ordered ring automorphism.

Proof:
We have that:
:an identity mapping is an order isomorphism
:an identity mapping is a group automorphism
:an identity mapping is a semigroup automorphism
Hence the result by definition of ordered ring automorphism.
{{qed}}
Theorem: Inverse of Reflexive Relation is Reflexive

Let $\RR$ be a relation on a set $S$.
If $\RR$ is reflexive, then so is $\RR^{-1}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x}
      | o = \in
      | r = \RR
      | c = {{Defof|Reflexive Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x}
      | o = \in
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Hence the result by definition of reflexive relation.
{{qed}}
Theorem: Inverse of Antireflexive Relation is Antireflexive

Let $\RR$ be a relation on a set $S$.
If $\RR$ is antireflexive, then so is $\RR^{-1}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x}
      | o = \notin
      | r = \RR
      | c = {{Defof|Antireflexive Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x}
      | o = \notin
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Hence the result by definition of antireflexive relation.
{{qed}}
Theorem: Inverse of Non-Reflexive Relation is Non-Reflexive

Let $\RR$ be a relation on a set $S$.
If $\RR$ is non-reflexive, then so is $\RR^{-1}$.

Proof:
Let $\RR$ be non-reflexive.
Then:
{{begin-eqn}}
{{eqn | q = \exists x \in S
      | l = \tuple {x, x}
      | o = \in
      | r = \RR
      | c = as $\RR$ is not antireflexive
}}
{{eqn | ll= \leadsto
      | q = \exists x \in S
      | l = \tuple {x, x}
      | o = \in
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Thus $\RR^{-1}$ is not antireflexive.
Also:
{{begin-eqn}}
{{eqn | q = \exists x \in S
      | l = \tuple {x, x}
      | o = \notin
      | r = \RR
      | c = as $\RR$ is not reflexive
}}
{{eqn | ll= \leadsto
      | q = \exists x \in S
      | l = \tuple {x, x}
      | o = \notin
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Thus $\RR^{-1}$ is not reflexive.
Hence the result, by definition of non-reflexive relation.
{{qed}}
Theorem: Inverse of Symmetric Relation is Symmetric

Let $\RR$ be a relation on a set $S$.
If $\RR$ is symmetric, then so is $\RR^{-1}$.

Proof:
Let $\RR$ be symmetric.
Then from Relation equals Inverse iff Symmetric it follows that $\RR^{-1}$ is also symmetric.
{{qed}}
Theorem: Inverse of Asymmetric Relation is Asymmetric

Let $\RR$ be a relation on a set $S$.
If $\RR$ is asymmetric, then so is $\RR^{-1}$.

Proof:
Let $\RR$ be asymmetric.
Let $\tuple {x, y} \in \RR^{-1}$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \RR^{-1}
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, x}
      | o = \in
      | r = \RR
      | c = Inverse of Inverse Relation
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \notin
      | r = \RR
      | c = {{Defof|Asymmetric Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, x}
      | o = \notin
      | r = \RR^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Thus it follows that $\RR^{-1}$ is also asymmetric.
{{qed}}
Theorem: Inverse of Antisymmetric Relation is Antisymmetric

Let $\RR$ be a relation on a set $S$.
If $\RR$ is antisymmetric, then so is $\RR^{-1}$.

Proof:
Let $\RR$ be antisymmetric.
Then:
:$\tuple {x, y} \land \tuple {y, x} \in \RR \implies x = y$
It follows that:
:$\tuple {y, x} \land \tuple {x, y} \in \RR^{-1} \implies x = y$
Thus it follows that $\RR^{-1}$ is also antisymmetric.
{{qed}}
Theorem: Inverse of Non-Symmetric Relation is Non-Symmetric

Let $\RR$ be a relation on a set $S$.
If $\RR$ is non-symmetric, then so is $\RR^{-1}$.

Proof:
Let $\RR$ be non-symmetric.
Then:
:$\exists \tuple {x_1, y_1} \in \RR \implies \tuple {y_1, x_1} \in \RR$
and also:
:$\exists \tuple {x_2, y_2} \in \RR \implies \tuple {y_2, x_2} \notin \RR$
Thus:
:$\exists \tuple {y_1, x_1} \in \RR^{-1} \implies \tuple {x_1, y_1} \in \RR^{-1}$
and also:
:$\exists \tuple {y_2, x_2} \in \RR^{-1} \implies \tuple {x_2, y_2} \notin \RR^{-1}$
and so $\RR^{-1}$ is non-symmetric.
{{qed}}