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