This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lvecdimfi

Description: Finite version of lvecdim which does not require the axiom of choice. The axiom of choice is used in acsmapd , which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023)

Ref Expression
Hypotheses lvecdimfi.j 
|- J = ( LBasis ` W )
lvecdimfi.w 
|- ( ph -> W e. LVec )
lvecdimfi.s 
|- ( ph -> S e. J )
lvecdimfi.t 
|- ( ph -> T e. J )
lvecdimfi.f 
|- ( ph -> S e. Fin )
Assertion lvecdimfi 
|- ( ph -> S ~~ T )

Proof

Step Hyp Ref Expression
1 lvecdimfi.j 
 |-  J = ( LBasis ` W )
2 lvecdimfi.w 
 |-  ( ph -> W e. LVec )
3 lvecdimfi.s 
 |-  ( ph -> S e. J )
4 lvecdimfi.t 
 |-  ( ph -> T e. J )
5 lvecdimfi.f 
 |-  ( ph -> S e. Fin )
6 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
7 eqid 
 |-  ( mrCls ` ( LSubSp ` W ) ) = ( mrCls ` ( LSubSp ` W ) )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 6 7 8 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 } ) ) ) )
10 2 9 syl 
 |-  ( ph -> ( ( 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 } ) ) ) )
11 10 simpld 
 |-  ( ph -> ( LSubSp ` W ) e. ( ACS ` ( Base ` W ) ) )
12 11 acsmred 
 |-  ( ph -> ( LSubSp ` W ) e. ( Moore ` ( Base ` W ) ) )
13 eqid 
 |-  ( mrInd ` ( LSubSp ` W ) ) = ( mrInd ` ( LSubSp ` W ) )
14 10 simprd 
 |-  ( ph -> 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 } ) ) )
15 6 7 8 13 1 lbsacsbs 
 |-  ( W e. LVec -> ( S e. J <-> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) ) )
16 15 biimpa 
 |-  ( ( W e. LVec /\ S e. J ) -> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) )
17 2 3 16 syl2anc 
 |-  ( ph -> ( S e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) ) )
18 17 simpld 
 |-  ( ph -> S e. ( mrInd ` ( LSubSp ` W ) ) )
19 6 7 8 13 1 lbsacsbs 
 |-  ( W e. LVec -> ( T e. J <-> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) ) )
20 19 biimpa 
 |-  ( ( W e. LVec /\ T e. J ) -> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) )
21 2 4 20 syl2anc 
 |-  ( ph -> ( T e. ( mrInd ` ( LSubSp ` W ) ) /\ ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) ) )
22 21 simpld 
 |-  ( ph -> T e. ( mrInd ` ( LSubSp ` W ) ) )
23 17 simprd 
 |-  ( ph -> ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( Base ` W ) )
24 21 simprd 
 |-  ( ph -> ( ( mrCls ` ( LSubSp ` W ) ) ` T ) = ( Base ` W ) )
25 23 24 eqtr4d 
 |-  ( ph -> ( ( mrCls ` ( LSubSp ` W ) ) ` S ) = ( ( mrCls ` ( LSubSp ` W ) ) ` T ) )
26 12 7 13 14 18 22 5 25 mreexfidimd 
 |-  ( ph -> S ~~ T )