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 ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tng0.2 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion tng0 ( 𝑁 ∈ 𝑉 → 0 = ( 0g ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tng0.2 ⊢ 0 = ( 0g ‘ 𝐺 )
3 eqidd ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 4 tngbas ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 1 6 tngplusg ⊢ ( 𝑁 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
8 7 oveqdr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
9 3 5 8 grpidpropd ⊢ ( 𝑁 ∈ 𝑉 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑇 ) )
10 2 9 eqtrid ⊢ ( 𝑁 ∈ 𝑉 → 0 = ( 0g ‘ 𝑇 ) )