This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tng0

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

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

Proof

Step Hyp Ref Expression
1 tngbas.t 
 |-  T = ( G toNrmGrp N )
2 tng0.2 
 |-  .0. = ( 0g ` G )
3 eqidd 
 |-  ( N e. V -> ( Base ` G ) = ( Base ` G ) )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 1 4 tngbas 
 |-  ( N e. V -> ( Base ` G ) = ( Base ` T ) )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 1 6 tngplusg 
 |-  ( N e. V -> ( +g ` G ) = ( +g ` T ) )
8 7 oveqdr 
 |-  ( ( N e. V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` T ) y ) )
9 3 5 8 grpidpropd 
 |-  ( N e. V -> ( 0g ` G ) = ( 0g ` T ) )
10 2 9 eqtrid 
 |-  ( N e. V -> .0. = ( 0g ` T ) )