Metamath Proof Explorer

Theorem lmimco

Description: The composition of two isomorphisms of modules is an isomorphism of modules. (Contributed by AV, 10-Mar-2019)

Ref Expression
Assertion lmimco 
|- ( ( F e. ( S LMIso T ) /\ G e. ( R LMIso S ) ) -> ( F o. G ) e. ( R LMIso T ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` S ) = ( Base ` S )
2 eqid 
 |-  ( Base ` T ) = ( Base ` T )
3 1 2 islmim 
 |-  ( F e. ( S LMIso T ) <-> ( F e. ( S LMHom T ) /\ F : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 1 islmim 
 |-  ( G e. ( R LMIso S ) <-> ( G e. ( R LMHom S ) /\ G : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
6 lmhmco 
 |-  ( ( F e. ( S LMHom T ) /\ G e. ( R LMHom S ) ) -> ( F o. G ) e. ( R LMHom T ) )
7 6 ad2ant2r 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) /\ ( G e. ( R LMHom S ) /\ G : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) ) -> ( F o. G ) e. ( R LMHom T ) )
8 f1oco 
 |-  ( ( F : ( Base ` S ) -1-1-onto-> ( Base ` T ) /\ G : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) -> ( F o. G ) : ( Base ` R ) -1-1-onto-> ( Base ` T ) )
9 8 ad2ant2l 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) /\ ( G e. ( R LMHom S ) /\ G : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) ) -> ( F o. G ) : ( Base ` R ) -1-1-onto-> ( Base ` T ) )
10 4 2 islmim 
 |-  ( ( F o. G ) e. ( R LMIso T ) <-> ( ( F o. G ) e. ( R LMHom T ) /\ ( F o. G ) : ( Base ` R ) -1-1-onto-> ( Base ` T ) ) )
11 7 9 10 sylanbrc 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) /\ ( G e. ( R LMHom S ) /\ G : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) ) -> ( F o. G ) e. ( R LMIso T ) )
12 3 5 11 syl2anb 
 |-  ( ( F e. ( S LMIso T ) /\ G e. ( R LMIso S ) ) -> ( F o. G ) e. ( R LMIso T ) )