Metamath Proof Explorer

Theorem tngtopn

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

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

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngtset.2 ⊢ 𝐷 = ( dist ‘ 𝑇 )
3 tngtset.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4 1 2 3 tngtset ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( TopSet ‘ 𝑇 ) )
5 df-mopn ⊢ MetOpen = ( 𝑥 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑥 ) ) )
6 5 dmmptss ⊢ dom MetOpen ⊆ ∪ ran ∞Met
7 6 sseli ⊢ ( 𝐷 ∈ dom MetOpen → 𝐷 ∈ ∪ ran ∞Met )
8 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
9 1 8 tngds ⊢ ( 𝑁 ∈ 𝑊 → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
10 9 2 eqtr4di ⊢ ( 𝑁 ∈ 𝑊 → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = 𝐷 )
11 10 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = 𝐷 )
12 11 dmeqd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → dom ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = dom 𝐷 )
13 dmcoss ⊢ dom ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⊆ dom ( -g ‘ 𝐺 )
14 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
15 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
16 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
17 14 15 16 8 grpsubfval ⊢ ( -g ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
18 ovex ⊢ ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ V
19 17 18 dmmpo ⊢ dom ( -g ‘ 𝐺 ) = ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) )
20 13 19 sseqtri ⊢ dom ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) )
21 12 20 eqsstrrdi ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → dom 𝐷 ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
22 21 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom 𝐷 ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
23 dmss ⊢ ( dom 𝐷 ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) → dom dom 𝐷 ⊆ dom ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
24 22 23 syl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 ⊆ dom ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
25 dmxpid ⊢ dom ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐺 )
26 24 25 sseqtrdi ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 ⊆ ( Base ‘ 𝐺 ) )
27 simpr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → 𝐷 ∈ ∪ ran ∞Met )
28 xmetunirn ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
29 27 28 sylib ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
30 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
31 30 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
32 29 31 syl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
33 1 14 tngbas ⊢ ( 𝑁 ∈ 𝑊 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
34 33 ad2antlr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
35 26 32 34 3sstr3d ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → ∪ ( MetOpen ‘ 𝐷 ) ⊆ ( Base ‘ 𝑇 ) )
36 sspwuni ⊢ ( ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) ↔ ∪ ( MetOpen ‘ 𝐷 ) ⊆ ( Base ‘ 𝑇 ) )
37 35 36 sylibr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ 𝐷 ∈ ∪ ran ∞Met ) → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) )
38 37 ex ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝐷 ∈ ∪ ran ∞Met → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) ) )
39 7 38 syl5 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) ) )
40 ndmfv ⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) = ∅ )
41 0ss ⊢ ∅ ⊆ 𝒫 ( Base ‘ 𝑇 )
42 40 41 eqsstrdi ⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) )
43 39 42 pm2.61d1 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) )
44 3 43 eqsstrid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 ⊆ 𝒫 ( Base ‘ 𝑇 ) )
45 4 44 eqsstrrd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( TopSet ‘ 𝑇 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) )
46 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
47 eqid ⊢ ( TopSet ‘ 𝑇 ) = ( TopSet ‘ 𝑇 )
48 46 47 topnid ⊢ ( ( TopSet ‘ 𝑇 ) ⊆ 𝒫 ( Base ‘ 𝑇 ) → ( TopSet ‘ 𝑇 ) = ( TopOpen ‘ 𝑇 ) )
49 45 48 syl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( TopSet ‘ 𝑇 ) = ( TopOpen ‘ 𝑇 ) )
50 4 49 eqtrd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( TopOpen ‘ 𝑇 ) )