avewright/proofwiki-math huggingface dataset:
Theorem: Order of Group of Units of Integers Modulo n

Let $n \in \Z_{\ge 0}$ be an integer.
Let $\struct {\Z / n \Z, +, \cdot}$ be the ring of integers modulo $n$.
Let $U = \struct {\paren {\Z / n \Z}^\times, \cdot}$ denote the group of units of this ring.
Then:
:$\order U = \map \phi n$
where $\phi$ denotes the Euler $\phi$-function.

Proof:
By Reduced Residue System under Multiplication forms Abelian Group, $U$ is equal to the set of integers modulo $n$ which are coprime to $n$.
It follows by Cardinality of Reduced Residue System:
:$\order U = \map \phi n$
{{qed}}
Theorem: Cyclicity Condition for Units of Ring of Integers Modulo n

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $\struct {\Z / n \Z, +, \times}$ be the ring of integers modulo $n$.
Let $U = \struct {\paren {\Z / n \Z}^\times, \times}$ denote the group of units of $\struct {\Z / n \Z, +, \times}$.
Then $U$ is cyclic {{iff}} either:
:$n = p^\alpha$
or:
:$n = 2 p^\alpha$
where $p \ge 3$ is prime and $\alpha \ge 0$.

Proof:
{{tidy}}
{{MissingLinks}}
Theorem: Chinese Remainder Theorem/Corollary

Let $n_1, n_2, \ldots, n_r$ be pairwise coprime positive integers.
Let $\ds N = \prod_{i \mathop = 1}^r n_i$.
For an integer $k$, let $\Z / k \Z$ denote the ring of integers modulo $k$.
Then we have a ring isomorphism:
:$\Z / N \Z \simeq \Z / n_1 \Z \times \cdots \times \Z / n_r \Z$

Proof:
Define a mapping:
:$\phi: \Z / N \Z \to \Z / n_1 \Z \times \cdots \times \Z / n_r \Z$
by:
:$\map \phi {d \pmod N} = \paren {d \pmod {n_1}, \ldots, d \pmod {n_r} }$
Then, by Mappings Between Residue Classes, $\phi$ is well-defined.
By the definition of multiplication and addition in $\Z / k \Z$, $k \in \Z$ we have:
:$\paren {a \pmod k} + \paren {b \pmod k} = \paren {a + b} \pmod k$
and
:$\paren {a \pmod k} \cdot \paren {b \pmod k} = \paren {a \cdot b} \pmod k$
Thus taking $k = n_1, \ldots, n_r$ separately we see that $\phi$ is a ring homomorphism.
Let:
:$\paren {a_1 \pmod {n_1}, \ldots, a_r \pmod {n_r} } \in \Z / n_1 \Z \times \cdots \times \Z / n_r \Z$
By the Chinese Remainder Theorem there exists a unique $x \in \Z / N \Z$ such that:
:$\map \phi x = \paren {a_1 \pmod {n_1}, \ldots, a_r \pmod {n_r} }$
Since such an $x$ exists, $\phi$ is surjective.
Since this $x$ is unique modulo $N$, it follows that $\phi$ is injective.
{{Qed}}
Theorem: Hilbert's Basis Theorem/Corollary

Let $A$ be a Noetherian ring.
Let $n \ge 1$ be an integer.
Let $A \sqbrk {x_1, \ldots, x_n}$ be the ring of polynomial forms over $A$ in the indeterminates $x_1, \ldots, x_n$.
Then $A \sqbrk {x_1, \ldots, x_n}$ is also a Noetherian ring.

Proof:
We proceed by induction over $n \ge 1$.
Theorem: Component of Finite Union in Ultrafilter

Let $S$ be a non-empty set.
Let $\UU$ be a ultrafilter on $S$.
Let $\set {Y_1, \dots, Y_n}$ be a pairwise disjoint set of subsets of $S$ such that $S = Y_1 \cup \cdots \cup Y_n$.
Then there is a unique $k \in \set {1, \dots, n}$ such that $Y_k \in \UU$.

