riscer

Description: Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Assertion	riscer	$⊢ ≃_{𝑟} Er dom ≃_{𝑟}$

Proof

Step	Hyp	Ref	Expression
1		df-risc	$⊢ ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))\}$
2	1	relopabi	$⊢ Rel ≃_{𝑟}$
3		eqid	$⊢ dom ≃_{𝑟} = dom ≃_{𝑟}$
4		vex	$⊢ r \in V$
5		vex	$⊢ s \in V$
6	4 5	isrisc	$⊢ r ≃_{𝑟} s \leftrightarrow ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))$
7		rngoisocnv	$⊢ (r \in RingOps \land s \in RingOps \land f \in (r RngIso s)) \to f^{-1} \in (s RngIso r)$
8	7	3expia	$⊢ (r \in RingOps \land s \in RingOps) \to (f \in (r RngIso s) \to f^{-1} \in (s RngIso r))$
9		risci	$⊢ (s \in RingOps \land r \in RingOps \land f^{-1} \in (s RngIso r)) \to s ≃_{𝑟} r$
10	9	3expia	$⊢ (s \in RingOps \land r \in RingOps) \to (f^{-1} \in (s RngIso r) \to s ≃_{𝑟} r)$
11	10	ancoms	$⊢ (r \in RingOps \land s \in RingOps) \to (f^{-1} \in (s RngIso r) \to s ≃_{𝑟} r)$
12	8 11	syld	$⊢ (r \in RingOps \land s \in RingOps) \to (f \in (r RngIso s) \to s ≃_{𝑟} r)$
13	12	exlimdv	$⊢ (r \in RingOps \land s \in RingOps) \to (\exists f f \in (r RngIso s) \to s ≃_{𝑟} r)$
14	13	imp	$⊢ ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s)) \to s ≃_{𝑟} r$
15	6 14	sylbi	$⊢ r ≃_{𝑟} s \to s ≃_{𝑟} r$
16		vex	$⊢ t \in V$
17	5 16	isrisc	$⊢ s ≃_{𝑟} t \leftrightarrow ((s \in RingOps \land t \in RingOps) \land \exists g g \in (s RngIso t))$
18		exdistrv	$⊢ \exists f \exists g (f \in (r RngIso s) \land g \in (s RngIso t)) \leftrightarrow (\exists f f \in (r RngIso s) \land \exists g g \in (s RngIso t))$
19		rngoisoco	$⊢ ((r \in RingOps \land s \in RingOps \land t \in RingOps) \land (f \in (r RngIso s) \land g \in (s RngIso t))) \to g \circ f \in (r RngIso t)$
20	19	ex	$⊢ (r \in RingOps \land s \in RingOps \land t \in RingOps) \to ((f \in (r RngIso s) \land g \in (s RngIso t)) \to g \circ f \in (r RngIso t))$
21		risci	$⊢ (r \in RingOps \land t \in RingOps \land g \circ f \in (r RngIso t)) \to r ≃_{𝑟} t$
22	21	3expia	$⊢ (r \in RingOps \land t \in RingOps) \to (g \circ f \in (r RngIso t) \to r ≃_{𝑟} t)$
23	22	3adant2	$⊢ (r \in RingOps \land s \in RingOps \land t \in RingOps) \to (g \circ f \in (r RngIso t) \to r ≃_{𝑟} t)$
24	20 23	syld	$⊢ (r \in RingOps \land s \in RingOps \land t \in RingOps) \to ((f \in (r RngIso s) \land g \in (s RngIso t)) \to r ≃_{𝑟} t)$
25	24	exlimdvv	$⊢ (r \in RingOps \land s \in RingOps \land t \in RingOps) \to (\exists f \exists g (f \in (r RngIso s) \land g \in (s RngIso t)) \to r ≃_{𝑟} t)$
26	18 25	syl5bir	$⊢ (r \in RingOps \land s \in RingOps \land t \in RingOps) \to ((\exists f f \in (r RngIso s) \land \exists g g \in (s RngIso t)) \to r ≃_{𝑟} t)$
27	26	3expb	$⊢ (r \in RingOps \land (s \in RingOps \land t \in RingOps)) \to ((\exists f f \in (r RngIso s) \land \exists g g \in (s RngIso t)) \to r ≃_{𝑟} t)$
28	27	adantlr	$⊢ ((r \in RingOps \land s \in RingOps) \land (s \in RingOps \land t \in RingOps)) \to ((\exists f f \in (r RngIso s) \land \exists g g \in (s RngIso t)) \to r ≃_{𝑟} t)$
29	28	imp	$⊢ (((r \in RingOps \land s \in RingOps) \land (s \in RingOps \land t \in RingOps)) \land (\exists f f \in (r RngIso s) \land \exists g g \in (s RngIso t))) \to r ≃_{𝑟} t$
30	29	an4s	$⊢ (((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s)) \land ((s \in RingOps \land t \in RingOps) \land \exists g g \in (s RngIso t))) \to r ≃_{𝑟} t$
31	6 17 30	syl2anb	$⊢ (r ≃_{𝑟} s \land s ≃_{𝑟} t) \to r ≃_{𝑟} t$
32	15 31	pm3.2i	$⊢ ((r ≃_{𝑟} s \to s ≃_{𝑟} r) \land ((r ≃_{𝑟} s \land s ≃_{𝑟} t) \to r ≃_{𝑟} t))$
33	32	ax-gen	$⊢ \forall t ((r ≃_{𝑟} s \to s ≃_{𝑟} r) \land ((r ≃_{𝑟} s \land s ≃_{𝑟} t) \to r ≃_{𝑟} t))$
34	33	gen2	$⊢ \forall r \forall s \forall t ((r ≃_{𝑟} s \to s ≃_{𝑟} r) \land ((r ≃_{𝑟} s \land s ≃_{𝑟} t) \to r ≃_{𝑟} t))$
35		dfer2	$⊢ ≃_{𝑟} Er dom ≃_{𝑟} \leftrightarrow (Rel ≃_{𝑟} \land dom ≃_{𝑟} = dom ≃_{𝑟} \land \forall r \forall s \forall t ((r ≃_{𝑟} s \to s ≃_{𝑟} r) \land ((r ≃_{𝑟} s \land s ≃_{𝑟} t) \to r ≃_{𝑟} t)))$
36	2 3 34 35	mpbir3an	$⊢ ≃_{𝑟} Er dom ≃_{𝑟}$

Metamath Proof Explorer

Theorem riscer

Proof