Metamath Proof Explorer


Theorem lmiclcl

Description: Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion lmiclcl R𝑚SRLMod

Proof

Step Hyp Ref Expression
1 brlmic R𝑚SRLMIsoS
2 n0 RLMIsoSffRLMIsoS
3 1 2 bitri R𝑚SffRLMIsoS
4 lmimlmhm fRLMIsoSfRLMHomS
5 lmhmlmod1 fRLMHomSRLMod
6 4 5 syl fRLMIsoSRLMod
7 6 exlimiv ffRLMIsoSRLMod
8 3 7 sylbi R𝑚SRLMod