Proof:
Assume that none of the $Y_k$ are empty.
If not, then any empty ones can simply be removed.
Theorem: Restricted Tukey's Theorem/Weak Form

Let $X$ be a set.
Let $\AA$ be a non-empty set of subsets of $X$.
Let $'$ be a unary operation on $X$.
Let $\AA$ have finite character.
For all $A \in \AA$ and all $x \in X$, let either:
:$A \cup \set x \in \AA$
or:
:$A \cup \set {x'} \in \AA$
Then there exists a $B \in \AA$ such that for all $x \in X$, either $x \in B$ or $x' \in B$.

Proof:
{{ProofWanted}}
{{Namedfor|John Wilder Tukey|cat = Tukey}}
Theorem: Restricted Tukey's Theorem/Strong Form

Let $X$ be a set.
Let $\AA$ be a non-empty set of subsets of $X$.
Let $'$ be a unary operation on $X$.
Let $\AA$ have finite character.
For all $A \in \AA$ and all $x \in X$, let either:
: $A \cup \set x \in \AA$
or:
:$A \cup \set {x'} \in \AA$
Then for each $A \in \AA$ there exists a $C \in \AA$ such that:
:$A \subseteq C$
and:
:for all $x \in X$, either $x \in C$ or $x' \in C$.

Proof:
Let $A \in \AA$.
Let:
:$\BB = \set {B: B \subseteq X \text{ and } A \cup B \in \AA}$
It is to be shown that $\BB$ has finite character:
First suppose that $B \in \BB$ and $F$ is a Definition:Finite Subset subset of $B$.
Then since $B \in \BB$, $B \subseteq X$ and $A \cup B \in \AA$.
We wish to show that $F \in \BB$.
Since $F \subseteq B \subseteq X$:
:$F \subseteq X$
It remains to be shown that:
:$A \cup F \in \AA$.
$A \cup F \subseteq A \cup B$.
Let $G$ be a finite subset of $A \cup F$.
Then $G$ is a finite subset of $A \cup B$.
Since $A \cup B \in \AA$ and $\AA$ has finite character, $G \in \AA$.
Thus every finite subset of $A \cup F$ is in $\AA$.
Since $\AA$ has finite character, $A \cup F \in \AA$.
Thus $F \in \BB$.
Suppose instead that $B \subseteq X$ and every finite subset of $B$ is an element of $\BB$.
We wish to show that $B \in \BB$.
In order to do this, we must show that $A \cup B \in \AA$.
Let $F$ be a finite subset of $A \cup B$.
$\AA$ has finite character, $F \cap A \in \AA$.
Since $F \cap B$ is a finite subset of $B$, $F \cap B \in \BB$ by assumption.
Then by the definition of $\BB$:
:$\paren {F \cap B} \cup A \in \AA$
But $F$ is a finite subset of $\paren {F \cap B} \cup A \in \AA$.
Since $\AA$ has finite character, $F \in \AA$.
As this holds for all finite subsets of $A \cup B$ and $\AA$ has finite character:
:$A \cup B \in \AA$
{{qed|lemma}}
Let $B \in \BB$ and $x \in X$.
Then:
:$B \cup A \in \AA$
so either $B \cup A \cup \set x$ or $B \cup A \cup \set {x'}$ is in $\AA$.
But then $B \cup \set x$ or $B \cup \set {x'}$ is in $\BB$ by the definition of $\BB$.
Thus $\BB$ satisfies the premises of the weak form of the Restricted Tukey's Theorem.
Thus there is a $B \in \BB$ such that for all $x \in X$, either $x \in B$ or $x' \in B$.
Let $C = A \cup B$.
Then since $B \subseteq C$, if $x \in X$ then either $x \in C$ or $x' \in C$.
But since $B \in \BB$:
:$C = A \cup B \in \AA$
{{qed}}
{{namedfor|John Wilder Tukey|cat = Tukey}}
Theorem: Boolean Prime Ideal Theorem/Extension Lemma

Let $\struct {B, \vee, \wedge, \le}$ be a Boolean lattice.
Let $F \subseteq B$ be a filter.
Let $J \subseteq B$ have the finite join property with respect to $F$.
Let $z \in B$.
Then either $J \cup \set z$ or $J \cup \set {\neg z}$ also has the finite join property with respect to $F$.

Proof:
{{AimForCont}} that neither $J \vee z$ nor $J \vee \neg z$ has the finite join property with respect to $F$.
Then there are $x_1, \dots, x_n, y_1, \dots, y_m \in J$ such that $x_1 \vee \dots \vee x_n \vee z \in F$ and $y_1 \vee \dots \vee y_m \vee \neg z \in F$.
Let $q = x_1 \vee \dots \vee x_n \vee y_1 \vee \dots \vee y_m$.
Then, by Join Succeeds Operands:
:$x_1 \vee \dots \vee x_n \le q$
:$y_1 \vee \dots \vee y_m \le q$
and so:
:$q \vee z \in F$
:$q \vee \neg z \in F$
by filter axiom $\paren 3$.
Thus:
{{begin-eqn}}
{{eqn | l = F
      | o = \ni
      | r = \paren {q \vee z} \wedge \paren {q \vee \neg z}
      | c = Filter is Closed under Meet
}}
{{eqn | r = \paren {q \wedge \paren {q \vee \neg z} } \vee \paren {z \wedge \paren {q \vee \neg z} }
      | c = Distributive Lattice Axiom $\paren {1'}$
}}
{{eqn | r = q \vee \paren {\paren {q \wedge z} \vee \paren {\neg z \wedge z} }
      | c = Meet Absorbs Join, Meet is Commutative, Distributive Lattice Axiom $\paren {1'}$
}}
{{eqn | r = q \vee \paren {q \wedge z}
      | c = {{Defof|Complement (Lattice Theory)|Complement}}, {{Defof|Bottom of Lattice|index = 2}}
}}
{{eqn | r = q
      | c = Join Absorbs Meet
}}
{{end-eqn}}
This contradicts the fact that $J$ has the finite join property.
{{qed}}
Category:Lattice Theory
hr5lnycab2352cuiahopfcvfsebe8u9
Theorem: Finite Character for Sets of Mappings

Let $S$ and $T$ be sets.
Let $\FF$ be a set of mappings from subsets of $S$ to $T$.
That is, let $\FF$ be a set of partial mappings from $S$ to $T$.
Then the following are equivalent:
{{begin-axiom}}
{{axiom | n = 1
        | t = $\FF$ has finite character in the sense of Definition:Finite Character/Mappings.
}}
{{axiom | n = 2
        | t = $\FF$ has finite character as a set of subsets of $S \times T$ in the sense of Definition:Finite Character.
}}
{{end-axiom}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $\FF$ have finite character in the sense of Definition:Finite Character/Mappings.
That is, suppose that for each partial mapping $f \subseteq S \times T$:
:$f \in \FF$ {{iff}} for each finite subset $K$ of the domain of $f$, the restriction of $f$ to $K$ is in $\FF$.
Let $q \subseteq S \times T$.
First suppose that $q \in \FF$.
Let $r$ be a finite subset of $q$.
Then $r$ is a partial mapping from its domain into $T$.
Since $r$ is finite, its domain, $\Dom r$, is a finite subset of the domain of $q$.
Since $\FF$ is of finite character as a set of mappings, $q \restriction \Dom r$ is in $\FF$.
But $q \restriction \Dom r = r$.
Therefore $r \in \FF$.
{{explain}}
Suppose instead that for each finite subset $r$ of $q$, $r \in \FF$.
Then for each finite subset $r$ of $q$, $r$ is a partial mapping from $S$ to $T$.
Let $x \in \Dom q$.
Let $y_1, y_2 \in T$.
Suppose that $\tuple {x, y_1}, \tuple {x, y_2} \in q$.
Then $\set {\tuple {x, y_1}, \tuple {x, y_2} }$ is a finite subset of $q$.
Therefore it must be a partial mapping.
Thus $y_1 = y_2$.
As this holds for all such $x, y_1, y_2$, $q$ is a partial mapping.
Let $K$ be a finite subset of $\Dom q$.
Then the restriction of $q$ to $K$ is a finite subset of $q$.
Thus $q \restriction K \in \FF$.
As this holds for all finite subsets $K$ of $\Dom q$, $q \in \FF$.
So we see that $\FF$ has finite character in the sense of Definition:Finite Character.
{{qed|lemma}}
Theorem: Ultrafilter Lemma/Corollary

Let $S$ be a non-empty set.
Let $\AA$ be a set of subsets of $S$.
Suppose that $\AA$ has the finite intersection property.
Then there is an ultrafilter $\UU$ on $S$ such that $\AA \subseteq \UU$.

Proof:
Let $\II$ be the set of intersections of non-empty finite subsets of $\AA$.
Let $\FF = \set {T \in \powerset S: \exists B \in \II: B \subseteq T}$.
Note that $\AA \subseteq \II \subseteq \FF$.
$\FF$ is a filter on $S$:
Because $\AA$ has the finite intersection property:
:$\O \notin \II$
Because each element of $\FF$ is a superset of some element of $\II$:
:$\O \notin \FF$
Let $P \in \FF$ and $P \subseteq Q \subseteq S$.
Then:
:$\exists B \in \II: B \subseteq P$
and so:
: $B \subseteq Q \subseteq S$
Thus:
:$Q \in \FF$
Let $P \in \FF$ and $Q \in \FF$.
Then:
:$\exists B, C \in \II: B \subseteq P$ and $C \subseteq Q$
Then:
:$B \cap C \in \II$
and:
:$B \cap C \subseteq P \cap Q \subseteq S$
Thus:
:$P \cap Q \in \FF$
Thus, by definition, $\FF$ is a filter on $S$.
By the Ultrafilter Lemma, there exists an ultrafilter $\UU$ on $S$ such that:
:$\FF \subseteq \UU$
Because $\AA \subseteq \FF$:
:$\AA \subseteq \UU$
{{qed}}
Category:Ultrafilter Lemma
7i7oq8boy33oo2e31nvdc6zekzu8jet
Theorem: Order-Extension Principle/Strict

Let $S$ be a set.
Let $\prec$ be a strict ordering on $S$.
Then there exists a strict total ordering $<$ on $S$ such that:
:$\forall a, b \in S: a \prec b \implies a < b$

Proof:
Let $\AA$ be the set of relations $A$ on $S$ with the property that the transitive closure $A^+$ of $A$ is a strict ordering of $S$.
For each $\tuple {x, y} \in S \times S$, let $\tuple {x, y}' = \tuple {y, x}$.
Let $A \in \AA$.
Let $\tuple {x, y} \in S \times S$.
Let $\tuple {x, y} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {x, y} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y} } \in \AA$
Let $\tuple {y, x} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {y, x} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y}'} = A \cup \set {\tuple {y, x} } \in \AA$
Otherwise, $x$ and $y$ are non-comparable by $A^+$.
So by Strict Ordering can be Expanded to Compare Additional Pair:
:$A \cup \set {\tuple {x, y} } \in \AA$
Thus it has been shown that for each $A \in \AA$ and each $\tuple {x, y} \in S$, either:
:$A \cup \set {\tuple {x, y} } \in \AA$
or:
:$A \cup \set {\tuple {x, y}'} \in \AA$
{{qed|lemma}}
Let $A \subseteq S \times S$.
Let $A \in \AA$.
Let $F$ be a finite subset of $A$.
Since $A^+$ is a strict ordering, it is asymmetric.
Since Transitive Closure is Closure Operator, $F^+ \subseteq A^+$.
So $F^+$ is also asymmetric.
Since $F^+$ is also transitive, it is a strict ordering.
So $F \in \AA$.
Suppose instead that each finite subset of $A$ is in $\AA$.
We must show that $A^+$ is antireflexive.
{{AimForCont}} that for some $x \in S$, $\tuple {x, x} \in A^+$.
Then by the definition of transitive closure, there are elements $y_0, \dots, y_n$ such that $x = y_0 = y_n$ and:
:$\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} \in A$
Let $F = \set {\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} }$.
Then $F$ is a finite subset of $A$.
But $\tuple {x, x} \in F^+$, contradicting the fact that $F \in \AA$.
Thus we see that $A^+$ is antireflexive, and thus a strict ordering of $S$.
Therefore, $\AA$ has finite character.
{{qed|lemma}}
Note that ${\prec} = {\prec^+}$, so ${\prec} \in \AA$.
By the Restricted Tukey's Theorem (Strong Form), there exists an $R \in \AA$ such that:
:${\prec} \subseteq R$
:For each $\tuple {m, n} \in S \times S$, either $\tuple {m, n} \in R$ or $\tuple {n, m} = \tuple {m, n}' \in R$.
Then:
:$R^+$ is a strict total ordering of $S$.
:$\forall a, b \in S: a \prec b \implies a < b$
{{qed}}
Theorem: Order-Extension Principle/Strict/Finite Set

Let $T$ be a finite set.
Let $\prec$ be a strict ordering on $T$.
Then there exists a strict total ordering $<$ on $T$ such that:
:$\forall a, b \in T: \paren {a \prec b \implies a < b}$

Proof:
{{ProofWanted|Use Strict Ordering can be Expanded to Compare Additional Pair.}}
Category:Set Theory
Category:Order Theory
3rvr5p803rau0xia8t260ztfwhhah99
Theorem: Finitely Satisfiable Theory has Maximal Finitely Satisfiable Extension/Lemma

Let $\LL$ be a language of predicate logic.
Let $T$ be a finitely satisfiable $\LL$-theory.
Let $\phi$ be an $\LL$-sentence.
Then either:
:$T \cup \set \phi$
or:
:$T \cup \set {\neg \phi}$
is finitely satisfiable.

Proof:
{{WLOG}}, suppose that $T \not\models \phi$ and $T \not\models \neg \phi$.
{{AimForCont}} that $T \cup \set \phi$ is not finitely satisfiable.
Then by definition there must be a finite subset $K$ of $T \cup \set \phi$ which is not satisfiable.
Since $T$ is finitely satisfiable, $\phi \in K$.
Therefore $\Delta = K \setminus \set \phi$ is a finite subset of $T$.
Thus, for every $\LL$-structure $\MM$ that models $\Delta$, $\phi$ is not valid.
Hence, for every $\LL$-structure $\MM$ that models $\Delta$, $\neg \phi$ is valid.
By definition, then, $\Delta \models \neg \phi$
:where $\models$ denotes semantic consequence.
Let $\Sigma$ be a finite subset of $T$.
Since $\Delta \cup \Sigma$ is a finite subset of $T$, it is satisfiable.
But $\Delta \models \neg \phi$.
Hence $\set {\neg \phi} \cup \Sigma$ is satisfiable.
But any finite subset of $T \cup \set {\neg \phi}$ is either in $T$ or of the form $\Sigma \cup \set {\neg \phi}$.
This demonstrates that $T \cup \set {\neg \phi}$ is finitely satisfiable, contradicting our assumption.
{{qed}}
{{LEM||3}}
Category:Model Theory for Predicate Logic
o4ghuk6srh3v820ysnd4qr46bf4vj8k
Theorem: Finitely Satisfiable Theory has Maximal Finitely Satisfiable Extension/Proof 2

Let $T$ be a finitely satisfiable $\LL$-theory.
There is a finitely satisfiable $\LL$-theory $T'$ which contains $T$ as a subset such that for all $\LL$-sentences $\phi$, either $\phi \in T'$ or $\neg\phi \in T'$.
{{explain|Does this actually mean the same as the statement of the theorem in Finitely Satisfiable Theory has Maximal Finitely Satisfiable Extension? If so, replace it. If not, then it is a different proof altogether. If the two statements are equivalent, then this needs to be demonstrated.}}

Proof:
Let $\AA$ be the set of finitely satisfiable extensions of $T$.
By the lemma, for each element $S$ of $\AA$ and each $\LL$-sentence $\phi$, either $S \cup \set \phi \in \AA$ or $S \cup \set {\neg \phi} \in \AA$.
$\AA$ has finite character, by the following argument:
Let $S \in \AA$.
Let $F$ be a finite subset of $S$.
Then $S$ is satisfiable and hence finitely satisfiable.
Thus in $\AA$.
Let $S$ be a theory on $\LL$.
Let every finite subset of $S$ be finitely satisfiable.
Then every finite subset of $S$ is satisfiable.
Therefore $S$ is finitely satisfiable.
Thus $\AA$ has finite character.
By the Restricted Tukey's Theorem, $\AA$ has an element $T'$ such that:
:for each $\LL$-sentence $\phi$, either $\phi \in T'$ or $\neg \phi \in T'$.
{{qed}}
Theorem: Reflexive Closure of Strict Total Ordering is Total Ordering

Let $S$ be a set.
Let $\prec$ be a strict total ordering of $S$.
Let $\preceq$ be the reflexive closure of $\prec$.
Then $\preceq$ is an total ordering of $S$.

Proof:
By the definition of strict total ordering, $\prec$ is a strict ordering which connects $S$.
By Reflexive Closure of Strict Ordering is Ordering, $\preceq$ is a ordering.
Since $\prec$ connects $S$, for each $a, b \in S$, either $a = b$, $a \prec b$ or $b \prec a$.
If $a = b$, then $a \preceq b$.
If $a \prec b$, then $a \preceq b$.
If $b \prec a$, then $b \preceq a$.
Thus in all cases either $a \preceq b$ or $b \preceq a$.
Thus $\preceq$ is a total ordering of $S$.
{{qed}}
Category:Strict Orderings
Category:Total Orderings
Category:Reflexive Closures
2qrsz4gca7i58m25eytsnixcbb34jfw
Theorem: Galois Field of Order q Exists iff q is Prime Power

Let $q \ge 0$ be a positive integer.
Then there exists a Galois field of order $q$ {{iff}} $q$ is a prime power.

Proof:
{{tidy}}
{{MissingLinks}}
Theorem: Leaf of Rooted Tree is on One Branch

Let $T$ be a rooted tree with root node $r_T$.
Let $t$ be a leaf node of $T$.
Then there exists a unique branch $\Gamma$ of $T$ such that $t \in \Gamma$.

Proof:
Let $t$ be on the branch $\Gamma$.
By definition of branch, $\Gamma$ is a path from the root node $r_T$ to $t$.
By Path in Tree is Unique, such $\Gamma$ is unique.
{{qed}}
Theorem: Branch of Finite Tree is Finite

Let $T$ be a finite rooted tree with root node $r_T$.
Let $\Gamma$ be a branch of $T$.
Then $\Gamma$ is a finite branch.

Proof:
Let $\Gamma$ be a branch of a finite rooted tree $T$.
{{AimForCont}} $\Gamma$ were an infinite branch of $T$.
By definition $\Gamma$ contains an infinite number of nodes.
{{explain|Technically, from the definition currently posted, it doesn't - that still needs to be demonstrated.}}
From Subset of Finite Set is Finite, it follows that $\Gamma$ has a finite number of nodes.
From this contradiction it follows that $\Gamma$ can not be an infinite branch of $T$.
Hence the result.
{{qed}}
Theorem: Snake Lemma

Let $A$ be a commutative ring with unity.
Let:
::<nowiki>$\begin{xy}\xymatrix@L+2mu@+1em{
&
 M_1 \ar[r]_*{\alpha_1}
     \ar[d]^*{\phi_1}
&
 M_2 \ar[r]_*{\alpha_2}
     \ar[d]^*{\phi_2}
&
 M_3 \ar[d]^*{\phi_3}
     \ar[r]
& 
 0
\\
 0 \ar[r]
&
 N_1 \ar[r]_*{\beta_1}
&
 N_2 \ar[r]_*{\beta_2}
&
 N_3
&
}\end{xy}$</nowiki>
be a commutative diagram of $A$-modules.
Suppose that the rows are exact.
Then we have a commutative diagram:
::<nowiki>$\begin{xy}\xymatrix@L+2mu@+1em{
&
 \ker \phi_1 \ar[r]_*{\tilde\alpha_1}
     \ar[d]^*{\iota_1}
&
 \ker \phi_2 \ar[r]_*{\tilde\alpha_2}
     \ar[d]^*{\iota_2}
&
 \ker \phi_3
     \ar[d]^*{\iota_3}
&
\\
&
 M_1 \ar[r]_*{\alpha_1}
     \ar[d]^*{\phi_1}
&
 M_2 \ar[r]_*{\alpha_2}
     \ar[d]^*{\phi_2}
&
 M_3 \ar[d]^*{\phi_3}
     \ar[r]
& 
 0
\\
 0 \ar[r]
&
 N_1 \ar[r]_*{\beta_1}
     \ar[d]^*{\pi_1}
&
 N_2 \ar[r]_*{\beta_2}
     \ar[d]^*{\pi_2}
&
 N_3 \ar[d]^*{\pi_3}
\\
&
 \operatorname{coker} \phi_1 \ar[r]_*{\bar\beta_1}
&
 \operatorname{coker} \phi_2 \ar[r]_*{\bar\beta_2}
&
 \operatorname{coker} \phi_3
&
}\end{xy}$</nowiki>
where, for $i = 1, 2, 3$ respectively $i = 1, 2$:
* $\ker \phi_i$ is the kernel of $\phi_i$
* $\operatorname{coker} \phi_i$ is the cokernel of $\phi_i$
* $\iota_i$ is the inclusion mapping
* $\pi_i$ is the quotient epimorphism
* $\tilde \alpha_i = \alpha_i {\restriction \ker \phi_i}$, the restriction of $\alpha_i$ to $\ker \phi_i$
* $\bar \beta_i$ is defined by:
::$\forall n_i + \Img {\phi_i} \in \operatorname {coker} \phi_i : \map {\bar \beta_i} {n_i + \Img {\phi_i} } = \map {\beta_i} {n_i} + \Img {\phi_{i + 1} }$
Moreover there exists a morphism $\delta : \ker \phi_3 \to \operatorname{coker} \phi_1$ such that we have an exact sequence:
::<nowiki>$\begin{xy}\xymatrix@L+2mu@+1em{
 \ker \phi_1 \ar[r]_*{\tilde\alpha_1}
&
 \ker \phi_2 \ar[r]_*{\tilde\alpha_2}
&
 \ker\phi_3 \ar[r]_*{\delta}
& 
 \operatorname{coker}\phi_1 \ar[r]_*{\bar\beta_1}
&
 \operatorname{coker}\phi_2 \ar[r]_*{\bar\beta_2}
&
 \operatorname{coker}\phi_3
}\end{xy}$</nowiki>

Proof:
{{ProofWanted}}
Category:Homological Algebra
Category:Named Theorems
gv5hyctbr94a8kkgou9pchdutitewfy
Theorem: Hall's Marriage Theorem/Finite Set

Let $\SS = \family {S_k}_{k \mathop \in I}$ be a finite indexed family of finite sets.
For each $F \subseteq I$, let $\ds Y_F = \bigcup_{k \mathop \in F} S_k$.
Let $Y = Y_I$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\SS$ satisfies the marriage condition: {{:Axiom:Marriage Condition}} }}
{{item|(2):|There exists an injection $f: I \to Y$ such that $\forall k \in I: \map f k \in S_k$}}
{{end-itemize}}

Proof:
=== $(2)$ implies $(1)$ ===
Let:
:$\exists P \subseteq I: \card P > \card {Y_P}$
Then:
:$\card P \not \le \card {Y_P}$
By contrapositive of Injection implies Cardinal Inequality, there can be no injection from $P$ to $Y_P$.
Thus there can be no injection from $I$ to $Y$ satisfying the requirements.
{{qed|lemma}}
Theorem: Connecting Homomorphism is Functorial

Let $A$ be a ring with unity.
Let:
:<nowiki>$\begin{xy}\xymatrix{
&&& M_1 \ar@{->}[rr]
     \ar@{->}[dl]^{f_1}
     \ar@{->}[dd]^{\phi_1}|!{[d];[d]}\hole
&& M_2 %
     \ar@{->}[rr]
     \ar@{->}[dl]^{f_2}
     \ar@{->}[dd]^{\phi_2}|!{[d];[d]}\hole
&& M_3 \ar@{->}[dl]^{f_3}
      \ar@{->}[dd]^{\phi_3}|!{[d];[d]}\hole
      \ar@{->}[rr]
&& 0
\\
&& M_1' \ar@{->}[rr]
   \ar@{->}[dd]^{\phi_1'}
&& M_2' \ar@{->}[rr]
     \ar@{->}[dd]^{\phi_2'}
&& M_3' \ar@{->}[dd]^{\phi_3'}
       \ar@{->}[rr]
&& 0
\\
& 0 \ar@{->}[rr]|!{[r];[r]}\hole
&& N_1 \ar@{->}[rr]|!{[r];[r]}\hole
     \ar@{->}[dl]_{g_1}
&& N_2 \ar@{->}[rr]|!{[r];[r]}\hole
     \ar@{->}[dl]_{g_2}
&& N_3 \ar@{->}[dl]_{g_3}
\\
%
0 \ar@{->}[rr]
&&
N_1' \ar@{->}^(.65){e’}[rr]
&&
N_2' \ar@{->}[rr]
&&
N_3'
}\end{xy}$</nowiki>
be a commutative diagram of $A$-modules.
Suppose that the rows are exact.
Let 
:$\delta : \map \ker {\phi_3} \to \map {\operatorname {coker} } {\phi_1}$ 
:$\delta' : \map \ker {\phi_3'} \to \map {\operatorname {coker} } {\phi_1'}$ 
be the boundary homomorphisms coming from Snake Lemma applied to the front diagram and the back diagram.
Then the diagram:
:<nowiki>$\begin{xy}\xymatrix{
\map \ker {\phi_3} \ar[r]^{\delta} \ar[d] & \map {\operatorname{coker} } {\phi_1} \ar[d] \\
\map \ker {\phi_3'} \ar[r]^{\delta'} & \map {\operatorname{coker} } {\phi_1'} \\
}
\end{xy}$</nowiki>
is commutative.
Here the vertical arrows in the commutative square are induced by $\tuple {f_3, g_3}$ and $\tuple {f_1, g_1}$.
{{finish}}

Proof:
{{proof wanted}}
Category:Homological Algebra
88br8tds8012egp9su74479ll2ycs7b
Theorem: Hall's Marriage Theorem/General Set

Let $\SS = \family {S_k}_{k \mathop \in I}$ be an indexed family of finite sets.
For each $F \subseteq I$, let $\ds Y_F = \bigcup_{k \mathop \in F} S_k$.
Let $Y = Y_I$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\SS$ satisfies the marriage condition: {{:Axiom:Marriage Condition}} }}
{{item|(2):|There exists an injection $f: I \to Y$ such that $\forall k \in I: \map f k \in S_k$}}
{{end-itemize}}

Proof:
=== $(2)$ implies $(1)$ ===
Suppose that for some finite $F \subseteq I$, $\card F > \card {Y_F}$.
Then $\card F \not \le \card {Y_F}$.
By contrapositive of Injection implies Cardinal Inequality, there can be no injection from $F$ to $Y_F$.
Thus there can be no injection from $I$ to $Y$ satisfying the requirements.
{{qed|lemma}}
Theorem: Branch of Finite Propositional Tableau is Finite

Let $T$ be a finite propositional tableau.
Let $\Gamma$ be a branch of $T$.
Then $\Gamma$ is a finite branch.

Proof:
By definition, a finite propositional tableau $T$ is formed by applying the tableau extension rules a finite number of times.
Each tableau extension rule extends $T$ finitely.
Therefore $T$ is a finite tree.
The result follows from Branch of Finite Tree is Finite.
{{qed}}
Category:Propositional Tableaux
kog39iuejrvkl50ne1cm6fbz2dr3llp