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

Metamath Proof Explorer

Theorem tngip

Description: The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses tngbas.t ⊢ T = G toNrmGrp N
tngip.2 ⊢ , ˙ = ⋅ 𝑖 ⁡ G
Assertion tngip ⊢ N ∈ V → , ˙ = ⋅ 𝑖 ⁡ T

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ T = G toNrmGrp N
2 tngip.2 ⊢ , ˙ = ⋅ 𝑖 ⁡ G
3 ipid ⊢ ⋅ 𝑖 = Slot ⋅ 𝑖 ⁡ ndx
4 slotstnscsi ⊢ TopSet ⁡ ndx ≠ Scalar ⁡ ndx ∧ TopSet ⁡ ndx ≠ ⋅ ndx ∧ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
5 4 simp3i ⊢ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
6 5 necomi ⊢ ⋅ 𝑖 ⁡ ndx ≠ TopSet ⁡ ndx
7 slotsdnscsi ⊢ dist ⁡ ndx ≠ Scalar ⁡ ndx ∧ dist ⁡ ndx ≠ ⋅ ndx ∧ dist ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
8 7 simp3i ⊢ dist ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
9 8 necomi ⊢ ⋅ 𝑖 ⁡ ndx ≠ dist ⁡ ndx
10 1 3 6 9 tnglem ⊢ N ∈ V → ⋅ 𝑖 ⁡ G = ⋅ 𝑖 ⁡ T
11 2 10 eqtrid ⊢ N ∈ V → , ˙ = ⋅ 𝑖 ⁡ T