Theorem tcphnmval

Description: The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphnmval.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	tcphnmval.v	$$⊢V={\mathrm{Base}}_W$$
	tcphnmval.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	tcphnmval	$$⊢\left(W\in \mathrm{Grp}\wedge X\in V\right)\to N\left(X\right)=\sqrt{X\underset{\dot{}}{,}X}$$

Proof

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