Metamath Proof Explorer

Theorem lmhmclm

Description: The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015)

Ref Expression
Assertion lmhmclm 
|- ( F e. ( S LMHom T ) -> ( S e. CMod <-> T e. CMod ) )

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 fveq2d 
 |-  ( F e. ( S LMHom T ) -> ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` T ) ) )
9 8 oveq2d 
 |-  ( F e. ( S LMHom T ) -> ( CCfld |`s ( Base ` ( Scalar ` S ) ) ) = ( CCfld |`s ( Base ` ( Scalar ` T ) ) ) )
10 7 9 eqeq12d 
 |-  ( F e. ( S LMHom T ) -> ( ( Scalar ` S ) = ( CCfld |`s ( Base ` ( Scalar ` S ) ) ) <-> ( Scalar ` T ) = ( CCfld |`s ( Base ` ( Scalar ` T ) ) ) ) )
11 8 eleq1d 
 |-  ( F e. ( S LMHom T ) -> ( ( Base ` ( Scalar ` S ) ) e. ( SubRing ` CCfld ) <-> ( Base ` ( Scalar ` T ) ) e. ( SubRing ` CCfld ) ) )
12 3 10 11 3anbi123d 
 |-  ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ ( Scalar ` S ) = ( CCfld |`s ( Base ` ( Scalar ` S ) ) ) /\ ( Base ` ( Scalar ` S ) ) e. ( SubRing ` CCfld ) ) <-> ( T e. LMod /\ ( Scalar ` T ) = ( CCfld |`s ( Base ` ( Scalar ` T ) ) ) /\ ( Base ` ( Scalar ` T ) ) e. ( SubRing ` CCfld ) ) ) )
13 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
14 4 13 isclm 
 |-  ( S e. CMod <-> ( S e. LMod /\ ( Scalar ` S ) = ( CCfld |`s ( Base ` ( Scalar ` S ) ) ) /\ ( Base ` ( Scalar ` S ) ) e. ( SubRing ` CCfld ) ) )
15 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
16 5 15 isclm 
 |-  ( T e. CMod <-> ( T e. LMod /\ ( Scalar ` T ) = ( CCfld |`s ( Base ` ( Scalar ` T ) ) ) /\ ( Base ` ( Scalar ` T ) ) e. ( SubRing ` CCfld ) ) )
17 12 14 16 3bitr4g 
 |-  ( F e. ( S LMHom T ) -> ( S e. CMod <-> T e. CMod ) )