Step | Hyp | Ref
| Expression |
1 | | dvrval.d |
. 2
⊢ / =
(/r‘𝑅) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | dvrval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2662 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅)) |
6 | | dvrval.u |
. . . . . 6
⊢ 𝑈 = (Unit‘𝑅) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈) |
8 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
9 | | dvrval.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
11 | | eqidd 2611 |
. . . . . 6
⊢ (𝑟 = 𝑅 → 𝑥 = 𝑥) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (invr‘𝑟) = (invr‘𝑅)) |
13 | | dvrval.i |
. . . . . . . 8
⊢ 𝐼 = (invr‘𝑅) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (invr‘𝑟) = 𝐼) |
15 | 14 | fveq1d 6105 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((invr‘𝑟)‘𝑦) = (𝐼‘𝑦)) |
16 | 10, 11, 15 | oveq123d 6570 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)) = (𝑥 · (𝐼‘𝑦))) |
17 | 4, 7, 16 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
18 | | df-dvr 18506 |
. . . 4
⊢
/r = (𝑟
∈ V ↦ (𝑥 ∈
(Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r‘𝑟)((invr‘𝑟)‘𝑦)))) |
19 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
20 | 3, 19 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
21 | | fvex 6113 |
. . . . . 6
⊢
(Unit‘𝑅)
∈ V |
22 | 6, 21 | eqeltri 2684 |
. . . . 5
⊢ 𝑈 ∈ V |
23 | 20, 22 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) ∈ V |
24 | 17, 18, 23 | fvmpt 6191 |
. . 3
⊢ (𝑅 ∈ V →
(/r‘𝑅) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
25 | | fvprc 6097 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(/r‘𝑅) =
∅) |
26 | | fvprc 6097 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
27 | 3, 26 | syl5eq 2656 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
28 | | eqid 2610 |
. . . . . 6
⊢ 𝑈 = 𝑈 |
29 | | mpt2eq12 6613 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝑈 = 𝑈) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
30 | 27, 28, 29 | sylancl 693 |
. . . . 5
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
31 | | mpt20 6623 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = ∅ |
32 | 30, 31 | syl6eq 2660 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) = ∅) |
33 | 25, 32 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑅 ∈ V →
(/r‘𝑅) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦)))) |
34 | 24, 33 | pm2.61i 175 |
. 2
⊢
(/r‘𝑅) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) |
35 | 1, 34 | eqtri 2632 |
1
⊢ / = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝑈 ↦ (𝑥 · (𝐼‘𝑦))) |