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 = ( toCPreHil ` W )
Assertion	tcphphl	|- ( W e. PreHil <-> G e. PreHil )

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	|- G = ( toCPreHil ` W )
2		eqidd	|- ( T. -> ( Base ` W ) = ( Base ` W ) )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4	1 3	tcphbas	|- ( Base ` W ) = ( Base ` G )
5	4	a1i	|- ( T. -> ( Base ` W ) = ( Base ` G ) )
6		eqid	|- ( +g ` W ) = ( +g ` W )
7	1 6	tchplusg	|- ( +g ` W ) = ( +g ` G )
8	7	a1i	|- ( T. -> ( +g ` W ) = ( +g ` G ) )
9	8	oveqdr	|- ( ( T. /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` G ) y ) )
10		eqidd	|- ( T. -> ( Scalar ` W ) = ( Scalar ` W ) )
11		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
12	1 11	tcphsca	|- ( Scalar ` W ) = ( Scalar ` G )
13	12	a1i	|- ( T. -> ( Scalar ` W ) = ( Scalar ` G ) )
14		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
15		eqid	|- ( .s ` W ) = ( .s ` W )
16	1 15	tcphvsca	|- ( .s ` W ) = ( .s ` G )
17	16	a1i	|- ( T. -> ( .s ` W ) = ( .s ` G ) )
18	17	oveqdr	|- ( ( T. /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( x ( .s ` W ) y ) = ( x ( .s ` G ) y ) )
19		eqid	|- ( .i ` W ) = ( .i ` W )
20	1 19	tcphip	|- ( .i ` W ) = ( .i ` G )
21	20	a1i	|- ( T. -> ( .i ` W ) = ( .i ` G ) )
22	21	oveqdr	|- ( ( T. /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .i ` W ) y ) = ( x ( .i ` G ) y ) )
23	2 5 9 10 13 14 18 22	phlpropd	|- ( T. -> ( W e. PreHil <-> G e. PreHil ) )
24	23	mptru	|- ( W e. PreHil <-> G e. PreHil )