ricsym

Description: Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025)

		Ref	Expression
	Assertion	ricsym	$⊢ R ≃_{𝑟} S \to S ≃_{𝑟} R$

Step	Hyp	Ref	Expression
1		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
2		n0	$⊢ R RingIso S \neq \emptyset \leftrightarrow \exists f f \in (R RingIso S)$
3		rimcnv	$⊢ f \in (R RingIso S) \to f^{-1} \in (S RingIso R)$
4		brrici	$⊢ f^{-1} \in (S RingIso R) \to S ≃_{𝑟} R$
5	3 4	syl	$⊢ f \in (R RingIso S) \to S ≃_{𝑟} R$
6	5	exlimiv	$⊢ \exists f f \in (R RingIso S) \to S ≃_{𝑟} R$
7	2 6	sylbi	$⊢ R RingIso S \neq \emptyset \to S ≃_{𝑟} R$
8	1 7	sylbi	$⊢ R ≃_{𝑟} S \to S ≃_{𝑟} R$

Metamath Proof Explorer