Step | Hyp | Ref
| Expression |
1 | | rrgval.e |
. 2
⊢ 𝐸 = (RLReg‘𝑅) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | rrgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2674 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
6 | | rrgval.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
7 | 5, 6 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
8 | 7 | oveqd 6667 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
9 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
10 | | rrgval.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
11 | 9, 10 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
12 | 8, 11 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) ↔ (𝑥 · 𝑦) = 0 )) |
13 | 11 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑦 = (0g‘𝑟) ↔ 𝑦 = 0 )) |
14 | 12, 13 | imbi12d 334 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
15 | 4, 14 | raleqbidv 3152 |
. . . . 5
⊢ (𝑟 = 𝑅 → (∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 ))) |
16 | 4, 15 | rabeqbidv 3195 |
. . . 4
⊢ (𝑟 = 𝑅 → {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
17 | | df-rlreg 19283 |
. . . 4
⊢ RLReg =
(𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}) |
18 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
19 | 3, 18 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
20 | 19 | rabex 4813 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} ∈
V |
21 | 16, 17, 20 | fvmpt 6282 |
. . 3
⊢ (𝑅 ∈ V →
(RLReg‘𝑅) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
22 | | fvprc 6185 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(RLReg‘𝑅) =
∅) |
23 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
24 | 3, 23 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
25 | | rabeq 3192 |
. . . . . 6
⊢ (𝐵 = ∅ → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (¬
𝑅 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
27 | | rab0 3955 |
. . . . 5
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} =
∅ |
28 | 26, 27 | syl6eq 2672 |
. . . 4
⊢ (¬
𝑅 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} =
∅) |
29 | 22, 28 | eqtr4d 2659 |
. . 3
⊢ (¬
𝑅 ∈ V →
(RLReg‘𝑅) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}) |
30 | 21, 29 | pm2.61i 176 |
. 2
⊢
(RLReg‘𝑅) =
{𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} |
31 | 1, 30 | eqtri 2644 |
1
⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )} |