Theorem 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	$$⊢{\simeq }_{𝑟}\mathrm{Er}\mathrm{dom}{\simeq }_{𝑟}$$

Proof

Step	Hyp	Ref	Expression
1		df-risc	Could not format ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } : No typesetting found for |- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } with typecode |-
2	1	relopabiv	$$⊢\mathrm{Rel}{\simeq }_{𝑟}$$
3		eqid	$$⊢\mathrm{dom}{\simeq }_{𝑟}=\mathrm{dom}{\simeq }_{𝑟}$$
4		vex	$$⊢r\in \mathrm{V}$$
5		vex	$$⊢s\in \mathrm{V}$$
6	4 5	isrisc	Could not format ( r ~=R s <-> ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) ) : No typesetting found for |- ( r ~=R s <-> ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) ) with typecode |-
7		rngoisocnv	Could not format ( ( r e. RingOps /\ s e. RingOps /\ f e. ( r RingOpsIso s ) ) -> `' f e. ( s RingOpsIso r ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ f e. ( r RingOpsIso s ) ) -> `' f e. ( s RingOpsIso r ) ) with typecode |-
8	7	3expia	Could not format ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RingOpsIso s ) -> `' f e. ( s RingOpsIso r ) ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RingOpsIso s ) -> `' f e. ( s RingOpsIso r ) ) ) with typecode |-
9		risci	Could not format ( ( s e. RingOps /\ r e. RingOps /\ `' f e. ( s RingOpsIso r ) ) -> s ~=R r ) : No typesetting found for |- ( ( s e. RingOps /\ r e. RingOps /\ `' f e. ( s RingOpsIso r ) ) -> s ~=R r ) with typecode |-
10	9	3expia	Could not format ( ( s e. RingOps /\ r e. RingOps ) -> ( `' f e. ( s RingOpsIso r ) -> s ~=R r ) ) : No typesetting found for |- ( ( s e. RingOps /\ r e. RingOps ) -> ( `' f e. ( s RingOpsIso r ) -> s ~=R r ) ) with typecode |-
11	10	ancoms	Could not format ( ( r e. RingOps /\ s e. RingOps ) -> ( `' f e. ( s RingOpsIso r ) -> s ~=R r ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps ) -> ( `' f e. ( s RingOpsIso r ) -> s ~=R r ) ) with typecode |-
12	8 11	syld	Could not format ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RingOpsIso s ) -> s ~=R r ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RingOpsIso s ) -> s ~=R r ) ) with typecode |-
13	12	exlimdv	Could not format ( ( r e. RingOps /\ s e. RingOps ) -> ( E. f f e. ( r RingOpsIso s ) -> s ~=R r ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps ) -> ( E. f f e. ( r RingOpsIso s ) -> s ~=R r ) ) with typecode |-
14	13	imp	Could not format ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) -> s ~=R r ) : No typesetting found for |- ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) -> s ~=R r ) with typecode |-
15	6 14	sylbi	$$⊢r{\simeq }_{𝑟}s\to s{\simeq }_{𝑟}r$$
16		vex	$$⊢t\in \mathrm{V}$$
17	5 16	isrisc	Could not format ( s ~=R t <-> ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RingOpsIso t ) ) ) : No typesetting found for |- ( s ~=R t <-> ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RingOpsIso t ) ) ) with typecode |-
18		exdistrv	Could not format ( E. f E. g ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) <-> ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) ) : No typesetting found for |- ( E. f E. g ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) <-> ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) ) with typecode |-
19		rngoisoco	Could not format ( ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) /\ ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) ) -> ( g o. f ) e. ( r RingOpsIso t ) ) : No typesetting found for |- ( ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) /\ ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) ) -> ( g o. f ) e. ( r RingOpsIso t ) ) with typecode |-
20	19	ex	Could not format ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> ( g o. f ) e. ( r RingOpsIso t ) ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> ( g o. f ) e. ( r RingOpsIso t ) ) ) with typecode |-
21		risci	Could not format ( ( r e. RingOps /\ t e. RingOps /\ ( g o. f ) e. ( r RingOpsIso t ) ) -> r ~=R t ) : No typesetting found for |- ( ( r e. RingOps /\ t e. RingOps /\ ( g o. f ) e. ( r RingOpsIso t ) ) -> r ~=R t ) with typecode |-
22	21	3expia	Could not format ( ( r e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RingOpsIso t ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RingOpsIso t ) -> r ~=R t ) ) with typecode |-
23	22	3adant2	Could not format ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RingOpsIso t ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RingOpsIso t ) -> r ~=R t ) ) with typecode |-
24	20 23	syld	Could not format ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) with typecode |-
25	24	exlimdvv	Could not format ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( E. f E. g ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( E. f E. g ( f e. ( r RingOpsIso s ) /\ g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) with typecode |-
26	18 25	biimtrrid	Could not format ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) with typecode |-
27	26	3expb	Could not format ( ( r e. RingOps /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) : No typesetting found for |- ( ( r e. RingOps /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) with typecode |-
28	27	adantlr	Could not format ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) : No typesetting found for |- ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) -> r ~=R t ) ) with typecode |-
29	28	imp	Could not format ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) /\ ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) ) -> r ~=R t ) : No typesetting found for |- ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) /\ ( E. f f e. ( r RingOpsIso s ) /\ E. g g e. ( s RingOpsIso t ) ) ) -> r ~=R t ) with typecode |-
30	29	an4s	Could not format ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) /\ ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RingOpsIso t ) ) ) -> r ~=R t ) : No typesetting found for |- ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) /\ ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RingOpsIso t ) ) ) -> r ~=R t ) with typecode |-
31	6 17 30	syl2anb	$$⊢\left(r{\simeq }_{𝑟}s\wedge s{\simeq }_{𝑟}t\right)\to r{\simeq }_{𝑟}t$$
32	15 31	pm3.2i	$$⊢\left(\left(r{\simeq }_{𝑟}s\to s{\simeq }_{𝑟}r\right)\wedge \left(\left(r{\simeq }_{𝑟}s\wedge s{\simeq }_{𝑟}t\right)\to r{\simeq }_{𝑟}t\right)\right)$$
33	32	ax-gen	$$⊢\forall t\left(\left(r{\simeq }_{𝑟}s\to s{\simeq }_{𝑟}r\right)\wedge \left(\left(r{\simeq }_{𝑟}s\wedge s{\simeq }_{𝑟}t\right)\to r{\simeq }_{𝑟}t\right)\right)$$
34	33	gen2	$$⊢\forall r\forall s\forall t\left(\left(r{\simeq }_{𝑟}s\to s{\simeq }_{𝑟}r\right)\wedge \left(\left(r{\simeq }_{𝑟}s\wedge s{\simeq }_{𝑟}t\right)\to r{\simeq }_{𝑟}t\right)\right)$$
35		dfer2	$$⊢{\simeq }_{𝑟}\mathrm{Er}\mathrm{dom}{\simeq }_{𝑟}\leftrightarrow \left(\mathrm{Rel}{\simeq }_{𝑟}\wedge \mathrm{dom}{\simeq }_{𝑟}=\mathrm{dom}{\simeq }_{𝑟}\wedge \forall r\forall s\forall t\left(\left(r{\simeq }_{𝑟}s\to s{\simeq }_{𝑟}r\right)\wedge \left(\left(r{\simeq }_{𝑟}s\wedge s{\simeq }_{𝑟}t\right)\to r{\simeq }_{𝑟}t\right)\right)\right)$$
36	2 3 34 35	mpbir3an	$$⊢{\simeq }_{𝑟}\mathrm{Er}\mathrm{dom}{\simeq }_{𝑟}$$