Metamath Proof Explorer

Theorem 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 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion lvecdim ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ≈ 𝑇 )

Proof

Step Hyp Ref Expression
1 lvecdim.1 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
3 eqid ⊢ ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrCls ‘ ( LSubSp ‘ 𝑊 ) )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 2 3 4 lssacsex ⊢ ( 𝑊 ∈ LVec → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) )
7 6 simpld ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) )
8 eqid ⊢ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrInd ‘ ( LSubSp ‘ 𝑊 ) )
9 6 simprd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) )
10 simp2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 )
11 2 3 4 8 1 lbsacsbs ⊢ ( 𝑊 ∈ LVec → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) )
12 11 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) )
13 10 12 mpbid ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) )
14 13 simpld ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) )
15 simp3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ 𝐽 )
16 2 3 4 8 1 lbsacsbs ⊢ ( 𝑊 ∈ LVec → ( 𝑇 ∈ 𝐽 ↔ ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) )
17 16 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑇 ∈ 𝐽 ↔ ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) )
18 15 17 mpbid ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) )
19 18 simpld ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) )
20 13 simprd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) )
21 18 simprd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) )
22 20 21 eqtr4d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) )
23 7 3 8 9 14 19 22 acsexdimd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ≈ 𝑇 )