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 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 Base W x 𝑖 W x V
6 eqid 𝑖 W = 𝑖 W
7 1 4 6 tcphval G = W toNrmGrp x Base W x 𝑖 W x
8 eqid MetOpen D = MetOpen D
9 7 2 8 tngtopn W V x Base W x 𝑖 W x V MetOpen D = TopOpen G
10 5 9 mpan2 W V MetOpen D = TopOpen G
11 3 10 eqtr4id W V J = MetOpen D