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 ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphtopn.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
tcphtopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion tcphtopn ( 𝑊 ∈ 𝑉 → 𝐽 = ( MetOpen ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphtopn.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
3 tcphtopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 4 tcphex ⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∈ V
6 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
7 1 4 6 tcphval ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
8 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
9 7 2 8 tngtopn ⊢ ( ( 𝑊 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∈ V ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐺 ) )
10 5 9 mpan2 ⊢ ( 𝑊 ∈ 𝑉 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐺 ) )
11 3 10 eqtr4id ⊢ ( 𝑊 ∈ 𝑉 → 𝐽 = ( MetOpen ‘ 𝐷 ) )