Theorem nmval

Description: The value of the norm as the distance to zero. Problem 1 of Kreyszig p. 63. (Contributed by NM, 4-Dec-2006) (Revised 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	nmval	$$⊢A\in X\to N\left(A\right)=AD\underset{\dot{}}{0}$$

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		oveq1	$$⊢x=A\to xD\underset{\dot{}}{0}=AD\underset{\dot{}}{0}$$
6	1 2 3 4	nmfval	$$⊢N=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
7		ovex	$$⊢AD\underset{\dot{}}{0}\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢A\in X\to N\left(A\right)=AD\underset{\dot{}}{0}$$