lmicsym

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

		Ref	Expression
	Assertion	lmicsym	$⊢ R ≃_{𝑚} S \to S ≃_{𝑚} R$

Step	Hyp	Ref	Expression
1		brlmic	$⊢ R ≃_{𝑚} S \leftrightarrow R LMIso S \neq \emptyset$
2		n0	$⊢ R LMIso S \neq \emptyset \leftrightarrow \exists f f \in (R LMIso S)$
3		lmimcnv	$⊢ f \in (R LMIso S) \to f^{-1} \in (S LMIso R)$
4		brlmici	$⊢ f^{-1} \in (S LMIso R) \to S ≃_{𝑚} R$
5	3 4	syl	$⊢ f \in (R LMIso S) \to S ≃_{𝑚} R$
6	5	exlimiv	$⊢ \exists f f \in (R LMIso S) \to S ≃_{𝑚} R$
7	2 6	sylbi	$⊢ R LMIso S \neq \emptyset \to S ≃_{𝑚} R$
8	1 7	sylbi	$⊢ R ≃_{𝑚} S \to S ≃_{𝑚} R$

Metamath Proof Explorer