avewright/proofwiki-math huggingface dataset:
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Proof 1

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
Let:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
It is to be shown that:
:* $\quad \mathscr I$ satisfies the matroid axioms
and
:* $\quad \rho$ is the rank function of the matroid $M = \struct{S, \mathscr I}$
==== Matroid Axioms ====
===== Matroid Axiom $(\text I 1)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 4}}{{qed|lemma}}
===== Matroid Axiom $(\text I 2)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5/Proof 1}}{{qed|lemma}}
===== Matroid Axiom $(\text I 3)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 6}}{{qed|lemma}}
==== $\rho$ is Rank Function ====
Let $\rho_M$ be the rank function of the matroid $M = \struct{S, \mathscr I}$.
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 8}}{{qed}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Proof 2

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
=== Lemma 1 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 1}}
=== Lemma 2 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 2}}
=== Lemma 3 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 3}}
Let:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
It is to be shown that:
:* $\quad \mathscr I$ satisfies the matroid axioms
and
:* $\quad \rho$ is the rank function of the matroid $M = \struct{S, \mathscr I}$
=== Matroid Axioms ===
==== Matroid Axiom $(\text I 1)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5}}{{qed|lemma}}
==== Matroid Axiom $(\text I 2)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5/Proof 2}}{{qed|lemma}}
==== Matroid Axiom $(\text I 4)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 7}}{{qed|lemma}}
We have proven that $\mathscr I$ satisifies the matroid axioms.
It follows that $M = \struct{S, \mathscr I}$ is a matroid by definition.
=== $\rho$ is Rank Function ===
Let $\rho_M$ be the rank function of the matroid $M = \struct{S, \mathscr I}$.
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 8}}{{qed}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 1

:$\forall A, B \subseteq S: A \subseteq B \implies \map \rho A \le \map \rho B$

Proof:
{{AimForCont}}:
:$\exists A, B \subseteq S : A \subseteq B$ and $\map \rho A > \map \rho B$
Let $B \subseteq S$:
:$\exists A \subseteq B : \map rho A > \map \rho B$
Let $A_0 \subseteq B$:
:$\card {A_0} = \max \set{\card A : A \subseteq B \land \map \rho A > \map \rho B}$
As $\map \rho {A_0} > \map \rho B$:
:$A_0 \ne B$
From Set Difference with Proper Subset:
:$\exists y \in B \setminus A_0$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho B
      | o = < 
      | r = \map \rho {A_0}
      | c = By Choice of $A_0$
}}
{{eqn | o = \le 
      | r = \map \rho {A_0 \cup \set y}
      | c = Rank axiom $(\text R 2)$
}}
{{eqn | o = \le 
      | r = \map \rho B
      | c = By Choice of $A_0$
}}
{{end-eqn}}
This is a contradiction.
Hence:
:$\forall A, B \subseteq S: A \subseteq B \implies \map \rho A \le \map \rho B$
{{qed}}
Category:Formulation 1 Rank Axioms Implies Rank Function of Matroid
jcsx2c6dlxw0l0u74xtcca6d7a20je3
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 2

:$\forall A \subseteq S: \map \rho A \le \card A$

Proof:
{{AimForCont}}:
:$\exists A \subseteq S : \map \rho A > \card A$
Let:
:$A_0 \subseteq S : \card{A_0} = \min \set{\card A : \map \rho A > \card A}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho \O
      | r = 0
      | c = Rank axiom $(\text R 1)$
}}
{{eqn | r = \card \O
      | c = Cardinality of Empty Set
}}
{{end-eqn}}
Hence:
:$A_0 \ne \O$
Let $y \in A_0$.
From Cardinality of Set Difference:
:$\card {A_0 \setminus \set y} = \card{A_0} - 1 < \card {A_0}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {A_0}
      | r = \map \rho {\paren {A_0 \setminus \set y} \cup \set y}
}}
{{eqn | o = \le
      | r = \map \rho {A_0 \setminus \set y} + 1
      | c = Rank axiom $(\text R 2)$
}}
{{eqn | o = \le
      | r = \card {A_0 \setminus \set y} + 1
      | c = By choice of $A_0$
}}
{{eqn | r = \card {A_0} - \card{\set y} + 1
      | c = Cardinality of Set Difference with Subset
}}
{{eqn | r = \card {A_0} - 1 + 1
      | c = Cardinality of Singleton
}}
{{eqn | r = \card {A_0}
}}
{{end-eqn}}
This contradicts the choice of $A_0$:
:$\card{A_0} = \min \set{\card A : \map \rho A > \card A}$
It follows that:
:$\forall A \subseteq S: \map \rho A \le \card A$
{{qed}}
Category:Formulation 1 Rank Axioms Implies Rank Function of Matroid
kl031kcqw6347ugz3ezudefiakrxqvx
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 3

