Theorem tcphphl

Description: Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space (because all the original components are the same). (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypothesis	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
Assertion	tcphphl	$$⊢W\in \mathrm{PreHil}\leftrightarrow G\in \mathrm{PreHil}$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		eqidd	$$⊢\top \to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4	1 3	tcphbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
5	4	a1i	$$⊢\top \to {\mathrm{Base}}_W={\mathrm{Base}}_G$$
6		eqid	$$⊢{+}_W={+}_W$$
7	1 6	tchplusg	$$⊢{+}_W={+}_G$$
8	7	a1i	$$⊢\top \to {+}_W={+}_G$$
9	8	oveqdr	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{+}_{W}y=x{+}_{G}y$$
10		eqidd	$$⊢\top \to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
11		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
12	1 11	tcphsca	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(G\right)$$
13	12	a1i	$$⊢\top \to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(G\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
15		eqid	$$⊢{\cdot }_W={\cdot }_W$$
16	1 15	tcphvsca	$$⊢{\cdot }_W={\cdot }_G$$
17	16	a1i	$$⊢\top \to {\cdot }_W={\cdot }_G$$
18	17	oveqdr	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{\cdot }_{W}y=x{\cdot }_{G}y$$
19		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
20	1 19	tcphip	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(G\right)$$
21	20	a1i	$$⊢\top \to {\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(G\right)$$
22	21	oveqdr	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{\cdot }_{𝑖}\left(W\right)y=x{\cdot }_{𝑖}\left(G\right)y$$
23	2 5 9 10 13 14 18 22	phlpropd	$$⊢\top \to \left(W\in \mathrm{PreHil}\leftrightarrow G\in \mathrm{PreHil}\right)$$
24	23	mptru	$$⊢W\in \mathrm{PreHil}\leftrightarrow G\in \mathrm{PreHil}$$