Theorem tngip

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

	Ref	Expression
Hypotheses	tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tngip.2	⊢ , = ( ·𝑖 ‘ 𝐺 )
Assertion	tngip	⊢ ( 𝑁 ∈ 𝑉 → , = ( ·𝑖 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tngip.2	⊢ , = ( ·𝑖 ‘ 𝐺 )
3		df-ip	⊢ ·𝑖 = Slot 8
4		8nn	⊢ 8 ∈ ℕ
5		8lt9	⊢ 8 < 9
6	1 3 4 5	tnglem	⊢ ( 𝑁 ∈ 𝑉 → ( ·𝑖 ‘ 𝐺 ) = ( ·𝑖 ‘ 𝑇 ) )
7	2 6	syl5eq	⊢ ( 𝑁 ∈ 𝑉 → , = ( ·𝑖 ‘ 𝑇 ) )