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 ∧ 𝑆𝐽𝑇𝐽 ) → 𝑆𝑇 )