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

Metamath Proof Explorer

Theorem lmicdim

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

Ref Expression
Hypotheses lmicdim.1 
|- ( ph -> S ~=m T )
lmicdim.2 
|- ( ph -> S e. LVec )
Assertion lmicdim 
|- ( ph -> ( dim ` S ) = ( dim ` T ) )

Proof

Step Hyp Ref Expression
1 lmicdim.1 
 |-  ( ph -> S ~=m T )
2 lmicdim.2 
 |-  ( ph -> S e. LVec )
3 brlmic 
 |-  ( S ~=m T <-> ( S LMIso T ) =/= (/) )
4 1 3 sylib 
 |-  ( ph -> ( S LMIso T ) =/= (/) )
5 n0 
 |-  ( ( S LMIso T ) =/= (/) <-> E. f f e. ( S LMIso T ) )
6 4 5 sylib 
 |-  ( ph -> E. f f e. ( S LMIso T ) )
7 simpr 
 |-  ( ( ph /\ f e. ( S LMIso T ) ) -> f e. ( S LMIso T ) )
8 2 adantr 
 |-  ( ( ph /\ f e. ( S LMIso T ) ) -> S e. LVec )
9 7 8 lmimdim 
 |-  ( ( ph /\ f e. ( S LMIso T ) ) -> ( dim ` S ) = ( dim ` T ) )
10 6 9 exlimddv 
 |-  ( ph -> ( dim ` S ) = ( dim ` T ) )