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	syl5eq	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝐽 = ( 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 ‘ 𝑇 ) )