Metamath Proof Explorer


Theorem tngplusg

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

Ref Expression
Hypotheses tngbas.t
|- T = ( G toNrmGrp N )
tngplusg.2
|- .+ = ( +g ` G )
Assertion tngplusg
|- ( N e. V -> .+ = ( +g ` T ) )

Proof

Step Hyp Ref Expression
1 tngbas.t
 |-  T = ( G toNrmGrp N )
2 tngplusg.2
 |-  .+ = ( +g ` G )
3 df-plusg
 |-  +g = Slot 2
4 2nn
 |-  2 e. NN
5 2lt9
 |-  2 < 9
6 1 3 4 5 tnglem
 |-  ( N e. V -> ( +g ` G ) = ( +g ` T ) )
7 2 6 syl5eq
 |-  ( N e. V -> .+ = ( +g ` T ) )