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 
|- J = ( LBasis ` W )
Assertion lvecdim 
|- ( ( W e. LVec /\ S e. J /\ T e. J ) -> S ~~ 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 e. LVec -> ( ( LSubSp ` W ) e. ( ACS ` ( Base ` W ) ) /\ A. x e. ~P ( Base ` W ) A. y e. ( Base ` W ) A. z e. ( ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` W ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { z } ) ) ) )
6 5 3ad2ant1 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( ( LSubSp ` W ) e. ( ACS ` ( Base ` W ) ) /\ A. x e. ~P ( Base ` W ) A. y e. ( Base ` W ) A. z e. ( ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` W ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { z } ) ) ) )
7 6 simpld 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( LSubSp ` W ) e. ( ACS ` ( Base ` W ) ) )
8 eqid 
 |-  ( mrInd ` ( LSubSp ` W ) ) = ( mrInd ` ( LSubSp ` W ) )
9 6 simprd 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> A. x e. ~P ( Base ` W ) A. y e. ( Base ` W ) A. z e. ( ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` W ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` W ) ) ` ( x u. { z } ) ) )
10 simp2 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> S e. J )
11 2 3 4 8 1 lbsacsbs 
 |-  ( W e. LVec -> ( S e. J <-> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) ) )
12 11 3ad2ant1 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( S e. J <-> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) ) )
13 10 12 mpbid 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) )
14 13 simpld 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> S e. ( mrInd ` ( LSubSp ` W ) ) )
15 simp3 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> T e. J )
16 2 3 4 8 1 lbsacsbs 
 |-  ( W e. LVec -> ( T e. J <-> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) ) )
17 16 3ad2ant1 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( T e. J <-> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) ) )
18 15 17 mpbid 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) )
19 18 simpld 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> T e. ( mrInd ` ( LSubSp ` W ) ) )
20 13 simprd 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) )
21 18 simprd 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) )
22 20 21 eqtr4d 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( ( mrCls ` ( LSubSp ` W ) ) ` T ) )
23 7 3 8 9 14 19 22 acsexdimd 
 |-  ( ( W e. LVec /\ S e. J /\ T e. J ) -> S ~~ T )