lvecdim

Description: The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex and lbsacsbs to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd . (Contributed by David Moews, 1-May-2017)

		Ref	Expression
	Hypothesis	lvecdim.1	$⊢ J = LBasis (W)$
	Assertion	lvecdim	$⊢ (W \in LVec \land S \in J \land T \in J) \to S \approx T$

Proof

Step	Hyp	Ref	Expression
1		lvecdim.1	$⊢ J = LBasis (W)$
2		eqid	$⊢ LSubSp (W) = LSubSp (W)$
3		eqid	$⊢ mrCls (LSubSp (W)) = mrCls (LSubSp (W))$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5	2 3 4	lssacsex	$⊢ W \in LVec \to (LSubSp (W) \in ACS ({Base}_{W}) \land \forall x \in 𝒫 {Base}_{W} \forall y \in {Base}_{W} \forall z \in (mrCls (LSubSp (W)) (x \cup \{y\}) ∖ mrCls (LSubSp (W)) (x)) y \in mrCls (LSubSp (W)) (x \cup \{z\}))$
6	5	3ad2ant1	$⊢ (W \in LVec \land S \in J \land T \in J) \to (LSubSp (W) \in ACS ({Base}_{W}) \land \forall x \in 𝒫 {Base}_{W} \forall y \in {Base}_{W} \forall z \in (mrCls (LSubSp (W)) (x \cup \{y\}) ∖ mrCls (LSubSp (W)) (x)) y \in mrCls (LSubSp (W)) (x \cup \{z\}))$
7	6	simpld	$⊢ (W \in LVec \land S \in J \land T \in J) \to LSubSp (W) \in ACS ({Base}_{W})$
8		eqid	$⊢ mrInd (LSubSp (W)) = mrInd (LSubSp (W))$
9	6	simprd	$⊢ (W \in LVec \land S \in J \land T \in J) \to \forall x \in 𝒫 {Base}_{W} \forall y \in {Base}_{W} \forall z \in (mrCls (LSubSp (W)) (x \cup \{y\}) ∖ mrCls (LSubSp (W)) (x)) y \in mrCls (LSubSp (W)) (x \cup \{z\})$
10		simp2	$⊢ (W \in LVec \land S \in J \land T \in J) \to S \in J$
11	2 3 4 8 1	lbsacsbs	$⊢ W \in LVec \to (S \in J \leftrightarrow (S \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (S) = {Base}_{W}))$
12	11	3ad2ant1	$⊢ (W \in LVec \land S \in J \land T \in J) \to (S \in J \leftrightarrow (S \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (S) = {Base}_{W}))$
13	10 12	mpbid	$⊢ (W \in LVec \land S \in J \land T \in J) \to (S \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (S) = {Base}_{W})$
14	13	simpld	$⊢ (W \in LVec \land S \in J \land T \in J) \to S \in mrInd (LSubSp (W))$
15		simp3	$⊢ (W \in LVec \land S \in J \land T \in J) \to T \in J$
16	2 3 4 8 1	lbsacsbs	$⊢ W \in LVec \to (T \in J \leftrightarrow (T \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (T) = {Base}_{W}))$
17	16	3ad2ant1	$⊢ (W \in LVec \land S \in J \land T \in J) \to (T \in J \leftrightarrow (T \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (T) = {Base}_{W}))$
18	15 17	mpbid	$⊢ (W \in LVec \land S \in J \land T \in J) \to (T \in mrInd (LSubSp (W)) \land mrCls (LSubSp (W)) (T) = {Base}_{W})$
19	18	simpld	$⊢ (W \in LVec \land S \in J \land T \in J) \to T \in mrInd (LSubSp (W))$
20	13	simprd	$⊢ (W \in LVec \land S \in J \land T \in J) \to mrCls (LSubSp (W)) (S) = {Base}_{W}$
21	18	simprd	$⊢ (W \in LVec \land S \in J \land T \in J) \to mrCls (LSubSp (W)) (T) = {Base}_{W}$
22	20 21	eqtr4d	$⊢ (W \in LVec \land S \in J \land T \in J) \to mrCls (LSubSp (W)) (S) = mrCls (LSubSp (W)) (T)$
23	7 3 8 9 14 19 22	acsexdimd	$⊢ (W \in LVec \land S \in J \land T \in J) \to S \approx T$

Metamath Proof Explorer

Theorem lvecdim

Proof