Metamath Proof Explorer


Theorem nmfval

Description: The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval.n N = norm W
nmfval.x X = Base W
nmfval.z 0 ˙ = 0 W
nmfval.d D = dist W
Assertion nmfval N = x X x D 0 ˙

Proof

Step Hyp Ref Expression
1 nmfval.n N = norm W
2 nmfval.x X = Base W
3 nmfval.z 0 ˙ = 0 W
4 nmfval.d D = dist W
5 fveq2 w = W Base w = Base W
6 5 2 eqtr4di w = W Base w = X
7 fveq2 w = W dist w = dist W
8 7 4 eqtr4di w = W dist w = D
9 eqidd w = W x = x
10 fveq2 w = W 0 w = 0 W
11 10 3 eqtr4di w = W 0 w = 0 ˙
12 8 9 11 oveq123d w = W x dist w 0 w = x D 0 ˙
13 6 12 mpteq12dv w = W x Base w x dist w 0 w = x X x D 0 ˙
14 df-nm norm = w V x Base w x dist w 0 w
15 eqid x X x D 0 ˙ = x X x D 0 ˙
16 df-ov x D 0 ˙ = D x 0 ˙
17 fvrn0 D x 0 ˙ ran D
18 16 17 eqeltri x D 0 ˙ ran D
19 18 a1i x X x D 0 ˙ ran D
20 15 19 fmpti x X x D 0 ˙ : X ran D
21 2 fvexi X V
22 4 fvexi D V
23 22 rnex ran D V
24 p0ex V
25 23 24 unex ran D V
26 fex2 x X x D 0 ˙ : X ran D X V ran D V x X x D 0 ˙ V
27 20 21 25 26 mp3an x X x D 0 ˙ V
28 13 14 27 fvmpt W V norm W = x X x D 0 ˙
29 fvprc ¬ W V norm W =
30 mpt0 x x D 0 ˙ =
31 29 30 eqtr4di ¬ W V norm W = x x D 0 ˙
32 fvprc ¬ W V Base W =
33 2 32 syl5eq ¬ W V X =
34 33 mpteq1d ¬ W V x X x D 0 ˙ = x x D 0 ˙
35 31 34 eqtr4d ¬ W V norm W = x X x D 0 ˙
36 28 35 pm2.61i norm W = x X x D 0 ˙
37 1 36 eqtri N = x X x D 0 ˙