avewright/proofwiki-math huggingface dataset:
Theorem: B-Algebra Power Law with Zero

:$\forall x \in X: n, m \in \N_{>0} \implies x^m \circ x^n = 0 \circ x^{n - m}$

Proof:
First we show that:
:$\forall x \in X: x \circ x^2 = 0 \circ x$
{{begin-eqn}}
{{eqn | l = x \circ x^2
      | r = x \circ \paren {x^1 \circ \paren {0 \circ x} }
      | c = {{Defof|Power (B-Algebra)|Power ($B$-Algebra)}}
}}
{{eqn | r = x \circ \paren {x \circ \paren {0 \circ x} }
      | c = First Power of Element in $B$-Algebra
}}
{{eqn | r = \paren {x \circ x} \circ x
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = 0 \circ x
      | c = {{B-algebra-axiom|1}}
}}
{{end-eqn}}
{{qed|lemma}}
Now we show that:
:$\forall x \in X: m \in \N_{>0}: x \circ x^m = 0 \circ x^{m - 1}$
{{begin-eqn}}
{{eqn | l = x \circ x^m
      | r = x \circ \paren {x^{m - 1} \circ \paren {0 \circ x} }
      | c = {{Defof|Power (B-Algebra)|Power ($B$-Algebra)}}
}}
{{eqn | r = \paren {x \circ x} \circ x^{m - 1}
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = 0 \circ x^{m - 1}
      | c = {{B-algebra-axiom|1}}
}}
{{end-eqn}}
{{qed|lemma}}
Now we prove the original proposition using a proof by induction.
The base case for $n = 1, m = 2$ was established in the first lemma. 
Let us assume $x^m \circ x^n = 0 \circ x^{n - m}$ for some $n, m \in \N_{>0}$.
Then: 
{{begin-eqn}}
{{eqn | l = x^{m + 1} \circ x^n
      | r = \paren {x^m \circ \paren {0 \circ x} } \circ x^n
      | c = {{Defof|Power (B-Algebra)|Power ($B$-Algebra)}}
}}
{{eqn | r = x^m \circ \paren {x^n \circ x}
      | c = Identity: $x \circ \paren {y \circ z} = \paren {x \circ \paren {0 \circ z} } \circ y$
}}
{{eqn | r = x^m \circ x^{n - 1}
      | c = $B$-Algebra Power Law
}}
{{eqn | r = x^0 \circ x^{n - m - 1}
      | c = Induction using the previous lemma
}}
{{eqn | r = 0 \circ x^{n - m - 1}
      | c = {{Defof|Power (B-Algebra)|Zeroth Power of Element}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:B-Algebras
r7jwmdj3egp1pkvx946zg21nat53jgw
Theorem: Product of Powers in B-Algebra

Let $\struct {X, \circ}$ be a $B$-algebra.
Let $x \in X$ and $m, n \in \N$.
Then:
:$x^m \circ x^n = \begin {cases}
x^{m - n} & : m \ge n \\
0 \circ x^{n - m} & : n > m
\end {cases}$

Proof:
For $m \ge n$ the result follows from $B$-Algebra Power Law.
For $n > m$ the result follows from $B$-Algebra Power Law with Zero.
{{qed}}
Category:B-Algebras
80evozxwp6k58y1u28pq15t2boz2ulb
Theorem: Superset of Co-Countable Set

Every superset of a co-countable set is co-countable.

Proof:
Let $S$ be a set.
Let $A$ be co-countable in $S$, and let $B$ be such that $A \subseteq B \subseteq S$.
From Relative Complement inverts Subsets, it follows that:
:$\complement_S \left({B}\right) \subseteq \complement_S \left({A}\right)$
As $A$ is co-countable, $\complement_S \left({A}\right)$ is countable.
By Subset of Countably Infinite Set is Countable, it follows that $\complement_S \left({B}\right)$ is also countable.
Therefore, $B$ is also co-countable, and the result follows.
{{qed}}
Theorem: Group Induces B-Algebra

Let $\struct {G, \circ}$ be a group whose identity element is $e$.
Let $*$ be the product inverse operation on $G$:
:$\forall a, b \in G: a * b = a \circ b^{-1}$
where $b^{-1}$ is the inverse element of $b$ under the operation $\circ$.
Then the algebraic structure $\struct {G, *}$ is a $B$-algebra.

Proof:
First note that by {{Group-axiom|0}}:
:$\forall a, b \in G: a * b \in G$
and so {{B-algebra-axiom|C}} holds.
We have that:
:$\forall x \in G: x * x = x \circ x^{-1} = e$
by definition of inverse element.
Let $0 := e$.
Then:
:{{B-algebra-axiom|0}}: $\quad \exists 0 \in G$
:{{B-algebra-axiom|1}}: $\quad \forall x \in G: x * x = 0$
Note that:
{{begin-eqn}}
{{eqn | q = \exists 0 \in G
      | l = 0^{-1}
      | r = e^{-1}
      | c = Definition of $0$
}}
{{eqn | r = e
      | c = Inverse of Identity Element is Itself
}}
{{eqn | r = 0
      | c = Definition of $0$
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x * 0
      | r = x \circ 0^{-1}
      | c = Definition of $*$
}}
{{eqn | r = x \circ e
      | c = Definition of $0$
}}
{{eqn | r = x
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
demonstrating:
:{{B-algebra-axiom|2}}: $\quad \forall x \in G: x * 0 = x$
Finally, let $x, y, z \in G$:
{{begin-eqn}}
{{eqn | l = \paren {x * y} * z
      | r = \paren {x \circ y^{-1} } \circ z^{-1}
      | c = Definition of $*$
}}
{{eqn | r = x \circ \paren {y^{-1} \circ z^{-1} }
      | c = {{Group-axiom|1}}
}}
{{eqn | r = x \circ \paren {z \circ y}^{-1}
      | c = Inverse of Group Product
}}
{{eqn | r = x \circ \paren {z \circ \paren {y^{-1} }^{-1} }^{-1}
      | c = Inverse of Group Inverse
}}
{{eqn | r = x * \paren {z * y^{-1} }
      | c = Definition of $*$
}}
{{eqn | r = x * \paren {z * \paren {0 \circ y^{-1} } }
      | c = as $0 = e$
}}
{{eqn | r = x * \paren {z * \paren {0 * y} }
      | c = Definition of $*$
}}
{{end-eqn}}
This demonstrates:
:{{B-algebra-axiom|3}}: $\quad \forall x, y, z \in G: \paren {x * y} * z = x * \paren {z * \paren {0 * y} }$
All axioms of the $B$-algebra have been demonstrated to hold.
Hence the result.
{{qed}}
Category:B-Algebras
Category:Group Theory
4cwou0a0u30ux1262gaxrknp36ynh0z
Theorem: Abelian Group Induces Commutative B-Algebra

Let $\struct {G, \circ}$ be an abelian group whose identity element is $e$.
Let $*$ be the product inverse operation on $G$:
:$\forall a, b \in G: a * b = a \circ b^{-1}$
where $b^{-1}$ is the inverse element of $b$ under the operation $\circ$.
Then the algebraic structure $\struct {G, *}$ is a commutative $B$-algebra.
That is:
:$\forall a, b \in G: a * \paren {0 * b} = b * \paren {0 * a}$

Proof:
From Group Induces $B$-Algebra, $\struct {G, *}$ is a $B$-Algebra.
As in the proof Group Induces $B$-Algebra, we let:
:$0 := e$
Now we demonstrate $0$-commutativity.
Let $x, y \in G$:
{{begin-eqn}}
{{eqn | l = x * \paren {0 * y}
      | r = x \circ \paren {e \circ y^{-1} }^{-1} 
      | c = Definition of $*$ and $0$
}}
{{eqn | r = x \circ \paren {y^{-1} }^{-1}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = x \circ y
      | c = Inverse of Group Inverse
}}
{{eqn | r = y \circ x
      | c = {{Defof|Abelian Group}}
}}
{{eqn | r = y \circ \paren {x^{-1} }^{-1}
      | c = Inverse of Group Inverse
}}
{{eqn | r = y \circ \paren {e \circ x^{-1} }^{-1}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = y * \paren {0 * x}
      | c = Definition of $*$ and $0$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:B-Algebras
Category:Abelian Groups
e267mdxnc9hjrc714emjg4amjxrdem2
Theorem: Identity of Cardinal Product is One

Let $\mathbf a$ be a cardinal.
Then:
: $\bsone \mathbf a = \mathbf a$
where $\bsone \mathbf a$ denotes the product of the (cardinal) one and $\mathbf a$.
That is, $\bsone$ is the identity element of the product operation on cardinals.

Proof:
Let $\mathbf a = \card A$ for some set $A$.
From the definition of (cardinal) one, $\bsone$ is the cardinal associated with a singleton set, say, $\set \O$.
We have by definition of product of cardinals that $\bsone \mathbf a$ is the cardinal associated with $\set \O \times A$.
Consider the mapping $f: \set \O \times A \to A$ defined as:
:$\forall a \in A: \map f {\O, a} = a$
Let $a_1, a_2 \in A$ such that:
:$\map f {\O, a_1} = \map f {\O, a_2}$
Then:
{{begin-eqn}}
{{eqn | l = \map f {\O, a_1}
      | r = \map f {\O, a_2}
}}
{{eqn | ll= \leadsto
      | l = a_1
      | r = a_2
      | c = Definition of $f$
}}
{{eqn | ll= \leadsto
      | l = \tuple {\O, a_1}
      | r = \tuple {\O, a_2}
      | c = Equality of Ordered Pairs
}}
{{end-eqn}}
Thus $f$ is an injection.
Let $a \in A$.
By definition of $f$:
:$a = \map f {\O, a}$
Thus $f$ is a surjection.
So $f$ is both an injection and a surjection, and so by definition a bijection.
Thus a bijection has been established between $\set \O \times A$ and $A$.
It follows by definition that $\set \O \times A$ and $A$ are equivalent.
The result follows by definition of cardinal.
{{qed}}
Theorem: Zero of Cardinal Product is Zero

Let $\mathbf a$ be a cardinal.
Then:
: $\mathbf 0 \mathbf a = \mathbf 0$
where $\mathbf 0 \mathbf a$ denotes the product of the (cardinal) zero and $\mathbf a$.
That is, $\mathbf 0$ is the zero element of the product operation on cardinals.

Proof:
Let $\mathbf a = \card A$ for some set $A$.
From the definition of (cardinal) zero, $\mathbf 0$ is the cardinal associated with the empty set $\O$.
We have by definition of product of cardinals that $\mathbf 0 \mathbf a$ is the cardinal associated with $\O \times A$.
But from Cartesian Product is Empty iff Factor is Empty:
:$\O \times A = \O$
Hence the result.
{{qed}}
Theorem: Sum of Cardinals is Commutative

Let $\mathbf a$ and $\mathbf b$ be cardinals.
Then:
:$\mathbf a + \mathbf b = \mathbf b + \mathbf a$
where $\mathbf a + \mathbf b$ denotes the sum of $\mathbf a$ and $\mathbf b$.

Proof:
Let $\mathbf a = \map \Card A$ and $\mathbf b = \map \Card B$ for some sets $A$ and $B$ such that $A \cap B = \O$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf a + \mathbf b
      | r = \map \Card {A \cup B}
      | c = {{Defof|Sum of Cardinals}}
}}
{{eqn | r = \map \Card {B \cup A}
      | c = Union is Commutative
}}
{{eqn | r = \mathbf b + \mathbf a
      | c = {{Defof|Sum of Cardinals}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cardinals is Associative

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be cardinals.
Then:
: $\mathbf a + \paren {\mathbf b + \mathbf c} = \paren {\mathbf a + \mathbf b} + \mathbf c$
where $\mathbf a + \mathbf b$ denotes the sum of $\mathbf a$ and $\mathbf b$.

Proof:
Let $\mathbf a = \card A, \mathbf b = \card B$ and $\mathbf c = \card C$ for some sets $A$, $B$ and $C$.
Let $A, B, C$ be pairwise disjoint, that is:
:$A \cap B = \O$
:$B \cap C = \O$
:$A \cap C = \O$
Then we can define:
:$A \sqcup B := A \cup B$
:$B \sqcup C := B \cup C$
:$A \sqcup C := A \cup C$
where $A \sqcup B$ denotes the disjoint union of $A$ and $B$.
Then we have:
:$\mathbf a + \mathbf b = \card {A \sqcup B} = \card {A \cup B}$
:$\mathbf b + \mathbf c = \card {B \sqcup C} = \card {B \cup C}$
Then:
{{begin-eqn}}
{{eqn | l=\paren {A \cup B} \cap C
      | r=\paren {A \cap C} \cup \paren {B \cap C}
      | c=Intersection Distributes over Union
}}
{{eqn | r=\O \cup \O
      | c=as $A \cap C = \O$ and $B \cap C = \O$
}}
{{eqn | r=\O
      | c=Union with Empty Set
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l=\card {\paren {A \cup B} \cup C}
      | r=\card {A \cup B} + \card C
      | c=as $\paren {A \cup B} \cap C = \O$ from above
}}
{{eqn | r=\paren {\mathbf a + \mathbf b} + \mathbf c
      | c={{Defof|Sum of Cardinals}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l=A \cap \paren {B \cup C}
      | r=\paren {A \cap B} \cup \paren {A \cap C}
      | c=Intersection Distributes over Union
}}
{{eqn | r=\O \cup \O
      | c=as $A \cap B = \O$ and $A \cap C = \O$
}}
{{eqn | r=\O
      | c=Union with Empty Set
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l=\card {A \cup \paren {B \cup C} }
      | r=\card A + \card {B \cup C}
      | c=as $A \cap \paren {B \cup C} = \O$ from above
}}
{{eqn | r=\mathbf a + \paren {\mathbf b + \mathbf c}
      | c={{Defof|Sum of Cardinals}}
}}
{{end-eqn}}
Finally note that from Union is Associative:
:$A \cup \paren {B \cup C} = \paren {A \cup B} \cup C$
{{qed}}
Theorem: B-Algebra is Commutative iff x(xy)=y

Let $\struct {X, \circ}$ be a $B$-algebra.
Then $\struct {X, \circ}$ is commutative {{iff}}:
:$\forall x, y \in X: x \circ \paren {x \circ y} = y$

Proof:
=== Necessary Condition ===
Let $x, y \in X$:
{{begin-eqn}}
{{eqn | l = x \circ \paren {x \circ y}
      | r = \paren {x \circ \paren {0 \circ y} } \circ x
      | c = Identity: $x \circ \paren {y \circ z} = \paren {x \circ \paren {0 \circ z} }  \circ y$
}}
{{eqn | r = \paren {y \circ \paren {0 \circ x} } \circ x
      | c = $\struct {X, \circ}$ is commutative
}}
{{eqn | r = y \circ \paren {x \circ x}
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = y \circ 0
      | c = {{B-algebra-axiom|1}}
}}
{{eqn | r = y
      | c = {{B-algebra-axiom|2}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Identity of Cardinal Sum is Zero

Let $\mathbf a$ be a cardinal.
Then:
: $\mathbf a + \mathbf 0 = \mathbf a$
where $\mathbf a + \mathbf 0$ denotes the sum of the zero cardinal and $\mathbf a$.
That is, $\mathbf 0$ is the identity element of the sum operation on cardinals.

Proof:
Let $\mathbf a = \card A$ for some set $A$.
From Union with Empty Set we have $A \cup \O = A$.
From Intersection with Empty Set we have $A \cap \O = \O$.
So $A$ and $\O$ are disjoint and so:
{{begin-eqn}}
{{eqn | l=\mathbf a + \mathbf 0
      | r=\card {A \cup \O}
      | c={{Defof|Sum of Cardinals}}
}}
{{eqn | r=\card A + \card \O
      | c=Cardinality of Set Union/Corollary
}}
{{eqn | r=\card A
      | c=Cardinality of Empty Set
}}
{{eqn | r=\mathbf a
      | c=
}}
{{end-eqn}}
{{qed}}
Theorem: Commutative B-Algebra Implies (zy)(zx)=xy

Let $\struct {B, \circ}$ be a commutative $B$-algebra. 
Then:
:$\forall x, y, z \in X: \paren {z \circ y} \circ \paren {z \circ x} = x \circ y$

Proof:
Let $x, y, z \in X$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {z \circ y} \circ \paren {z \circ x}
      | r = \paren {\paren {z \circ y} \circ \paren {0 \circ x} } \circ z
      | c = Identity: $x \circ \paren {y \circ z} = \paren {x \circ \paren {0 \circ z} } \circ y$
}}
{{eqn | r = \paren {x \circ \paren {0 \circ \paren {z \circ y} } } \circ z
      | c = {{Defof|Commutative B-Algebra|Commutative $B$-Algebra}}
}}
{{eqn | r = x \circ \paren {z \circ \paren {0 \circ \paren {0 \circ \paren {z \circ y} } } }
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = x \circ \paren {z \circ \paren {z \circ y} }
      | c = Identity: $x \circ y = x \circ \paren {0 \circ \paren {0 \circ y} }$ 
}}
{{eqn | r = x \circ y
      | c = $B$-Algebra is Commutative iff $x \circ \paren {x \circ y} = y$
}}
{{end-eqn}}
{{qed}}
Category:B-Algebras
11vqlot4f87wcqmp619co91axvgiddf
Theorem: Cardinal Product Distributes over Cardinal Sum

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be cardinals.
Then:
: $\mathbf a \paren {\mathbf b + \mathbf c} = \mathbf a \mathbf b + \mathbf a \mathbf c$
where:
: $\mathbf a + \mathbf b$ denotes the sum of $\mathbf a$ and $\mathbf b$.
: $\mathbf a \mathbf b$ denotes the product of $\mathbf a$ and $\mathbf b$.

Proof:
Let $\mathbf a = \card A$, $\mathbf b = \card B$ and $\mathbf c = \card C$ for some sets $A$, $B$ and $C$.
Let $B$ and $C$ be pairwise disjoint, that is:
:$B \cap C = \O$
Then we can define:
:$B \sqcup C := B \cup C$
where $B \sqcup C$ denotes the disjoint union of $B$ and $C$.
Then we have:
:$\mathbf b + \mathbf c = \card {B \sqcup C} = \card {B \cup C}$
Then:
{{begin-eqn}}
{{eqn | l=\paren {A \times B} \cap \paren {A \times C}
      | r=A \times \paren {B \cap C}
      | c=Cartesian Product of Intersections/Corollary 1
}}
{{eqn | r=A \times \O
      | c=as $B \cap C = \O$
}}
{{eqn | r=\O
      | c=Cartesian Product is Empty iff Factor is Empty
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l=\card {\paren {A \times B} \cup \paren {A \times C} }
      | r=\card {A \times B} + \card {A \times C}
      | c=as $A \times B$ and $A \times C$ are disjoint from above
}}
{{eqn | r=\mathbf a \mathbf b + \mathbf a \mathbf c
      | c={{Defof|Product of Cardinals}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l=\card {\paren {A \times B} \cup \paren {A \times C} }
      | r=\card {A \times \paren {B \cup C} }
      | c=Cartesian Product Distributes over Union
}}
{{eqn | r=\mathbf a \paren {\mathbf b + \mathbf c}
      | c={{Defof|Product of Cardinals}} and {{Defof|Sum of Cardinals}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ordering of Cardinals Compatible with Cardinal Product

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be cardinals.
Then:
:$\mathbf a \le \mathbf b \implies \mathbf a \mathbf c \le \mathbf b \mathbf c$
where $\mathbf a \mathbf c$ denotes the product of $\mathbf a$ and $\mathbf c$.

Proof:
Let $\mathbf a = \map \Card A$, $\mathbf b = \map \Card B$ and $\mathbf c = \map \Card C$ for some sets $A$, $B$ and $C$.
Let $\mathbf a \le \mathbf b$.
Then by definition of cardinal, there exists an injection $f: A \to B$.
Then the mapping $g: A \times C \to B \times C$ defined as:
:$\forall \tuple {a, c} \in A \times C: \map g {a, c} = \tuple {\map f a, c}$
Let $\tuple {a_1, c_1} \in A \times C$ and $\tuple {a_2, c_2} \in A \times C$ such that:
:$\map g {a_1, c_1} = \map g {a_2, c_2}$
That is:
:$\tuple {\map f {a_1}, c_1} = \tuple {\map f {a_2}, c_2}$
By Equality of Ordered Pairs:
:$\map f {a_1} = \map f {a_2}, c_1 = c_2$
and so as $f$ is an injection:
:$a_1 = a_2, c_1 = c_2$
By Equality of Ordered Pairs:
:$\tuple {a_1, c_1} = \tuple {a_2, c_2}$
demonstrating that $g$ is an injection.
So, by definition of product of cardinals:
:$\mathbf a \mathbf c \le \mathbf b \mathbf c$
{{qed}}
Theorem: Ordering of Cardinals Compatible with Cardinal Sum

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be cardinals.
Then:
:$\mathbf a \le \mathbf b \implies \mathbf a + \mathbf c \le \mathbf b + \mathbf c$
where $\mathbf a \mathbf c$ denotes the sum of $\mathbf a$ and $\mathbf c$.

Proof:
Let $\mathbf a = \map \Card A$, $\mathbf b = \map \Card B$ and $\mathbf c = \map \Card C$ for some sets $A$, $B$ and $C$.
Let $C$ be chosen such that $A \cap C = \O = B \cap C$.
Let $\mathbf a \le \mathbf b$.
Then by definition of cardinal, there exists an injection $f: A \to B$.
Then the mapping $h: A \cup C \to B \cup C$ defined as:
:$\forall x \in A \cup C: \map h x = \begin{cases}
\map f x & : x \in A \\
x & : x \in C
\end{cases}$
Let $a_1 \in A \cup C$ and $a_2 \in A \cup C$ such that:
:$\map h {a_1} = \map h {a_2}$
Then:
{{begin-eqn}}
{{eqn | l = a_1
      | o = \in
      | r = C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a_1
      | r = \map h {a_1}
      | c = Definition of $h$
}}
{{eqn | ll= \leadsto
      | l = a_1
      | r = \map h {a_2}
      | c = as $\map h {a_1} = \map h {a_2}$
}}
{{eqn | ll= \leadsto
      | l = a_1
      | r = a_2
      | c = as $\map h {a_2}$ must also be in $C$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a_1
      | o = \notin
      | r = C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map h {a_1}
      | r = \map f {a_1}
      | c = Definition of $h$
}}
{{eqn | ll= \leadsto
      | l = \map h {a_2}
      | r = \map f {a_1}
      | c = as $\map h {a_1} = \map h {a_2}$
}}
{{eqn | ll= \leadsto
      | l = \map h {a_2}
      | r = \map f {a_2}
      | c = as $\map h {a_2}$ must also not be in $C$
}}
{{eqn | ll= \leadsto
      | l = \map f {a_1}
      | r = \map f {a_2}
      | c = as $\map h {a_1} = \map h {a_2}$
}}
{{eqn | ll= \leadsto
      | l = a_1
      | r = a_2
      | c = as $f$ is an injection
}}
{{end-eqn}}
So:
:$\map h {a_1} = \map h {a_2} \implies a_1 = a_2$
demonstrating that $h$ is an injection.
So, by definition of sum of cardinals:
:$\mathbf a + \mathbf c \le \mathbf b + \mathbf c$
{{qed}}
Theorem: Group is B-Algebra Iff All Elements Self-Inverse

Let $\struct {G, \circ}$ be a group whose identity element is $e$.
Then $\struct {G, \circ}$ is also a $B$-algebra {{iff}}:
:$\forall g \in G: g = g^{-1}$
That is, {{iff}} all elements of $G$ are self-inverse.

Proof:
Let $\struct {G, \circ}$ be a group such that $\forall g \in G: g = g^{-1}$.
From Group Induces B-Algebra, the algebraic structure $\struct {G, *}$ where $*$ is defined as:
:$\forall a, b \in G: a * b := a \circ b^{-1}$
is a $B$-algebra.
But as $b = b^{-1}$, it follows that:
:$\forall a, b \in G: a * b := a \circ b$
and so $\struct {G, \circ}$ is itself a $B$-algebra.
Now suppose it is not the case that $\forall g \in G: g = g^{-1}$.
Suppose $\struct {G, \circ}$ were a $B$-algebra.
By {{B-algebra-axiom|2}}, the identity element $e$ would be the $0$, as:
:$\forall a \in G: a \circ 0 = a$
As an Identity is Unique, there can be no other element in $G$ which can satisfy the conditions to be the $0$ of a $B$-algebra.
Now as not every element is self-inverse:
:$\exists x \in G: x \circ x \ne e$
Then by {{B-algebra-axiom|1}} it follows that $\struct {G, \circ}$ is not a $B$-algebra.
Hence the result.
{{qed}}
Category:Group Theory
Category:B-Algebras
djjbp5esjoule2xwmn2s7onm1w1y0jl
Theorem: Condition for Existence of Cardinal Sum

Let $\mathbf a$ and $\mathbf b$ be cardinals.
Then:
: $\mathbf a \le \mathbf b \iff \exists \mathbf c: \mathbf a + \mathbf c = \mathbf b$
where $\mathbf c$ is also a cardinal.

Proof:
Let $\mathbf a = \card A$ and $\mathbf b = \card B$ for some sets $A$ and $B$.
From Equivalence of Definitions of Dominate (Set Theory), there exists a bijection from $A$ onto a subset $E$ of $B$.
Thus:
: $\mathop a = \card E$
Let $F = \relcomp B E$
From Set with Relative Complement forms Partition:
: $B = E \cup F$
: $E \cap F = \O$
By definition of sum of cardinals, it follows that:
{{begin-eqn}}
{{eqn | l = \mathbf b
      | r = \card B
      | c =
}}
{{eqn | r = \card {E \cup F}
      | c =
}}
{{eqn | r = \card E + \card F
      | c =
}}
{{eqn | r = \mathbf a + \card F
      | c =
}}
{{end-eqn}}
By defining $\mathbf c := \card F$ it follows that:
:$\mathbf a + \mathbf c = \mathbf b$
for the $\mathbf c$ that has been demonstrated to exist.
Now suppose there exists a cardinal $\mathbf c$ such that $\mathbf a + \mathbf c = \mathbf b$.
Then by definition of sum of cardinals:
:$\card B = \card {A \cup C}$
for some sets $A$, $B$ and $C$ such that $A \cap C = \O$.
Let $f: A \to B$ be an injection, proved to exist by Equivalence of Definitions of Dominate (Set Theory).
Then it follows that $\mathbf a \le \mathbf b$.
{{qed}}
Theorem: Cardinal One is Cancellable for Cardinal Sum

Let $\mathbf a$ and $\mathbf b$ be cardinals.
Then:
:$\mathbf a + \mathbf 1 = \mathbf b + \mathbf 1 \implies \mathbf a = \mathbf b$
where $\mathbf 1$ is (cardinal) one.

Proof:
Suppose $\mathbf a + \mathbf 1 = \mathbf b + \mathbf 1$.
Then from Condition for Existence of Cardinal Sum there exists some cardinal $\mathbf c$ such that 
:$\mathbf a + \mathbf 1 = \mathbf b + \mathbf 1 = \mathbf c$
By definition of cardinal there exists a set $C$ such that $\mathbf c = \map \Card C$.
$C$ also has subsets $A$ and $B$ such that there also exist elements of $\alpha, \beta \in C$ such that:
:$\relcomp C A = \set \alpha$
:$\relcomp C B = \set \beta$
If $\alpha = \beta$ then $A = B$ and so $\mathbf a = \mathbf b$.
On the other hand, if $\alpha \ne \beta$ then $\alpha \in B$ and $\beta \in A$ and so:
:$\set \beta \cup \paren {A \cap B} = A$
:$\set \alpha \cup \paren {A \cap B} = B$
Since:
:$\set \beta \cap A \cap B = \O = \set \alpha \cap A \cap B$
it follows that:
:$\mathbf a = \map \Card A = \mathbf 1 + \map \Card {A \cap B} = \map \Card B = \mathbf b$
{{qed}}
Theorem: Mapping from Finite Set to Itself is Injection iff Surjection

Let $S$ be a finite set.
Let $f: S \to S$ be a mapping.
Then $f$ is injective {{iff}} $f$ is surjective.

Proof:
Let $f$ be an injection.
From Injection to Image is Bijection, $S$ is equivalent to the image $\Img f$ of $f$.
We are given that $S$ is finite.
It follows from Infinite Set is Equivalent to Proper Subset that $\Img f = S$.
It follows by definition that $f$ is surjective.
{{qed|lemma}}
Let $f$ be a surjection.
Then by Surjection iff Right Inverse there exists a mapping $g: S \to S$ such that:
:$f \circ g = I_S$
where $I_S$ is the identity mapping.
By Right Inverse Mapping is Injection, $g$ is an injection.
By the above, it follows that $g$ is also a surjection.
Thus $g$ is a bijection.
It follows that $f = g^{-1}$ is also a bijection and so by definition an injection.
{{qed}}
Theorem: Finite Cardinals form Infinite Set

The finite cardinals form a set which is infinite.

Proof:
{{proof wanted|This proof depends upon the Axiom of Infinity.}}
Theorem: Natural Numbers as Cardinals

The natural numbers $\N = \set {0, 1, 2, 3, \ldots}$ can be defined as the set of cardinals.

Proof:
From Finite Cardinals form Infinite Set we have that the cardinals form a set which is infinite.
{{proof wanted|Show that the set of finite cardinals satisfy Peano's axioms.}}