This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tngtset

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngtset.2 ⊢ 𝐷 = ( dist ‘ 𝑇 )
tngtset.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion tngtset ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( TopSet ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngtset.2 ⊢ 𝐷 = ( dist ‘ 𝑇 )
3 tngtset.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4 ovex ⊢ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) ∈ V
5 fvex ⊢ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ∈ V
6 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
7 6 setsid ⊢ ( ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) ∈ V ∧ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ∈ V ) → ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) ) )
8 4 5 7 mp2an ⊢ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
9 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
10 1 9 tngds ⊢ ( 𝑁 ∈ 𝑊 → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
11 2 10 eqtr4id ⊢ ( 𝑁 ∈ 𝑊 → 𝐷 = ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
12 11 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐷 = ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
13 12 fveq2d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) )
14 3 13 eqtrid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) )
15 eqid ⊢ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( 𝑁 ∘ ( -g ‘ 𝐺 ) )
16 eqid ⊢ ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) = ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
17 1 9 15 16 tngval ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) )
18 17 fveq2d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( TopSet ‘ 𝑇 ) = ( TopSet ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ) ⟩ ) ) )
19 8 14 18 3eqtr4a ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( TopSet ‘ 𝑇 ) )