Metamath Proof Explorer


Theorem lmicrcl

Description: Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion lmicrcl
|- ( R ~=m S -> S e. LMod )

Proof

Step Hyp Ref Expression
1 brlmic
 |-  ( R ~=m S <-> ( R LMIso S ) =/= (/) )
2 n0
 |-  ( ( R LMIso S ) =/= (/) <-> E. f f e. ( R LMIso S ) )
3 1 2 bitri
 |-  ( R ~=m S <-> E. f f e. ( R LMIso S ) )
4 lmimlmhm
 |-  ( f e. ( R LMIso S ) -> f e. ( R LMHom S ) )
5 lmhmlmod2
 |-  ( f e. ( R LMHom S ) -> S e. LMod )
6 4 5 syl
 |-  ( f e. ( R LMIso S ) -> S e. LMod )
7 6 exlimiv
 |-  ( E. f f e. ( R LMIso S ) -> S e. LMod )
8 3 7 sylbi
 |-  ( R ~=m S -> S e. LMod )