Theorem cphnm

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmsq.v	$$⊢V={\mathrm{Base}}_W$$
	nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	nmsq.n	$$⊢N=\mathrm{norm}\left(W\right)$$
Assertion	cphnm	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to N\left(A\right)=\sqrt{A\underset{\dot{}}{,}A}$$

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	$$⊢V={\mathrm{Base}}_W$$
2		nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		nmsq.n	$$⊢N=\mathrm{norm}\left(W\right)$$
4	1 2 3	cphnmfval	$$⊢W\in \mathrm{CPreHil}\to N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
5	4	fveq1d	$$⊢W\in \mathrm{CPreHil}\to N\left(A\right)=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\left(A\right)$$
6		oveq12	$$⊢\left(x=A\wedge x=A\right)\to x\underset{\dot{}}{,}x=A\underset{\dot{}}{,}A$$
7	6	anidms	$$⊢x=A\to x\underset{\dot{}}{,}x=A\underset{\dot{}}{,}A$$
8	7	fveq2d	$$⊢x=A\to \sqrt{x\underset{\dot{}}{,}x}=\sqrt{A\underset{\dot{}}{,}A}$$
9		eqid	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
10		fvex	$$⊢\sqrt{A\underset{\dot{}}{,}A}\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢A\in V\to \left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\left(A\right)=\sqrt{A\underset{\dot{}}{,}A}$$
12	5 11	sylan9eq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to N\left(A\right)=\sqrt{A\underset{\dot{}}{,}A}$$