Metamath Proof Explorer


Theorem tngval

Description: Value of the function which augments a given structure G with a norm N . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses tngval.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngval.m = ( -g𝐺 )
tngval.d 𝐷 = ( 𝑁 )
tngval.j 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion tngval ( ( 𝐺𝑉𝑁𝑊 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) )

Proof

Step Hyp Ref Expression
1 tngval.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngval.m = ( -g𝐺 )
3 tngval.d 𝐷 = ( 𝑁 )
4 tngval.j 𝐽 = ( MetOpen ‘ 𝐷 )
5 elex ( 𝐺𝑉𝐺 ∈ V )
6 elex ( 𝑁𝑊𝑁 ∈ V )
7 simpl ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → 𝑔 = 𝐺 )
8 simpr ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → 𝑓 = 𝑁 )
9 7 fveq2d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( -g𝑔 ) = ( -g𝐺 ) )
10 9 2 eqtr4di ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( -g𝑔 ) = )
11 8 10 coeq12d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( 𝑓 ∘ ( -g𝑔 ) ) = ( 𝑁 ) )
12 11 3 eqtr4di ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( 𝑓 ∘ ( -g𝑔 ) ) = 𝐷 )
13 12 opeq2d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g𝑔 ) ) ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
14 7 13 oveq12d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g𝑔 ) ) ⟩ ) = ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) )
15 12 fveq2d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( MetOpen ‘ ( 𝑓 ∘ ( -g𝑔 ) ) ) = ( MetOpen ‘ 𝐷 ) )
16 15 4 eqtr4di ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( MetOpen ‘ ( 𝑓 ∘ ( -g𝑔 ) ) ) = 𝐽 )
17 16 opeq2d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g𝑔 ) ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ )
18 14 17 oveq12d ( ( 𝑔 = 𝐺𝑓 = 𝑁 ) → ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g𝑔 ) ) ) ⟩ ) = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) )
19 df-tng toNrmGrp = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g𝑔 ) ) ) ⟩ ) )
20 ovex ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) ∈ V
21 18 19 20 ovmpoa ( ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐺 toNrmGrp 𝑁 ) = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) )
22 5 6 21 syl2an ( ( 𝐺𝑉𝑁𝑊 ) → ( 𝐺 toNrmGrp 𝑁 ) = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) )
23 1 22 syl5eq ( ( 𝐺𝑉𝑁𝑊 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ ) )