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

Metamath Proof Explorer

Theorem tcphtopn

Description: The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphtopn.d 
|- D = ( dist ` G )
tcphtopn.j 
|- J = ( TopOpen ` G )
Assertion tcphtopn 
|- ( W e. V -> J = ( MetOpen ` D ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphtopn.d 
 |-  D = ( dist ` G )
3 tcphtopn.j 
 |-  J = ( TopOpen ` G )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 4 tcphex 
 |-  ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V
6 eqid 
 |-  ( .i ` W ) = ( .i ` W )
7 1 4 6 tcphval 
 |-  G = ( W toNrmGrp ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
8 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
9 7 2 8 tngtopn 
 |-  ( ( W e. V /\ ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V ) -> ( MetOpen ` D ) = ( TopOpen ` G ) )
10 5 9 mpan2 
 |-  ( W e. V -> ( MetOpen ` D ) = ( TopOpen ` G ) )
11 3 10 eqtr4id 
 |-  ( W e. V -> J = ( MetOpen ` D ) )