This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )