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 ) )