Metamath Proof Explorer


Theorem tngplusg

Description: The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngplusg.2 + = ( +g𝐺 )
Assertion tngplusg ( 𝑁𝑉+ = ( +g𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngplusg.2 + = ( +g𝐺 )
3 plusgid +g = Slot ( +g ‘ ndx )
4 tsetndxnplusgndx ( TopSet ‘ ndx ) ≠ ( +g ‘ ndx )
5 4 necomi ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx )
6 dsndxnplusgndx ( dist ‘ ndx ) ≠ ( +g ‘ ndx )
7 6 necomi ( +g ‘ ndx ) ≠ ( dist ‘ ndx )
8 1 3 5 7 tnglem ( 𝑁𝑉 → ( +g𝐺 ) = ( +g𝑇 ) )
9 2 8 eqtrid ( 𝑁𝑉+ = ( +g𝑇 ) )