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 ( 𝑅𝑚 𝑆𝑅 ∈ LMod )

Proof

Step Hyp Ref Expression
1 brlmic ( 𝑅𝑚 𝑆 ↔ ( 𝑅 LMIso 𝑆 ) ≠ ∅ )
2 n0 ( ( 𝑅 LMIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) )
3 1 2 bitri ( 𝑅𝑚 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) )
4 lmimlmhm ( 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑓 ∈ ( 𝑅 LMHom 𝑆 ) )
5 lmhmlmod1 ( 𝑓 ∈ ( 𝑅 LMHom 𝑆 ) → 𝑅 ∈ LMod )
6 4 5 syl ( 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑅 ∈ LMod )
7 6 exlimiv ( ∃ 𝑓 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑅 ∈ LMod )
8 3 7 sylbi ( 𝑅𝑚 𝑆𝑅 ∈ LMod )