Matroid Bases Satisfy Formulation 7 of Matroid Base Axiom

== Theorem ==
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:
== Proof ==
Let $\mathscr C$ denote the set of circuits of $M$.
From Circuits of Matroid iff Matroid Circuit Axioms, $\mathscr C$ satisifies:
:
=== Lemma 1 ===
</onlyinclude>
Let $B_1, B_2 \in \mathscr B$.
From Matroid Base Union External Element has Fundamental Circuit:
:for each $x \in B_1 \setminus B_2$ let $C_x$ denote the fundamental circuit of $x$ in $B_2$
By definition of the fundamental circuit of $x$ in $B_2$:
:$\forall y \in B_1 \setminus B_2 : y \ne x: x \notin C_y$
It follows that:
:$\forall x \in B_1 \setminus B_2: C_x \nsubseteq \ds \bigcup_{y \ne x} C_y$
Hence lemma 1 can be applied to $\set{C_x : x \in B_1 \setminus B_2}$
For each $x \in B_1 \setminus B_2$ let:
:$(1): \quad C^\prime_x = C_x \cap \paren{B_2 \setminus B_1}$
From Subset Intersection Set Difference is Empty Iff Subset of Second Set:
:$C^\prime_x = \O \iff C_x \subseteq B_1$
From Subset of Set Difference iff Disjoint Set:
:$C^\prime_x \ne \O$
From Matroid Base Substitution From Fundamental Circuit:
:$(2): \quad \forall y \in C^\prime_x: \paren{B_2 \setminus \set y} \cup \set x \in \mathscr B$
Consider the set of sets:
:$\set{C^\prime_x : x \in B_1 \setminus B_2}$
 $\set{x_1, \ldots, x_n}$ is a finite subset of $B_1 \setminus B_2$ of cardinality $n$ such that:
:$\size{C^\prime_{x_1} \cup \ldots \cup C^\prime_{x_1}} < n$
Let $D = C^\prime_{x_1} \cup \ldots \cup C^\prime_{x_1}$.
Applying lemma 1 to $\set{C_x : x \in B_1 \setminus B_2}$ and $D$:
:$\exists C \in \mathscr C : C \subseteq \ds \paren{\bigcup_{k =1}^n C_{x_k}} \setminus D$
Note that:
We have:
From Subset Relation is Transitive:
:$C \subseteq B_1$
This contradicts Matroid Base Contains No Circuit.
Hence for all finite $F \subseteq B_1 \setminus B_2$:
:$\size F \le \size{\ds \bigcup_{x \in F} C^\prime_x}$
That is, the indexed family of finite sets $\set{C^\prime_x : x \in B_1 \setminus B_2}$ satisfies the marriage condition.
From Hall's Marriage Theorem:
:there exists an injection $\pi : B_1 \setminus B_2 \to \ds \bigcup_{x \in F} C^\prime_x$ such that:
::$\forall x \in B_1 \setminus B_2: \map \pi x \in C^\prime_x$
From $(1)$ and $(2)$:
:$\forall x \in B_1 \setminus B_2 : \map \pi x \in B_2 \setminus B_1 : \paren{B_2 \setminus \set {\map \pi x}} \cup \set x \in \mathscr B$
We have:
From the contrapositive statement of Cardinality of Proper Subset of Finite Set:
:$\pi \sqbrk {B_1 \setminus B_2} = B_2 \setminus B_1$
Hence:
:$\pi$ is a bijection, $\pi : B_1 \setminus B_2 \to B_2 \setminus B_1$:
::$\forall x \in B_1 \setminus B_2 : \map \pi x \in B_2 \setminus B_1 : \paren{B_2 \setminus \set {\map \pi x}} \cup \set x \in \mathscr B$
Let $\pi^\prime : B_1 \to B_2$ be defined by:
:$\forall x \in B_1 : \map {\pi^\prime} x = \begin{cases}
\map \pi x & : x \in B_1 \setminus B_2\\
x & : x \in B_1 \cap B_2 
\end{cases}$
From Set Difference Union Intersection:
:$B_1 = \paren{B_1 \setminus B_2} \cup \paren{B_1 \cap B_2}$
From Set Difference and Intersection are Disjoint:
:$\paren{B_1 \setminus B_2} \cap \paren{B_1 \cap B_2} = \O$
Hence:
:$\pi^\prime : B_1 \to B_2$ is well-defined
From Set Difference and Intersection are Disjoint:
:$\paren{B_2 \setminus B_1} \cap \paren{B_1 \cap B_2} = \O$
From Union of Bijections with Disjoint Domains and Codomains is Bijection:
:$\pi^\prime$ is a bijection
Furthermore:
:$\forall x \in B_1 : \paren{B_2 \setminus \set {\map {\pi^\prime} x} } \cup \set x = \begin{cases}
\paren{B_2 \setminus \set {\map \pi x} } \cup \set x \in \mathscr B & : x \in B_1 \setminus B_2\\
\paren{B_2 \setminus \set x} \cup \set x = B_2 \in \mathscr B& : x \in B_1 \cap B_2 
\end{cases}$
It follows that $\mathscr B$ satisfies formulation $7$ of base axiom:
== Sources ==
* 
* 
* 
Category:Matroid Bases
Category:Matroid Bases Satisfy Formulation 7 of Matroid Base Axiom