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 syl5eq G V N W T = G sSet dist ndx D sSet TopSet ndx J