Theorem lmicsym

Description: Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Assertion	lmicsym	⊢ ( 𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		brlmic	⊢ ( 𝑅 ≃𝑚 𝑆 ↔ ( 𝑅 LMIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝑅 LMIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) )
3		lmimcnv	⊢ ( 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → ◡ 𝑓 ∈ ( 𝑆 LMIso 𝑅 ) )
4		brlmici	⊢ ( ◡ 𝑓 ∈ ( 𝑆 LMIso 𝑅 ) → 𝑆 ≃𝑚 𝑅 )
5	3 4	syl	⊢ ( 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑆 ≃𝑚 𝑅 )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 LMIso 𝑆 ) → 𝑆 ≃𝑚 𝑅 )
7	2 6	sylbi	⊢ ( ( 𝑅 LMIso 𝑆 ) ≠ ∅ → 𝑆 ≃𝑚 𝑅 )
8	1 7	sylbi	⊢ ( 𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅 )