Proof of Theorem iscrngo2
Step | Hyp | Ref
| Expression |
1 | | iscrngo 35891 |
. 2
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2)) |
2 | | relrngo 35791 |
. . . . 5
⊢ Rel
RingOps |
3 | | 1st2nd 7810 |
. . . . 5
⊢ ((Rel
RingOps ∧ 𝑅 ∈
RingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
4 | 2, 3 | mpan 690 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) |
5 | | eleq1 2825 |
. . . . 5
⊢ (𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 →
(𝑅 ∈ Com2 ↔
〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ Com2)) |
6 | | iscring2.3 |
. . . . . . . 8
⊢ 𝑋 = ran 𝐺 |
7 | | iscring2.1 |
. . . . . . . . 9
⊢ 𝐺 = (1st ‘𝑅) |
8 | 7 | rneqi 5806 |
. . . . . . . 8
⊢ ran 𝐺 = ran (1st
‘𝑅) |
9 | 6, 8 | eqtri 2765 |
. . . . . . 7
⊢ 𝑋 = ran (1st
‘𝑅) |
10 | 9 | raleqi 3323 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥) ↔ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
11 | | iscring2.2 |
. . . . . . . . . 10
⊢ 𝐻 = (2nd ‘𝑅) |
12 | 11 | oveqi 7226 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝑥(2nd ‘𝑅)𝑦) |
13 | 11 | oveqi 7226 |
. . . . . . . . 9
⊢ (𝑦𝐻𝑥) = (𝑦(2nd ‘𝑅)𝑥) |
14 | 12, 13 | eqeq12i 2755 |
. . . . . . . 8
⊢ ((𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ (𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
15 | 9, 14 | raleqbii 3156 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
16 | 15 | ralbii 3088 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
17 | | fvex 6730 |
. . . . . . 7
⊢
(1st ‘𝑅) ∈ V |
18 | | fvex 6730 |
. . . . . . 7
⊢
(2nd ‘𝑅) ∈ V |
19 | | iscom2 35890 |
. . . . . . 7
⊢
(((1st ‘𝑅) ∈ V ∧ (2nd
‘𝑅) ∈ V) →
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ Com2 ↔ ∀𝑥 ∈ ran (1st
‘𝑅)∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥))) |
20 | 17, 18, 19 | mp2an 692 |
. . . . . 6
⊢
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ Com2 ↔ ∀𝑥 ∈ ran (1st
‘𝑅)∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
21 | 10, 16, 20 | 3bitr4ri 307 |
. . . . 5
⊢
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ Com2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)) |
22 | 5, 21 | bitrdi 290 |
. . . 4
⊢ (𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 →
(𝑅 ∈ Com2 ↔
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
23 | 4, 22 | syl 17 |
. . 3
⊢ (𝑅 ∈ RingOps → (𝑅 ∈ Com2 ↔
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
24 | 23 | pm5.32i 578 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2) ↔ (𝑅 ∈ RingOps ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
25 | 1, 24 | bitri 278 |
1
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |