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	⊢ ( ( 𝑅 ≃𝑚 𝑆 ∧ 𝑆 ≃𝑚 𝑇 ) → 𝑅 ≃𝑚 𝑇 )