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 ) , 𝐽 ⟩ ) )