rictr

Description: Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025)

		Ref	Expression
	Assertion	rictr	$⊢ (R ≃_{𝑟} S \land S ≃_{𝑟} T) \to R ≃_{𝑟} T$

Step	Hyp	Ref	Expression
1		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
2		brric	$⊢ S ≃_{𝑟} T \leftrightarrow S RingIso T \neq \emptyset$
3		n0	$⊢ R RingIso S \neq \emptyset \leftrightarrow \exists f f \in (R RingIso S)$
4		n0	$⊢ S RingIso T \neq \emptyset \leftrightarrow \exists g g \in (S RingIso T)$
5		exdistrv	$⊢ \exists f \exists g (f \in (R RingIso S) \land g \in (S RingIso T)) \leftrightarrow (\exists f f \in (R RingIso S) \land \exists g g \in (S RingIso T))$
6		rimco	$⊢ (g \in (S RingIso T) \land f \in (R RingIso S)) \to g \circ f \in (R RingIso T)$
7		brrici	$⊢ g \circ f \in (R RingIso T) \to R ≃_{𝑟} T$
8	6 7	syl	$⊢ (g \in (S RingIso T) \land f \in (R RingIso S)) \to R ≃_{𝑟} T$
9	8	ancoms	$⊢ (f \in (R RingIso S) \land g \in (S RingIso T)) \to R ≃_{𝑟} T$
10	9	exlimivv	$⊢ \exists f \exists g (f \in (R RingIso S) \land g \in (S RingIso T)) \to R ≃_{𝑟} T$
11	5 10	sylbir	$⊢ (\exists f f \in (R RingIso S) \land \exists g g \in (S RingIso T)) \to R ≃_{𝑟} T$
12	3 4 11	syl2anb	$⊢ (R RingIso S \neq \emptyset \land S RingIso T \neq \emptyset) \to R ≃_{𝑟} T$
13	1 2 12	syl2anb	$⊢ (R ≃_{𝑟} S \land S ≃_{𝑟} T) \to R ≃_{𝑟} T$

Metamath Proof Explorer