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 ) )