Metamath Proof Explorer

Theorem lmimdim

Description: Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses lmimdim.1 
|- ( ph -> F e. ( S LMIso T ) )
lmimdim.2 
|- ( ph -> S e. LVec )
Assertion lmimdim 
|- ( ph -> ( dim ` S ) = ( dim ` T ) )

Proof

Step Hyp Ref Expression
1 lmimdim.1 
 |-  ( ph -> F e. ( S LMIso T ) )
2 lmimdim.2 
 |-  ( ph -> S e. LVec )
3 eqid 
 |-  ( LBasis ` S ) = ( LBasis ` S )
4 3 lbsex 
 |-  ( S e. LVec -> ( LBasis ` S ) =/= (/) )
5 2 4 syl 
 |-  ( ph -> ( LBasis ` S ) =/= (/) )
6 n0 
 |-  ( ( LBasis ` S ) =/= (/) <-> E. b b e. ( LBasis ` S ) )
7 5 6 sylib 
 |-  ( ph -> E. b b e. ( LBasis ` S ) )
8 1 adantr 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> F e. ( S LMIso T ) )
9 8 resexd 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( F |` b ) e. _V )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 eqid 
 |-  ( Base ` T ) = ( Base ` T )
12 10 11 lmimf1o 
 |-  ( F e. ( S LMIso T ) -> F : ( Base ` S ) -1-1-onto-> ( Base ` T ) )
13 f1of1 
 |-  ( F : ( Base ` S ) -1-1-onto-> ( Base ` T ) -> F : ( Base ` S ) -1-1-> ( Base ` T ) )
14 8 12 13 3syl 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> F : ( Base ` S ) -1-1-> ( Base ` T ) )
15 10 3 lbsss 
 |-  ( b e. ( LBasis ` S ) -> b C_ ( Base ` S ) )
16 15 adantl 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> b C_ ( Base ` S ) )
17 f1ssres 
 |-  ( ( F : ( Base ` S ) -1-1-> ( Base ` T ) /\ b C_ ( Base ` S ) ) -> ( F |` b ) : b -1-1-> ( Base ` T ) )
18 14 16 17 syl2anc 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( F |` b ) : b -1-1-> ( Base ` T ) )
19 hashf1dmrn 
 |-  ( ( ( F |` b ) e. _V /\ ( F |` b ) : b -1-1-> ( Base ` T ) ) -> ( # ` b ) = ( # ` ran ( F |` b ) ) )
20 9 18 19 syl2anc 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( # ` b ) = ( # ` ran ( F |` b ) ) )
21 df-ima 
 |-  ( F " b ) = ran ( F |` b )
22 21 fveq2i 
 |-  ( # ` ( F " b ) ) = ( # ` ran ( F |` b ) )
23 20 22 eqtr4di 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( # ` b ) = ( # ` ( F " b ) ) )
24 3 dimval 
 |-  ( ( S e. LVec /\ b e. ( LBasis ` S ) ) -> ( dim ` S ) = ( # ` b ) )
25 2 24 sylan 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( dim ` S ) = ( # ` b ) )
26 lmimlmhm 
 |-  ( F e. ( S LMIso T ) -> F e. ( S LMHom T ) )
27 1 26 syl 
 |-  ( ph -> F e. ( S LMHom T ) )
28 lmhmlvec 
 |-  ( F e. ( S LMHom T ) -> ( S e. LVec <-> T e. LVec ) )
29 28 biimpa 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LVec ) -> T e. LVec )
30 27 2 29 syl2anc 
 |-  ( ph -> T e. LVec )
31 30 adantr 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> T e. LVec )
32 eqid 
 |-  ( LBasis ` T ) = ( LBasis ` T )
33 3 32 lmimlbs 
 |-  ( ( F e. ( S LMIso T ) /\ b e. ( LBasis ` S ) ) -> ( F " b ) e. ( LBasis ` T ) )
34 1 33 sylan 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( F " b ) e. ( LBasis ` T ) )
35 32 dimval 
 |-  ( ( T e. LVec /\ ( F " b ) e. ( LBasis ` T ) ) -> ( dim ` T ) = ( # ` ( F " b ) ) )
36 31 34 35 syl2anc 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( dim ` T ) = ( # ` ( F " b ) ) )
37 23 25 36 3eqtr4d 
 |-  ( ( ph /\ b e. ( LBasis ` S ) ) -> ( dim ` S ) = ( dim ` T ) )
38 7 37 exlimddv 
 |-  ( ph -> ( dim ` S ) = ( dim ` T ) )