Let:
:$A \subseteq S : \map \rho A = \card A$
Let:
:$B \subseteq S : \forall b \in B \setminus A : \map \rho {A \cup \set b} \ne \card{A \cup \set b}$
Then:
:$\map \rho {A \cup B} = \map \rho A$

Proof:
=== Case 1 : $B \setminus A = \O$ ===
Let $B \setminus A = \O$.
From Set Difference with Superset is Empty Set:
:$B \subseteq A$
From Union with Superset is Superset:
:$A \cup B = A$
It follows that:
:$\map \rho {A \cup B} = \map \rho A$
{{qed|lemma}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 8

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ be the matroid where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Let $\rho_M$ be the rank function of the matroid $M = \struct{S, \mathscr I}$.
Then $\rho_M = \rho$.

Proof:
Let $X \subseteq S$.
By definition of the rank function:
:$\map {\rho_M} X = \max \set{\card Y : Y \subseteq X, Y \in \mathscr I}$
Let $Y_0 \subseteq X$:
:$\card {Y_0} = \max \set{\card Y : Y \subseteq X, Y \in \mathscr I}$
Then:
{{begin-eqn}}
{{eqn | l = \map {\rho_M} X
      | r = \card {Y_0}
      | c = By choice of $Y_0$
}}
{{eqn | r = \map \rho {Y_0}
      | c = As $Y_0 \in \mathscr I$
}}
{{end-eqn}}
So it remains  to show:
:$\map \rho {Y_0} = \map \rho X$
===== Case 1 : $Y_0 = X$ =====
Let $Y_0 = X$.
Then:
:$\map \rho {Y_0} = \map \rho X$
{{qed|lemma}}
===== Case 2 : $Y_0 \ne X$ =====
Let $Y_0 \ne X$.
Then:
:$Y_0 \subsetneq X$
From Set Difference with Proper Subset:
:$X \setminus Y_0 \ne \O$
By choice of $Y_0$:
:$\forall y \in X \setminus Y_0 : Y_0 \cup \set y \notin \mathscr I$
That is:
:$\forall y \in X \setminus Y_0 : \map \rho {Y_0 \cup \set y} \ne \card {Y_0 \cup \set y}$
From Lemma 3:
:$\map \rho {Y_0} = \map \rho {Y_0 \cup X} = \map \rho X$
{{qed|lemma}}
In either case:
: $\map \rho {Y_0} = \map \rho X$
It follows that:
:$\forall X \subseteq S : \map {\rho_M} X = \map \rho X$
Hence $\rho$ is the rank function of the matroid $M = \struct{S, \mathscr I}$.
Theorem: Equivalence of Definitions of Purely Inseparable Extension

Let $E / F$ be an algebraic field extension.
{{TFAE|def = Purely Inseparable Field Extension}}

Proof:
{{tidy}}
{{MissingLinks}}
Theorem: Transitivity of Separable Field Extensions

Let $E / K / F$ be a tower of fields.
Let $E / K$ and $K / F$ be separable.
Then $E / F$ is separable.

Proof:
{{ProofWanted|Using Chapter V, $\S4$, Corollary 4.2 of Lang's Algebra}}
Theorem: Separable Degree is At Most Equal To Degree

Let $E / F$ be a finite field extension.
Then $\index E F_s$ is finite, and:
:$\index E F_s \le \index E F$
where:
:$\index E F$ denotes the degree of $E / F$
:$\index E F_s$ denotes the separable degree of $E / F$.

Proof:
{{ProofWanted|Theorem $4.1$ of Lang's Algebra}}
Theorem: Separable Degree of Field Extensions is Multiplicative

Let $E / F / k$ be a tower of fields. Then
:$\index E k_s = \index E F_s \index F k_s$
where $\index E F_s$ denotes the separable degree of $E / F$.

Proof:
If $E / k$ is infinite, both sides are infinite.
Now assume $E / k$ is finite.
Let $L$ be the algebraic closure of  $k$.
Let $\set{\sigma_i}$ be the family of distinct embedding of $F$ to $L$ fixing $k$,
By definition 2 of separable degree, the set $\set{\sigma_i}$ has $\index F k_s$ elements.
For each $i$, let $\set{\tau_{i j}}$ be the family of distinct extensions of $\sigma_i$ to $E$.
We can view $L$ as an algebraic closure of $F$. By definition 2 of separable degree, each $\sigma_i$ has precisely
:$\index E F_s$
extensions to embeddings of $E$ in $L$.
The set of embeddings $\set{\tau_{i j}}$ contains precisely
:$\index E F_s \index F k_s$
elements.
Any embedding of $E$ into $L$ fixing $k$ must be one of the $\tau_{i j}$, and thus we have
:$\index E k_s = \index E F_s \index F k_s$
{{qed}}
Theorem: Steinitz's Theorem

Let $E / F$ be a finite field extension.
{{TFAE}}
:$(1): \quad E / F$ is simple: there exists $\alpha \in E$ such that $E = \map F \alpha$
:$(2): \quad$ there are only finitely many intermediate fields between $E$ and $F$.

Proof:
=== $1$ implies $2$ ===
Suppose $E = F \sqbrk \alpha$ for some $\alpha \in F$.
Let $M$ be any intermediate field between $E$ and $F$.
Let $g$ be the minimal polynomial of $\alpha$ over $M$. Write
:$\ds g = x^ d + \sum _{i \mathop = 0}^{d \mathop - 1} a_ i x^ i$
Let $M'$ be the field extension of $F$ generated by all the coefficients of $g$.
:$M' = F \paren {a_0, \dots, a_{d-1}}$
Then $M' \subseteq M$ by definition of the minimal polynomial over $M$.
Since $g \in M' \sqbrk x$,
$g$ is the minimal polynomial of $\alpha$ over $M'$,
then the degree of $\alpha$ over $M'$ is $d$, but $E = M' \sqbrk \alpha$, so
:$\index E {M'} = d$
similarly, we have $\index E M = d$,
we conclude by Tower Law,
:$\index M {M'} = 1$
hence
:$M = M' = F \paren {a_0, \dots, a_{d-1}}$
Thus it suffices to show there are at most finitely many possibilities for the polynomial $g$. 
Let $f$ be the minimal polynomial of $\alpha$ over $F$,
since $f \in M \sqbrk x$, and $\map f \alpha = 0$,
by definition of $g$,
:$g \divides f$
By unique factorization in $E \sqbrk x$,
the polynomial $f$ has only finitely many divisors in $E \sqbrk x$,
so there are only finitely many intermediate fields between $E$ and $F$.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Separable Degree

Let $E / F$ be a field extension.
{{TFAE|def = Separable Degree}}

Proof:
{{Refactor|level = medium|separate the lemma into its own page for neatness}}
Theorem: Vector Space over an Infinite Field is not equal to the Union of Proper Subspaces

Let $U_1, U_2, \dots, U_n$ be proper subspaces of a vector space $V$ over an infinite field $F$, 
Then $V$ is not equal to the union of $U_1, U_2, \dots, U_n$.

Proof:
{{MissingLinks}}
{{AimForCont}} $V = V_1 \cup \cdots \cup V_n$.
We can assume that $n \geq 2$, and that $m$ is minimal $n$ with this property.
Choose and fix some $y \in V \setminus V_1$.
Let $x \in V_1$.
Since $F$ is infinite field, we can choose a subset $S \subset F$ of size $m+1$.
For each $\alpha \in S$, we can find some
:$\map i \alpha \in \set {1, \cdots, m}$
such that $x+\alpha y \in V_{\map i \alpha}$ because $V = V_1 \cup \cdots \cup V_m$.
The function $i: S \to \set{1, \cdots, m}$ cannot be injective.
So we can find $\alpha \neq \beta$ in $S$ such that $x + \alpha y$ and $x + \beta y$ both lie in $V_{\map i \alpha}$.
But then:
:$y = \dfrac {\paren {x + \alpha y} - \paren {x + \beta y} } {\alpha - \beta} \in V_{\map i \alpha}$
Since $y \notin V_1$ by assumption, we conclude that $\map i \alpha > 1$.
Then:
:$x = \paren {x + \alpha y} - \alpha y \in V_{\map i \alpha} \subseteq V_2 \cup \cdots \cup V_m$
for every $x \in V_1$.
Hence
:$V_1 \subseteq V_2 \cup \cdots \cup V_m$
This implies that $V = V_2 \cup \cdots \cup V_m$, which contradicts the minimality of $m$.
{{finish|Explain why this proves the thesis. The variable names don't match for a start.}}
Theorem: Kinetic Energy of Body at Constant Angular Speed

Let $B$ be a body rotating at an angular speed $\omega$ about some axis of rotation $\LL$.
Let $I$ denote the moment of inertia of $B$ about $\LL$.
Then the kinetic energy $T$ of $B$ brought about by this rotation is given by:
:$T = \dfrac {I \omega^2} 2$

Proof:
=== Discrete Case ===
{{Recall|Moment of Inertia|Discrete Moment of Inertia|subdef = Discrete}}
{{:Definition:Moment of Inertia/Discrete}}
The total kinetic energy of $B$ is equal to the sum of the kinetic energies of every $P_i$.
{{begin-eqn}}
{{eqn | l = K
      | r = \sum_i K_i
}}
{{eqn | r = \sum_i \frac {m_i v_i^2} 2
      | c = Kinetic Energy of Motion
}}
{{eqn | r = \sum_i \frac {m_i \paren {r_i \omega}^2 } 2
      | c = Angular Speed of Particle in Circular Motion at Constant Speed
}}
{{eqn | r = \frac {\omega^2} 2 \sum_i m_i r_i^2
      | c = Indexed Summation of Multiple of Mapping
}}
{{eqn | r = \frac {I \omega^2} 2
      | c = {{Defof|Moment of Inertia (Discrete)}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Outer Jordan Content of Right Triangle

Let $T \subseteq \R^2$ be defined as:
:$T = \set {\tuple {x, y} \in \R^2 : x \ge 0 \land y \ge 0 \land x + y \le 1}$
Then:
:$\map {m^*} T = \dfrac 1 2$
{{explain|notation}}

Proof:
Let $\epsilon > 0$ be arbitrary.
By the Axiom of Archimedes, let $n \in \N$ such that:
:$n > 2 \epsilon$
Define $C \subseteq \powerset {\R^2}$ as:
:$C = \set {\closedint {\dfrac p n} {\dfrac {p + 1} n} \times \closedint {\dfrac q n} {\dfrac {q + 1} n} : p, q \in \set {0, 1, \dotsc, n - 1} \land p + q < n}$
By construction, $C$ is a finite set of closed $2$-rectangles.
Let $\tuple {x, y} \in T$ be arbitrary.
Let $p \in \Z_{\ge 0}$ be the smallest non-negative integer such that:
:$\dfrac {p + 1} n \ge x$
Because:
:$\dfrac {\paren {n - 1} + 1} n = 1 \ge x$
we have:
:$p \le n - 1$
If $\dfrac {p'} n < x$ for any $p' \in \Z_{\ge 0}$, then:
:$\dfrac p n < x$
by minimality.
Otherwise, $p = 0$ as the smallest non-negative integer overall, so:
:$\dfrac p n = 0 \le x$
In either case:
:$\dfrac p n \le x$
In like manner, let $q \in \Z_{\ge 0}$ be the smallest non-negative integer such that:
:$\dfrac {q + 1} n \ge y$
By the same argument as before:
:$\dfrac q n \le y$
We also have:
{{begin-eqn}}
{{eqn | l = \frac {\paren {n - 1 - p} + 1} n
      | r = \frac {n - p} n
}}
{{eqn | r = 1 - \frac p n
}}
{{eqn | o = \ge
      | r = 1 - x
      | c = as $\dfrac p n < x$ by minimality of $p$; in the case where $\dfrac {p + 1} n \ge x$ for all $p$, then $p = 0$, and the step follows from $x \ge 0$ {{improve|too much going on here; separate this out so as to implement this step (or however many steps this actually subsumses) into a more explicit structure, perhaps as a lemma; however it is best implemented; I rather lack the time and inclination to analyse this directly myself}}
}}
{{eqn | o = \ge
      | r = y
      | c = as $x + y \le 1$ {{hypothesis}}
}}
{{eqn | ll = \leadsto
      | l = q
      | o = \le
      | r = n - 1 - p
      | c = by minimality of $q$
}}
{{eqn | ll = \leadsto
      | l = p + q
      | o = \le
      | r = n - 1
}}
{{eqn | o = <
      | r = n
}}
{{end-eqn}}
Therefore:
:$\closedint {\dfrac p n} {\dfrac {p + 1} n} \times \closedint {\dfrac q n} {\dfrac {q + 1} n} \in C$
Since, by the previous inequalities:
:$\dfrac p n \le x \le \dfrac {p + 1} n$
:$\dfrac q n \le y \le \dfrac {q + 1} n$
it follows that:
:$\tuple {x, y} \in \closedint {\dfrac p n} {\dfrac {p + 1} n} \times \closedint {\dfrac q n} {\dfrac {q + 1} n}$
As $\tuple {x, y} \in T$ was arbitrary, we have that $C$ is a covering of $T$.
{{WIP}}
3vb8zt6q13vcf1cgcrszwl4nvb5lmsd
Theorem: Set Difference Then Union Equals Union Then Set Difference

Let $S, A, B$ be sets.
Let $A \cap B = \O$.
Then:
:$\paren {S \setminus A} \cup B = \paren {S \cup B} \setminus A$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \paren {S \cup B} \setminus A
      | r = \paren {S \setminus A} \cup \paren {B \setminus A}
      | c = Set Difference is Right Distributive over Union
}}
{{eqn | r = \paren {S \setminus A} \cup B
      | c = Set Difference with Disjoint Set
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
5jzoc6sxo49gugwyg24m68sow504xks
Theorem: Lagrange Interpolation Formula/Formulation 1

Let $\tuple {x_0, \ldots, x_n}$ and $\tuple {a_0, \ldots, a_n}$ be ordered tuples of real numbers such that $x_i \ne x_j$ for $i \ne j$.
Then there exists a unique polynomial $P \in \R \sqbrk X$ of degree at most $n$ such that:
:$\map P {x_i} = a_i$ for all $i \in \set {0, 1, \ldots, n}$
Moreover $P$ is given by the formula:
:$\ds \map P X = \sum_{j \mathop = 0}^n a_i \map {L_j} X$
where $\map {L_j} X$ is the $j$th Lagrange basis polynomial associated to the $x_i$.

Proof:
Recall the definition:
:$\ds \map {L_j} X = \prod_{\substack {0 \mathop \le i \mathop \le n \\ i \mathop \ne j}} \frac {X - x_i} {x_j - x_i} \in \R \sqbrk X$
{{mistake|Not sure if it's a mistake or a different way of defining it, but {{BookReference|Dictionary of Mathematics|1989|Ephraim J. Borowski|author2 = Jonathan M. Borwein|entry = Lagrange interpolation formula}} has the above wrapped up in another product symbol}}
From this we see that:
:$\map {L_j} {x_i} = \delta_{i j}$
Therefore:
:$\ds \map P{x_i} = \sum_{j \mathop = 0}^n a_i \delta_{i j} = a_i$
Moreover, by Degree of Product of Polynomials over Integral Domain and Degree of Sum of Polynomials, the degree of $P$ as defined above is at most $n$.
It remains to show that the choice of $P$ is unique.
{{AimForCont}} $\tilde P$ is another polynomial with the required properties.
Let $\Delta = P - \tilde P$.
By Degree of Sum of Polynomials, the degree of $\Delta$ is at most $n$.
Now we see that for $i = 0, \ldots, n$:
:$\map \Delta {x_i} = \map P {x_i} - \map {\tilde P} {x_i} = a_i - a_i = 0$
Since {{hypothesis}} the $x_i$ are distinct, $\Delta$ has $n + 1$ distinct zeros in $\R$.
But by {{Corollary|Polynomial Factor Theorem}} this shows that:
:$\ds \map \Delta X = \alpha \prod_{i \mathop = 0}^n \paren {X - x_i}$
If $\alpha \ne 0$, then this shows that the degree of $\Delta$ is $n+1$, a contradiction.
Therefore:
:$\Delta = 0$
and so:
:$P = \tilde P$
This establishes uniqueness.
{{Qed}}
Theorem: Equivalence of Definitions of Matroid Base Axioms/Formulation 1 Iff Formulation 5

Let $S$ be a finite set.
Let $\mathscr B$ be a non-empty set of subsets of $S$.
Then:
:$\mathscr B$ satisfies formulation $1$ of base axiom:
{{:Axiom:Base Axiom (Matroid)/Formulation 1}}
{{iff}}
:$\mathscr B$ satisfies formulation $5$ of base axiom:
{{:Axiom:Base Axiom (Matroid)/Formulation 5}}

Proof:
=== Necessary Condition ===
From:
:* Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom
:* Matroid Bases Satisfy Formulation 4 Base Axiom
formulation $4$ follows from formulation $1$.
We have formulation $5$ follows from formulation $4$.
{{qed|lemma}}
=== Sufficient Condition ===
Let $\mathscr B$ satisfy formulation $5$ base axiom.
Let $\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
From Subsets Satisfy Formulation 5 Matroid Base Axiom Iff Complements Satisfy Formulation 1:
:$\mathscr B^*$ satisfies formulation 1 base axiom.
From Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom:
:there exists a matroid $M^* = \struct{S, \mathscr I^*}$ whose bases is the set:
::$\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
From Matroid Bases Satisfy Formulation 4 Base Axiom:
:$\mathscr B^*$ satisfies formulation $4$ base axiom
By formulation $5$ base axiom:
:$\mathscr B^*$ satisfies formulation $5$ base axiom
From Subsets Satisfy Formulation 1 Matroid Base Axiom Iff Complements Satisfy Formulation 5:
:$\mathscr B$ satisfies formulation 1 base axiom.
Theorem: Matroid Bases Iff Satisfies Matroid Base Axiom

Let $S$ be a finite set.
Let $\mathscr B$ be a non-empty set of subsets of $S$.
Then $\mathscr B$ is the set of bases of a matroid on $S$ {{iff}} $\mathscr B$ satisfies any one of the base axioms:
{{:Axiom:Base Axiom (Matroid)/Formulation 1}}{{:Axiom:Base Axiom (Matroid)/Formulation 2}}{{:Axiom:Base Axiom (Matroid)/Formulation 3}}{{:Axiom:Base Axiom (Matroid)/Formulation 4}}{{:Axiom:Base Axiom (Matroid)/Formulation 5}}{{:Axiom:Base Axiom (Matroid)/Formulation 6}}{{:Axiom:Base Axiom (Matroid)/Formulation 7}}
In which case, $\mathscr B$ satisfies all of the base axioms.

Proof:
Follows immediately from:
:* Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom
:* Equivalence of Definitions of Matroid Base Axioms
{{qed}}
Theorem: Kakutani's Fixed Point Theorem

Let $S \subset \R^n$ be nonempty, compact, and convex.
Let $\Phi : S \to 2^S$ be a correspondence.
Let the following conditions be satisfied:
:$(1): \quad \map \Phi x$ is nonempty and convex for all $x$
:$(2): \quad \map \Phi \cdot$ is upper hemi-continuous
Then $\Phi$ has a fixed point.

Proof:
{{ProofWanted}}
{{Namedfor|Shizuo Kakutani|Kakutani}}
Theorem: Matroid Bases Satisfy Formulation 7 of Matroid Base Axiom

Let $M = \struct{S, \mathscr I}$ be a matroid.
Let $\mathscr B$ be the set of bases of the matroid $M$.
Then $\mathscr B$ satisfies formulation $7$ of base axiom:
{{:Axiom:Base Axiom (Matroid)/Formulation 7}}

Proof:
Let $\mathscr C$ denote the set of circuits of $M$.
From Circuits of Matroid iff Matroid Circuit Axioms, $\mathscr C$ satisifies:
:{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}
Theorem: Bonnet's Recursion Formula

Let $\map {P_n} x$ denote the Legendre polynomial of order $n$.
'''Bonnet's Recursion Formula''' states:
:$\paren {n + 1} \map {P_{n + 1} } x = \paren {2 n + 1} x \map {P_n} x - n \map {P_{n - 1} } x$

Proof:
From Generating Function for Legendre Polynomials, the generating function for $P_n$ is:
:$(1): \quad \ds \frac 1 {\sqrt {1 - 2 x t + t^2} } = \sum_{n \mathop = 0}^\infty \map {P_n} x t^n$
Differentiating both sides of $(1)$ {{WRT|Differentiation}} $t$:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d t} } {\paren {1 - 2 x t + t^2 }^{-1/2} }
      | r = \map {\dfrac \d {\d t} } {\sum_{n \mathop = 0}^\infty \map {P_n} x t^n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\dfrac 1 2 \paren {-2 x + 2 t} \paren {1 - 2 x t + t^2 }^{-3/2}
      | r = \sum_{n \mathop = 0}^\infty \map {\dfrac \d {\d t} } {\map {P_n} x t^n}
      | c = Derivative of Power, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - t} {\sqrt {1 - 2 x t + t^2} }
      | r = \paren {1 - 2 x t + t^2} \sum_{n \mathop = 1}^\infty n \map {P_n} x t^{n - 1}
      | c = Derivative of Power and multiplying both sides by $1 - 2 x t + t^2$
}}
{{eqn | ll= \leadsto
      | l = \paren {x - t} \sum_{n \mathop = 0}^\infty \map {P_n} x t^n
      | r = \paren {1 - 2 x t + t^2} \sum_{n \mathop = 1}^\infty n \map {P_n} x t^{n - 1}
      | c = substituting $\ds \sum_{n \mathop = 0}^\infty \map {P_n} x t^n$ for $\dfrac 1 {\sqrt {1 - 2 x t + t^2} }$ from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \paren {x - t} \sum_{n \mathop = 0}^\infty \map {P_n} x t^n
      | r = \paren {1 - 2 x t + t^2} \sum_{n \mathop = 0}^\infty \paren {n + 1} \map {P_{n + 1} } x t^n
      | c = Translation of Index Variable of Summation in {{RHS}}
}}
{{end-eqn}}
Equating coefficients of $t^n$:
{{begin-eqn}}
{{eqn | l = x \map {P_n} x - \map {P_{n - 1} } x
      | r = \paren {n + 1} \map {P_{n + 1} } x - 2 x n \map {P_n} x + \paren {n - 1} \map {P_{n - 1} } x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {n + 1} \map {P_{n + 1} } x
      | r = x \map {P_n} x - \map {P_{n - 1} } x + 2 x n \map {P_n} x - \paren {n - 1} \map {P_{n - 1} } x
      | c = rearranging
}}
{{eqn | r = \paren {2 n + 1} x \map {P_n} x - n \map {P_{n - 1} } x
      | c = simplifying
}}
{{end-eqn}}
Hence the result.
{{qed}}