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 ˙ = 0 G
Assertion tng0 ⊢ N ∈ V → 0 ˙ = 0 T

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ T = G toNrmGrp N
2 tng0.2 ⊢ 0 ˙ = 0 G
3 eqidd ⊢ N ∈ V → Base G = Base G
4 eqid ⊢ Base G = Base G
5 1 4 tngbas ⊢ N ∈ V → Base G = Base T
6 eqid ⊢ + G = + G
7 1 6 tngplusg ⊢ N ∈ V → + G = + T
8 7 oveqdr ⊢ N ∈ V ∧ x ∈ Base G ∧ y ∈ Base G → x + G y = x + T y
9 3 5 8 grpidpropd ⊢ N ∈ V → 0 G = 0 T
10 2 9 eqtrid ⊢ N ∈ V → 0 ˙ = 0 T