# 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}=\mathrm{norm}\left({W}\right)$
nmfval.x ${⊢}{X}={\mathrm{Base}}_{{W}}$
nmfval.z
nmfval.d ${⊢}{D}=\mathrm{dist}\left({W}\right)$
Assertion nmfval

### Proof

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