This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmictra

Description: Module isomorphism is transitive. (Contributed by AV, 10-Mar-2019)

Ref Expression
Assertion lmictra ( ( 𝑅 ≃𝑚 𝑆 ∧ 𝑆 ≃𝑚 𝑇 ) → 𝑅 ≃𝑚 𝑇 )

Proof

Step Hyp Ref Expression
1 brlmic ⊢ ( 𝑅 ≃𝑚 𝑆 ↔ ( 𝑅 LMIso 𝑆 ) ≠ ∅ )
2 brlmic ⊢ ( 𝑆 ≃𝑚 𝑇 ↔ ( 𝑆 LMIso 𝑇 ) ≠ ∅ )
3 n0 ⊢ ( ( 𝑅 LMIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) )
4 n0 ⊢ ( ( 𝑆 LMIso 𝑇 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) )
5 lmimco ⊢ ( ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 LMIso 𝑇 ) )
6 brlmici ⊢ ( ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 LMIso 𝑇 ) → 𝑅 ≃𝑚 𝑇 )
7 5 6 syl ⊢ ( ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) ) → 𝑅 ≃𝑚 𝑇 )
8 7 ex ⊢ ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑅 ≃𝑚 𝑇 ) )
9 8 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑅 ≃𝑚 𝑇 ) )
10 9 com12 ⊢ ( 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → 𝑅 ≃𝑚 𝑇 ) )
11 10 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → 𝑅 ≃𝑚 𝑇 ) )
12 11 imp ⊢ ( ( ∃ 𝑔 𝑔 ∈ ( 𝑅 LMIso 𝑆 ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) ) → 𝑅 ≃𝑚 𝑇 )
13 3 4 12 syl2anb ⊢ ( ( ( 𝑅 LMIso 𝑆 ) ≠ ∅ ∧ ( 𝑆 LMIso 𝑇 ) ≠ ∅ ) → 𝑅 ≃𝑚 𝑇 )
14 1 2 13 syl2anb ⊢ ( ( 𝑅 ≃𝑚 𝑆 ∧ 𝑆 ≃𝑚 𝑇 ) → 𝑅 ≃𝑚 𝑇 )