Metamath Proof Explorer

Theorem lmhmlvec

Description: The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023)

Ref Expression
Assertion lmhmlvec 
|- ( F e. ( S LMHom T ) -> ( S e. LVec <-> T e. LVec ) )

Proof

Step Hyp Ref Expression
1 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
2 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
3 1 2 2thd 
 |-  ( F e. ( S LMHom T ) -> ( S e. LMod <-> T e. LMod ) )
4 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
5 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
6 4 5 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) )
7 6 eqcomd 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` S ) = ( Scalar ` T ) )
8 7 eleq1d 
 |-  ( F e. ( S LMHom T ) -> ( ( Scalar ` S ) e. DivRing <-> ( Scalar ` T ) e. DivRing ) )
9 3 8 anbi12d 
 |-  ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ ( Scalar ` S ) e. DivRing ) <-> ( T e. LMod /\ ( Scalar ` T ) e. DivRing ) ) )
10 4 islvec 
 |-  ( S e. LVec <-> ( S e. LMod /\ ( Scalar ` S ) e. DivRing ) )
11 5 islvec 
 |-  ( T e. LVec <-> ( T e. LMod /\ ( Scalar ` T ) e. DivRing ) )
12 9 10 11 3bitr4g 
 |-  ( F e. ( S LMHom T ) -> ( S e. LVec <-> T e. LVec ) )