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\mathrm{toNrmGrp}N$$
	tng0.2	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	tng0	$$⊢N\in V\to \underset{\dot{}}{0}=0_T$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tng0.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqidd	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	1 4	tngbas	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_T$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6	tngplusg	$$⊢N\in V\to {+}_G={+}_T$$
8	7	oveqdr	$$⊢\left(N\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{T}y$$
9	3 5 8	grpidpropd	$$⊢N\in V\to 0_G=0_T$$
10	2 9	syl5eq	$$⊢N\in V\to \underset{\dot{}}{0}=0_T$$