Step | Hyp | Ref
| Expression |
1 | | opprdomn.1 |
. . . 4
⊢ 𝑂 =
(oppr‘𝑅) |
2 | 1 | opprnzrbg 13665 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing)) |
3 | | eqid 2193 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | 1, 3 | opprbasg 13555 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘𝑂)) |
5 | | vex 2763 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
6 | | vex 2763 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
7 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
8 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(.r‘𝑂) = (.r‘𝑂) |
9 | 3, 7, 1, 8 | opprmulg 13551 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑦 ∈ V ∧ 𝑥 ∈ V) → (𝑦(.r‘𝑂)𝑥) = (𝑥(.r‘𝑅)𝑦)) |
10 | 5, 6, 9 | mp3an23 1340 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑦(.r‘𝑂)𝑥) = (𝑥(.r‘𝑅)𝑦)) |
11 | 10 | eqcomd 2199 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑥(.r‘𝑅)𝑦) = (𝑦(.r‘𝑂)𝑥)) |
12 | | eqid 2193 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
13 | 1, 12 | oppr0g 13561 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (0g‘𝑅) = (0g‘𝑂)) |
14 | 11, 13 | eqeq12d 2208 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) ↔ (𝑦(.r‘𝑂)𝑥) = (0g‘𝑂))) |
15 | 13 | eqeq2d 2205 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑥 = (0g‘𝑅) ↔ 𝑥 = (0g‘𝑂))) |
16 | 13 | eqeq2d 2205 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑦 = (0g‘𝑅) ↔ 𝑦 = (0g‘𝑂))) |
17 | 15, 16 | orbi12d 794 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ((𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)) ↔ (𝑥 = (0g‘𝑂) ∨ 𝑦 = (0g‘𝑂)))) |
18 | | orcom 729 |
. . . . . . . 8
⊢ ((𝑥 = (0g‘𝑂) ∨ 𝑦 = (0g‘𝑂)) ↔ (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))) |
19 | 17, 18 | bitrdi 196 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ((𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)) ↔ (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂)))) |
20 | 14, 19 | imbi12d 234 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) ↔ ((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))))) |
21 | 4, 20 | raleqbidv 2706 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) ↔ ∀𝑦 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))))) |
22 | 4, 21 | raleqbidv 2706 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) ↔ ∀𝑥 ∈ (Base‘𝑂)∀𝑦 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))))) |
23 | | ralcom 2657 |
. . . 4
⊢
(∀𝑥 ∈
(Base‘𝑂)∀𝑦 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))) ↔ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂)))) |
24 | 22, 23 | bitrdi 196 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) ↔ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))))) |
25 | 2, 24 | anbi12d 473 |
. 2
⊢ (𝑅 ∈ 𝑉 → ((𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)))) ↔ (𝑂 ∈ NzRing ∧ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂)))))) |
26 | 3, 7, 12 | isdomn 13749 |
. 2
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))))) |
27 | | eqid 2193 |
. . 3
⊢
(Base‘𝑂) =
(Base‘𝑂) |
28 | | eqid 2193 |
. . 3
⊢
(0g‘𝑂) = (0g‘𝑂) |
29 | 27, 8, 28 | isdomn 13749 |
. 2
⊢ (𝑂 ∈ Domn ↔ (𝑂 ∈ NzRing ∧
∀𝑦 ∈
(Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r‘𝑂)𝑥) = (0g‘𝑂) → (𝑦 = (0g‘𝑂) ∨ 𝑥 = (0g‘𝑂))))) |
30 | 25, 26, 29 | 3bitr4g 223 |
1
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn)) |