Theorem tcphval

Description: Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphval.v	$$⊢V={\mathrm{Base}}_W$$
	tcphval.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	tcphval	$$⊢G=W\mathrm{toNrmGrp}\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		tcphval.v	$$⊢V={\mathrm{Base}}_W$$
3		tcphval.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
4		id	$$⊢w=W\to w=W$$
5		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
6	5 2	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=V$$
7		fveq2	$$⊢w=W\to {\cdot }_{𝑖}\left(w\right)={\cdot }_{𝑖}\left(W\right)$$
8	7 3	eqtr4di	$$⊢w=W\to {\cdot }_{𝑖}\left(w\right)=\underset{\dot{}}{,}$$
9	8	oveqd	$$⊢w=W\to x{\cdot }_{𝑖}\left(w\right)x=x\underset{\dot{}}{,}x$$
10	9	fveq2d	$$⊢w=W\to \sqrt{x{\cdot }_{𝑖}\left(w\right)x}=\sqrt{x\underset{\dot{}}{,}x}$$
11	6 10	mpteq12dv	$$⊢w=W\to \left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
12	4 11	oveq12d	$$⊢w=W\to w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
13		df-tcph	$$⊢\mathrm{toCPreHil}=\left(w\in \mathrm{V}⟼w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
14		ovex	$$⊢W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\in \mathrm{V}$$
15	12 13 14	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{toCPreHil}\left(W\right)=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
16		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toCPreHil}\left(W\right)=\varnothing$$
17		reldmtng	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$
18	17	ovprc1	$$⊢\neg W\in \mathrm{V}\to W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)=\varnothing$$
19	16 18	eqtr4d	$$⊢\neg W\in \mathrm{V}\to \mathrm{toCPreHil}\left(W\right)=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
20	15 19	pm2.61i	$$⊢\mathrm{toCPreHil}\left(W\right)=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$
21	1 20	eqtri	$$⊢G=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$