Step | Hyp | Ref
| Expression |
1 | | rrgval.e |
. 2
⊢ 𝐸 = (RLReg‘𝑅) |
2 | | fveq2 6735 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | rrgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | eqtr4di 2797 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | | fveq2 6735 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
6 | | rrgval.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
7 | 5, 6 | eqtr4di 2797 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
8 | 7 | oveqd 7248 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
9 | | fveq2 6735 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
10 | | rrgval.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
11 | 9, 10 | eqtr4di 2797 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
12 | 8, 11 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) ↔ (𝑥 · 𝑦) = 0 )) |
13 | 11 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑦 = (0g‘𝑟) ↔ 𝑦 = 0 )) |
14 | 12, 13 | imbi12d 348 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
15 | 4, 14 | raleqbidv 3325 |
. . . . 5
⊢ (𝑟 = 𝑅 → (∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
16 | 4, 15 | rabeqbidv 3408 |
. . . 4
⊢ (𝑟 = 𝑅 → {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
17 | | df-rlreg 20345 |
. . . 4
⊢ RLReg =
(𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) |
18 | 3 | fvexi 6749 |
. . . . 5
⊢ 𝐵 ∈ V |
19 | 18 | rabex 5239 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} ∈
V |
20 | 16, 17, 19 | fvmpt 6836 |
. . 3
⊢ (𝑅 ∈ V →
(RLReg‘𝑅) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
21 | | fvprc 6727 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(RLReg‘𝑅) =
∅) |
22 | | fvprc 6727 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
23 | 3, 22 | syl5eq 2791 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
24 | 23 | rabeqdv 3407 |
. . . . 5
⊢ (¬
𝑅 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
25 | | rab0 4311 |
. . . . 5
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} =
∅ |
26 | 24, 25 | eqtrdi 2795 |
. . . 4
⊢ (¬
𝑅 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} =
∅) |
27 | 21, 26 | eqtr4d 2781 |
. . 3
⊢ (¬
𝑅 ∈ V →
(RLReg‘𝑅) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
28 | 20, 27 | pm2.61i 185 |
. 2
⊢
(RLReg‘𝑅) =
{𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} |
29 | 1, 28 | eqtri 2766 |
1
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} |