Step | Hyp | Ref
| Expression |
1 | | basfn 12663 |
. . . . 5
⊢ Base Fn
V |
2 | | vex 2763 |
. . . . 5
⊢ 𝑟 ∈ V |
3 | | funfvex 5563 |
. . . . . 6
⊢ ((Fun
Base ∧ 𝑟 ∈ dom
Base) → (Base‘𝑟)
∈ V) |
4 | 3 | funfni 5346 |
. . . . 5
⊢ ((Base Fn
V ∧ 𝑟 ∈ V) →
(Base‘𝑟) ∈
V) |
5 | 1, 2, 4 | mp2an 426 |
. . . 4
⊢
(Base‘𝑟)
∈ V |
6 | 5 | a1i 9 |
. . 3
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
7 | | fveq2 5546 |
. . . 4
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
8 | | isdomn.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
9 | 7, 8 | eqtr4di 2244 |
. . 3
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
10 | | fn0g 12945 |
. . . . . 6
⊢
0g Fn V |
11 | | funfvex 5563 |
. . . . . . 7
⊢ ((Fun
0g ∧ 𝑟
∈ dom 0g) → (0g‘𝑟) ∈ V) |
12 | 11 | funfni 5346 |
. . . . . 6
⊢
((0g Fn V ∧ 𝑟 ∈ V) → (0g‘𝑟) ∈ V) |
13 | 10, 2, 12 | mp2an 426 |
. . . . 5
⊢
(0g‘𝑟) ∈ V |
14 | 13 | a1i 9 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) ∈ V) |
15 | | fveq2 5546 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
16 | 15 | adantr 276 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = (0g‘𝑅)) |
17 | | isdomn.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
18 | 16, 17 | eqtr4di 2244 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = 0 ) |
19 | | simplr 528 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → 𝑏 = 𝐵) |
20 | | fveq2 5546 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
21 | | isdomn.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
22 | 20, 21 | eqtr4di 2244 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
23 | 22 | oveqdr 5938 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
24 | | id 19 |
. . . . . . . 8
⊢ (𝑧 = 0 → 𝑧 = 0 ) |
25 | 23, 24 | eqeqan12d 2209 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥(.r‘𝑟)𝑦) = 𝑧 ↔ (𝑥 · 𝑦) = 0 )) |
26 | | eqeq2 2203 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑥 = 𝑧 ↔ 𝑥 = 0 )) |
27 | | eqeq2 2203 |
. . . . . . . . 9
⊢ (𝑧 = 0 → (𝑦 = 𝑧 ↔ 𝑦 = 0 )) |
28 | 26, 27 | orbi12d 794 |
. . . . . . . 8
⊢ (𝑧 = 0 → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 ))) |
29 | 28 | adantl 277 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 ))) |
30 | 25, 29 | imbi12d 234 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
31 | 19, 30 | raleqbidv 2706 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
32 | 19, 31 | raleqbidv 2706 |
. . . 4
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
33 | 14, 18, 32 | sbcied2 3023 |
. . 3
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
34 | 6, 9, 33 | sbcied2 3023 |
. 2
⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
35 | | df-domn 13733 |
. 2
⊢ Domn =
{𝑟 ∈ NzRing ∣
[(Base‘𝑟) /
𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))} |
36 | 34, 35 | elrab2 2919 |
1
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |