# 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}=\mathrm{toCPreHil}\left({W}\right)$
tcphtopn.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
tcphtopn.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
Assertion tcphtopn ${⊢}{W}\in {V}\to {J}=\mathrm{MetOpen}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 tcphval.n ${⊢}{G}=\mathrm{toCPreHil}\left({W}\right)$
2 tcphtopn.d ${⊢}{D}=\mathrm{dist}\left({G}\right)$
3 tcphtopn.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
5 4 tcphex ${⊢}\left({x}\in {\mathrm{Base}}_{{W}}⟼\sqrt{{x}{\cdot }_{𝑖}\left({W}\right){x}}\right)\in \mathrm{V}$
6 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
7 1 4 6 tcphval ${⊢}{G}={W}\mathrm{toNrmGrp}\left({x}\in {\mathrm{Base}}_{{W}}⟼\sqrt{{x}{\cdot }_{𝑖}\left({W}\right){x}}\right)$
8 eqid ${⊢}\mathrm{MetOpen}\left({D}\right)=\mathrm{MetOpen}\left({D}\right)$
9 7 2 8 tngtopn ${⊢}\left({W}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{W}}⟼\sqrt{{x}{\cdot }_{𝑖}\left({W}\right){x}}\right)\in \mathrm{V}\right)\to \mathrm{MetOpen}\left({D}\right)=\mathrm{TopOpen}\left({G}\right)$
10 5 9 mpan2 ${⊢}{W}\in {V}\to \mathrm{MetOpen}\left({D}\right)=\mathrm{TopOpen}\left({G}\right)$
11 10 3 syl6reqr ${⊢}{W}\in {V}\to {J}=\mathrm{MetOpen}\left({D}\right)$