Theorem tcphbas

Description: The base set 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)$$
	tcphbas.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	tcphbas	$$⊢V={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphbas.v	$$⊢V={\mathrm{Base}}_W$$
3	2	tcphex	$$⊢\left(x\in V⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}$$
4		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
5	1 2 4	tcphval	$$⊢G=W\mathrm{toNrmGrp}\left(x\in V⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
6	5 2	tngbas	$$⊢\left(x\in V⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}\to V={\mathrm{Base}}_G$$
7	3 6	ax-mp	$$⊢V={\mathrm{Base}}_G$$