Step | Hyp | Ref
| Expression |
1 | | iscrngo 36458 |
. 2
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2)) |
2 | | relrngo 36358 |
. . . . 5
⊢ Rel
RingOps |
3 | | 1st2nd 7972 |
. . . . 5
⊢ ((Rel
RingOps ∧ 𝑅 ∈
RingOps) → 𝑅 =
⟨(1st ‘𝑅), (2nd ‘𝑅)⟩) |
4 | 2, 3 | mpan 689 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝑅 = ⟨(1st
‘𝑅), (2nd
‘𝑅)⟩) |
5 | | eleq1 2826 |
. . . . 5
⊢ (𝑅 = ⟨(1st
‘𝑅), (2nd
‘𝑅)⟩ →
(𝑅 ∈ Com2 ↔
⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ Com2)) |
6 | | iscring2.3 |
. . . . . . . 8
⊢ 𝑋 = ran 𝐺 |
7 | | iscring2.1 |
. . . . . . . . 9
⊢ 𝐺 = (1st ‘𝑅) |
8 | 7 | rneqi 5893 |
. . . . . . . 8
⊢ ran 𝐺 = ran (1st
‘𝑅) |
9 | 6, 8 | eqtri 2765 |
. . . . . . 7
⊢ 𝑋 = ran (1st
‘𝑅) |
10 | 9 | raleqi 3312 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥) ↔ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
11 | | iscring2.2 |
. . . . . . . . . 10
⊢ 𝐻 = (2nd ‘𝑅) |
12 | 11 | oveqi 7371 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝑥(2nd ‘𝑅)𝑦) |
13 | 11 | oveqi 7371 |
. . . . . . . . 9
⊢ (𝑦𝐻𝑥) = (𝑦(2nd ‘𝑅)𝑥) |
14 | 12, 13 | eqeq12i 2755 |
. . . . . . . 8
⊢ ((𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ (𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
15 | 9, 14 | raleqbii 3316 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
16 | 15 | ralbii 3097 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ran (1st ‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
17 | | fvex 6856 |
. . . . . . 7
⊢
(1st ‘𝑅) ∈ V |
18 | | fvex 6856 |
. . . . . . 7
⊢
(2nd ‘𝑅) ∈ V |
19 | | iscom2 36457 |
. . . . . . 7
⊢
(((1st ‘𝑅) ∈ V ∧ (2nd
‘𝑅) ∈ V) →
(⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ Com2 ↔ ∀𝑥 ∈ ran (1st
‘𝑅)∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥))) |
20 | 17, 18, 19 | mp2an 691 |
. . . . . 6
⊢
(⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ Com2 ↔ ∀𝑥 ∈ ran (1st
‘𝑅)∀𝑦 ∈ ran (1st
‘𝑅)(𝑥(2nd ‘𝑅)𝑦) = (𝑦(2nd ‘𝑅)𝑥)) |
21 | 10, 16, 20 | 3bitr4ri 304 |
. . . . 5
⊢
(⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ Com2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥)) |
22 | 5, 21 | bitrdi 287 |
. . . 4
⊢ (𝑅 = ⟨(1st
‘𝑅), (2nd
‘𝑅)⟩ →
(𝑅 ∈ Com2 ↔
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
23 | 4, 22 | syl 17 |
. . 3
⊢ (𝑅 ∈ RingOps → (𝑅 ∈ Com2 ↔
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
24 | 23 | pm5.32i 576 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2) ↔ (𝑅 ∈ RingOps ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |
25 | 1, 24 | bitri 275 |
1
⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) |