Step | Hyp | Ref
| Expression |
1 | | nmfval.n |
. 2
⊢ 𝑁 = (norm‘𝑊) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | nmfval.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝑊) |
4 | 2, 3 | syl6eqr 2662 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑋) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (dist‘𝑤) = (dist‘𝑊)) |
6 | | nmfval.d |
. . . . . . 7
⊢ 𝐷 = (dist‘𝑊) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (dist‘𝑤) = 𝐷) |
8 | | eqidd 2611 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
9 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
10 | | nmfval.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) |
12 | 7, 8, 11 | oveq123d 6570 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥(dist‘𝑤)(0g‘𝑤)) = (𝑥𝐷 0 )) |
13 | 4, 12 | mpteq12dv 4663 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤))) = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 ))) |
14 | | df-nm 22197 |
. . . 4
⊢ norm =
(𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤)))) |
15 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) |
16 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑥𝐷 0 ) = (𝐷‘〈𝑥, 0 〉) |
17 | | fvrn0 6126 |
. . . . . . . 8
⊢ (𝐷‘〈𝑥, 0 〉) ∈ (ran 𝐷 ∪
{∅}) |
18 | 16, 17 | eqeltri 2684 |
. . . . . . 7
⊢ (𝑥𝐷 0 ) ∈ (ran 𝐷 ∪
{∅}) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → (𝑥𝐷 0 ) ∈ (ran 𝐷 ∪
{∅})) |
20 | 15, 19 | fmpti 6291 |
. . . . 5
⊢ (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )):𝑋⟶(ran 𝐷 ∪ {∅}) |
21 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑊)
∈ V |
22 | 3, 21 | eqeltri 2684 |
. . . . 5
⊢ 𝑋 ∈ V |
23 | | fvex 6113 |
. . . . . . . 8
⊢
(dist‘𝑊)
∈ V |
24 | 6, 23 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐷 ∈ V |
25 | 24 | rnex 6992 |
. . . . . 6
⊢ ran 𝐷 ∈ V |
26 | | p0ex 4779 |
. . . . . 6
⊢ {∅}
∈ V |
27 | 25, 26 | unex 6854 |
. . . . 5
⊢ (ran
𝐷 ∪ {∅}) ∈
V |
28 | | fex2 7014 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )):𝑋⟶(ran 𝐷 ∪ {∅}) ∧ 𝑋 ∈ V ∧ (ran 𝐷 ∪ {∅}) ∈ V) → (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) ∈
V) |
29 | 20, 22, 27, 28 | mp3an 1416 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) ∈
V |
30 | 13, 14, 29 | fvmpt 6191 |
. . 3
⊢ (𝑊 ∈ V →
(norm‘𝑊) = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 ))) |
31 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝑊 ∈ V →
(norm‘𝑊) =
∅) |
32 | | mpt0 5934 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 )) =
∅ |
33 | 31, 32 | syl6eqr 2662 |
. . . 4
⊢ (¬
𝑊 ∈ V →
(norm‘𝑊) = (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 ))) |
34 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
35 | 3, 34 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑊 ∈ V → 𝑋 = ∅) |
36 | 35 | mpteq1d 4666 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) = (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 ))) |
37 | 33, 36 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑊 ∈ V →
(norm‘𝑊) = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 ))) |
38 | 30, 37 | pm2.61i 175 |
. 2
⊢
(norm‘𝑊) =
(𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) |
39 | 1, 38 | eqtri 2632 |
1
⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) |