Step | Hyp | Ref
| Expression |
1 | | dvrval.d |
. 2
⊢ / =
(/r‘𝑅) |
2 | | fveq2 6538 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | dvrval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2849 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | | fveq2 6538 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅)) |
6 | | dvrval.u |
. . . . . 6
⊢ 𝑈 = (Unit‘𝑅) |
7 | 5, 6 | syl6eqr 2849 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈) |
8 | | fveq2 6538 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
9 | | dvrval.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
10 | 8, 9 | syl6eqr 2849 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
11 | | eqidd 2796 |
. . . . . 6
⊢ (𝑟 = 𝑅 → 𝑥 = 𝑥) |
12 | | fveq2 6538 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (invr‘𝑟) = (invr‘𝑅)) |
13 | | dvrval.i |
. . . . . . . 8
⊢ 𝐼 = (invr‘𝑅) |
14 | 12, 13 | syl6eqr 2849 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (invr‘𝑟) = 𝐼) |
15 | 14 | fveq1d 6540 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((invr‘𝑟)‘𝑦) = (𝐼‘𝑦)) |
16 | 10, 11, 15 | oveq123d 7037 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)) = (𝑥 · (𝐼‘𝑦))) |
17 | 4, 7, 16 | mpoeq123dv 7087 |
. . . 4
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
18 | | df-dvr 19123 |
. . . 4
⊢
/r = (𝑟
∈ V ↦ (𝑥 ∈
(Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)))) |
19 | 3 | fvexi 6552 |
. . . . 5
⊢ 𝐵 ∈ V |
20 | 6 | fvexi 6552 |
. . . . 5
⊢ 𝑈 ∈ V |
21 | 19, 20 | mpoex 7633 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) ∈ V |
22 | 17, 18, 21 | fvmpt 6635 |
. . 3
⊢ (𝑅 ∈ V →
(/r‘𝑅) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
23 | | fvprc 6531 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(/r‘𝑅) =
∅) |
24 | | fvprc 6531 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
25 | 3, 24 | syl5eq 2843 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
26 | | eqid 2795 |
. . . . . 6
⊢ 𝑈 = 𝑈 |
27 | | mpoeq12 7085 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑈 = 𝑈) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
28 | 25, 26, 27 | sylancl 586 |
. . . . 5
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
29 | | mpo0 7095 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = ∅ |
30 | 28, 29 | syl6eq 2847 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = ∅) |
31 | 23, 30 | eqtr4d 2834 |
. . 3
⊢ (¬
𝑅 ∈ V →
(/r‘𝑅) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
32 | 22, 31 | pm2.61i 183 |
. 2
⊢
(/r‘𝑅) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) |
33 | 1, 32 | eqtri 2819 |
1
⊢ / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) |