Theorem tchnmfval

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	tchnmfval	$$⊢W\in \mathrm{Grp}\to N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$

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		eqid	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
6		fvrn0	$$⊢\sqrt{x\underset{\dot{}}{,}x}\in \left(\mathrm{ran}\surd \cup \left\{\varnothing \right\}\right)$$
7	6	a1i	$$⊢x\in V\to \sqrt{x\underset{\dot{}}{,}x}\in \left(\mathrm{ran}\surd \cup \left\{\varnothing \right\}\right)$$
8	5 7	fmpti	$$⊢\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right):V⟶\mathrm{ran}\surd \cup \left\{\varnothing \right\}$$
9	1 3 4	tcphval	$$⊢G=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
10		cnex	$$⊢ℂ\in \mathrm{V}$$
11		sqrtf	$$⊢\surd :ℂ⟶ℂ$$
12		frn	$$⊢\surd :ℂ⟶ℂ\to \mathrm{ran}\surd \subseteq ℂ$$
13	11 12	ax-mp	$$⊢\mathrm{ran}\surd \subseteq ℂ$$
14	10 13	ssexi	$$⊢\mathrm{ran}\surd \in \mathrm{V}$$
15		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
16	14 15	unex	$$⊢\mathrm{ran}\surd \cup \left\{\varnothing \right\}\in \mathrm{V}$$
17	9 3 16	tngnm	$$⊢\left(W\in \mathrm{Grp}\wedge \left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right):V⟶\mathrm{ran}\surd \cup \left\{\varnothing \right\}\right)\to \left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\mathrm{norm}\left(G\right)$$
18	8 17	mpan2	$$⊢W\in \mathrm{Grp}\to \left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\mathrm{norm}\left(G\right)$$
19	2 18	eqtr4id	$$⊢W\in \mathrm{Grp}\to N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$