Theorem ipnm

Description: Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipid.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ipid.6	$$⊢N={norm}_{CV}\left(U\right)$$
	ipid.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	ipnm	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)=\sqrt{APA}$$

Proof

Step	Hyp	Ref	Expression
1		ipid.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ipid.6	$$⊢N={norm}_{CV}\left(U\right)$$
3		ipid.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
4	1 2 3	ipidsq	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to APA={N\left(A\right)}^2$$
5	4	fveq2d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to \sqrt{APA}=\sqrt{{N\left(A\right)}^2}$$
6	1 2	nvcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$
7	1 2	nvge0	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to 0\le N\left(A\right)$$
8	6 7	sqrtsqd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to \sqrt{{N\left(A\right)}^2}=N\left(A\right)$$
9	5 8	eqtr2d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)=\sqrt{APA}$$