Metamath Proof Explorer

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 ≃𝑟 Er dom ≃𝑟

Proof

Step Hyp Ref Expression
1 df-risc ⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) }
2 1 relopabiv ⊢ Rel ≃𝑟
3 eqid ⊢ dom ≃𝑟 = dom ≃𝑟
4 vex ⊢ 𝑟 ∈ V
5 vex ⊢ 𝑠 ∈ V
6 4 5 isrisc ⊢ ( 𝑟 ≃𝑟 𝑠 ↔ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) )
7 rngoisocnv ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) → ◡ 𝑓 ∈ ( 𝑠 RngIso 𝑟 ) )
8 7 3expia ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) → ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) → ◡ 𝑓 ∈ ( 𝑠 RngIso 𝑟 ) ) )
9 risci ⊢ ( ( 𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps ∧ ◡ 𝑓 ∈ ( 𝑠 RngIso 𝑟 ) ) → 𝑠 ≃𝑟 𝑟 )
10 9 3expia ⊢ ( ( 𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps ) → ( ◡ 𝑓 ∈ ( 𝑠 RngIso 𝑟 ) → 𝑠 ≃𝑟 𝑟 ) )
11 10 ancoms ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) → ( ◡ 𝑓 ∈ ( 𝑠 RngIso 𝑟 ) → 𝑠 ≃𝑟 𝑟 ) )
12 8 11 syld ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) → ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) → 𝑠 ≃𝑟 𝑟 ) )
13 12 exlimdv ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) → ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) → 𝑠 ≃𝑟 𝑟 ) )
14 13 imp ⊢ ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) → 𝑠 ≃𝑟 𝑟 )
15 6 14 sylbi ⊢ ( 𝑟 ≃𝑟 𝑠 → 𝑠 ≃𝑟 𝑟 )
16 vex ⊢ 𝑡 ∈ V
17 5 16 isrisc ⊢ ( 𝑠 ≃𝑟 𝑡 ↔ ( ( 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) )
18 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) )
19 rngoisoco ⊢ ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ∧ ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑟 RngIso 𝑡 ) )
20 19 ex ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑟 RngIso 𝑡 ) ) )
21 risci ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps ∧ ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑟 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 )
22 21 3expia ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑟 RngIso 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) )
23 22 3adant2 ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑟 RngIso 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) )
24 20 23 syld ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 ) )
25 24 exlimdvv ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 ) )
26 18 25 syl5bir ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 ) )
27 26 3expb ⊢ ( ( 𝑟 ∈ RingOps ∧ ( 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 ) )
28 27 adantlr ⊢ ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ( 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) → 𝑟 ≃𝑟 𝑡 ) )
29 28 imp ⊢ ( ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ( 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ) ∧ ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) ) → 𝑟 ≃𝑟 𝑡 )
30 29 an4s ⊢ ( ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) ∧ ( ( 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑠 RngIso 𝑡 ) ) ) → 𝑟 ≃𝑟 𝑡 )
31 6 17 30 syl2anb ⊢ ( ( 𝑟 ≃𝑟 𝑠 ∧ 𝑠 ≃𝑟 𝑡 ) → 𝑟 ≃𝑟 𝑡 )
32 15 31 pm3.2i ⊢ ( ( 𝑟 ≃𝑟 𝑠 → 𝑠 ≃𝑟 𝑟 ) ∧ ( ( 𝑟 ≃𝑟 𝑠 ∧ 𝑠 ≃𝑟 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) )
33 32 ax-gen ⊢ ∀ 𝑡 ( ( 𝑟 ≃𝑟 𝑠 → 𝑠 ≃𝑟 𝑟 ) ∧ ( ( 𝑟 ≃𝑟 𝑠 ∧ 𝑠 ≃𝑟 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) )
34 33 gen2 ⊢ ∀ 𝑟 ∀ 𝑠 ∀ 𝑡 ( ( 𝑟 ≃𝑟 𝑠 → 𝑠 ≃𝑟 𝑟 ) ∧ ( ( 𝑟 ≃𝑟 𝑠 ∧ 𝑠 ≃𝑟 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) )
35 dfer2 ⊢ ( ≃𝑟 Er dom ≃𝑟 ↔ ( Rel ≃𝑟 ∧ dom ≃𝑟 = dom ≃𝑟 ∧ ∀ 𝑟 ∀ 𝑠 ∀ 𝑡 ( ( 𝑟 ≃𝑟 𝑠 → 𝑠 ≃𝑟 𝑟 ) ∧ ( ( 𝑟 ≃𝑟 𝑠 ∧ 𝑠 ≃𝑟 𝑡 ) → 𝑟 ≃𝑟 𝑡 ) ) ) )
36 2 3 34 35 mpbir3an ⊢ ≃𝑟 Er dom ≃𝑟