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	syl5eq	|- ( N e. V -> .0. = ( 0g ` T ) )