Step | Hyp | Ref
| Expression |
1 | | rrgval.e |
. . . 4
⊢ 𝐸 = (RLReg‘𝑅) |
2 | 1 | rrgmex 13741 |
. . 3
⊢ (𝑧 ∈ 𝐸 → 𝑅 ∈ V) |
3 | | elrabi 2913 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} → 𝑧 ∈ 𝐵) |
4 | | rrgval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
5 | 4 | basmex 12667 |
. . . 4
⊢ (𝑧 ∈ 𝐵 → 𝑅 ∈ V) |
6 | 3, 5 | syl 14 |
. . 3
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} → 𝑅 ∈ V) |
7 | | df-rlreg 13738 |
. . . . . 6
⊢ RLReg =
(𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) |
8 | | fveq2 5546 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
9 | 8, 4 | eqtr4di 2244 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
10 | | fveq2 5546 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
11 | | rrgval.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
12 | 10, 11 | eqtr4di 2244 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
13 | 12 | oveqd 5927 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
14 | | fveq2 5546 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
15 | | rrgval.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
16 | 14, 15 | eqtr4di 2244 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
17 | 13, 16 | eqeq12d 2208 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) ↔ (𝑥 · 𝑦) = 0 )) |
18 | 16 | eqeq2d 2205 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑦 = (0g‘𝑟) ↔ 𝑦 = 0 )) |
19 | 17, 18 | imbi12d 234 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
20 | 9, 19 | raleqbidv 2706 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
21 | 9, 20 | rabeqbidv 2755 |
. . . . . 6
⊢ (𝑟 = 𝑅 → {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
22 | | id 19 |
. . . . . 6
⊢ (𝑅 ∈ V → 𝑅 ∈ V) |
23 | | basfn 12666 |
. . . . . . . . 9
⊢ Base Fn
V |
24 | | funfvex 5563 |
. . . . . . . . . 10
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
25 | 24 | funfni 5346 |
. . . . . . . . 9
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
26 | 23, 25 | mpan 424 |
. . . . . . . 8
⊢ (𝑅 ∈ V →
(Base‘𝑅) ∈
V) |
27 | 4, 26 | eqeltrid 2280 |
. . . . . . 7
⊢ (𝑅 ∈ V → 𝐵 ∈ V) |
28 | | rabexg 4172 |
. . . . . . 7
⊢ (𝐵 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} ∈
V) |
29 | 27, 28 | syl 14 |
. . . . . 6
⊢ (𝑅 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} ∈
V) |
30 | 7, 21, 22, 29 | fvmptd3 5643 |
. . . . 5
⊢ (𝑅 ∈ V →
(RLReg‘𝑅) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
31 | 1, 30 | eqtrid 2238 |
. . . 4
⊢ (𝑅 ∈ V → 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
32 | 31 | eleq2d 2263 |
. . 3
⊢ (𝑅 ∈ V → (𝑧 ∈ 𝐸 ↔ 𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )})) |
33 | 2, 6, 32 | pm5.21nii 705 |
. 2
⊢ (𝑧 ∈ 𝐸 ↔ 𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
34 | 33 | eqriv 2190 |
1
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} |