Theorem nmfval

Description: The value of the norm function as the distance to zero. (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	$$⊢\underset{\dot{}}{0}=0_W$$
	nmfval.d	$$⊢D=\mathrm{dist}\left(W\right)$$
Assertion	nmfval	$$⊢N=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmfval.n	$$⊢N=\mathrm{norm}\left(W\right)$$
2		nmfval.x	$$⊢X={\mathrm{Base}}_W$$
3		nmfval.z	$$⊢\underset{\dot{}}{0}=0_W$$
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	$$⊢w=W\to 0_w=\underset{\dot{}}{0}$$
12	8 9 11	oveq123d	$$⊢w=W\to x\mathrm{dist}\left(w\right)0_w=xD\underset{\dot{}}{0}$$
13	6 12	mpteq12dv	$$⊢w=W\to \left(x\in {\mathrm{Base}}_w⟼x\mathrm{dist}\left(w\right)0_w\right)=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
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	$$⊢\left(x\in X⟼xD\underset{\dot{}}{0}\right)=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
16		df-ov	$$⊢xD\underset{\dot{}}{0}=D\left(⟨x,\underset{\dot{}}{0}⟩\right)$$
17		fvrn0	$$⊢D\left(⟨x,\underset{\dot{}}{0}⟩\right)\in \left(\mathrm{ran}D\cup \left\{\varnothing \right\}\right)$$
18	16 17	eqeltri	$$⊢xD\underset{\dot{}}{0}\in \left(\mathrm{ran}D\cup \left\{\varnothing \right\}\right)$$
19	18	a1i	$$⊢x\in X\to xD\underset{\dot{}}{0}\in \left(\mathrm{ran}D\cup \left\{\varnothing \right\}\right)$$
20	15 19	fmpti	$$⊢\left(x\in X⟼xD\underset{\dot{}}{0}\right):X⟶\mathrm{ran}D\cup \left\{\varnothing \right\}$$
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	$$⊢\left(\left(x\in X⟼xD\underset{\dot{}}{0}\right):X⟶\mathrm{ran}D\cup \left\{\varnothing \right\}\wedge X\in \mathrm{V}\wedge \mathrm{ran}D\cup \left\{\varnothing \right\}\in \mathrm{V}\right)\to \left(x\in X⟼xD\underset{\dot{}}{0}\right)\in \mathrm{V}$$
27	20 21 25 26	mp3an	$$⊢\left(x\in X⟼xD\underset{\dot{}}{0}\right)\in \mathrm{V}$$
28	13 14 27	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{norm}\left(W\right)=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
29		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{norm}\left(W\right)=\varnothing$$
30		mpt0	$$⊢\left(x\in \varnothing ⟼xD\underset{\dot{}}{0}\right)=\varnothing$$
31	29 30	eqtr4di	$$⊢\neg W\in \mathrm{V}\to \mathrm{norm}\left(W\right)=\left(x\in \varnothing ⟼xD\underset{\dot{}}{0}\right)$$
32		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
33	2 32	syl5eq	$$⊢\neg W\in \mathrm{V}\to X=\varnothing$$
34	33	mpteq1d	$$⊢\neg W\in \mathrm{V}\to \left(x\in X⟼xD\underset{\dot{}}{0}\right)=\left(x\in \varnothing ⟼xD\underset{\dot{}}{0}\right)$$
35	31 34	eqtr4d	$$⊢\neg W\in \mathrm{V}\to \mathrm{norm}\left(W\right)=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
36	28 35	pm2.61i	$$⊢\mathrm{norm}\left(W\right)=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
37	1 36	eqtri	$$⊢N=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$