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 ⊢ T = G toNrmGrp N
tngval.m ⊢ - ˙ = - G
tngval.d ⊢ D = N ∘ - ˙
tngval.j ⊢ J = MetOpen ⁡ D
Assertion tngval ⊢ G ∈ V ∧ N ∈ W → T = G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J

Proof

Step Hyp Ref Expression
1 tngval.t ⊢ T = G toNrmGrp N
2 tngval.m ⊢ - ˙ = - G
3 tngval.d ⊢ D = N ∘ - ˙
4 tngval.j ⊢ J = MetOpen ⁡ D
5 elex ⊢ G ∈ V → G ∈ V
6 elex ⊢ N ∈ W → N ∈ V
7 simpl ⊢ g = G ∧ f = N → g = G
8 simpr ⊢ g = G ∧ f = N → f = N
9 7 fveq2d ⊢ g = G ∧ f = N → - g = - G
10 9 2 eqtr4di ⊢ g = G ∧ f = N → - g = - ˙
11 8 10 coeq12d ⊢ g = G ∧ f = N → f ∘ - g = N ∘ - ˙
12 11 3 eqtr4di ⊢ g = G ∧ f = N → f ∘ - g = D
13 12 opeq2d ⊢ g = G ∧ f = N → dist ⁡ ndx f ∘ - g = dist ⁡ ndx D
14 7 13 oveq12d ⊢ g = G ∧ f = N → g sSet dist ⁡ ndx f ∘ - g = G sSet dist ⁡ ndx D
15 12 fveq2d ⊢ g = G ∧ f = N → MetOpen ⁡ f ∘ - g = MetOpen ⁡ D
16 15 4 eqtr4di ⊢ g = G ∧ f = N → MetOpen ⁡ f ∘ - g = J
17 16 opeq2d ⊢ g = G ∧ f = N → TopSet ⁡ ndx MetOpen ⁡ f ∘ - g = TopSet ⁡ ndx J
18 14 17 oveq12d ⊢ g = G ∧ f = N → g sSet dist ⁡ ndx f ∘ - g sSet TopSet ⁡ ndx MetOpen ⁡ f ∘ - g = G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J
19 df-tng ⊢ toNrmGrp = g ∈ V , f ∈ V ⟼ g sSet dist ⁡ ndx f ∘ - g sSet TopSet ⁡ ndx MetOpen ⁡ f ∘ - g
20 ovex ⊢ G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J ∈ V
21 18 19 20 ovmpoa ⊢ G ∈ V ∧ N ∈ V → G toNrmGrp N = G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J
22 5 6 21 syl2an ⊢ G ∈ V ∧ N ∈ W → G toNrmGrp N = G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J
23 1 22 eqtrid ⊢ G ∈ V ∧ N ∈ W → T = G sSet dist ⁡ ndx D sSet TopSet ⁡ ndx J