Theorem tngipOLD

Description: Obsolete proof of tngip as of 31-Oct-2024. The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

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	tnglemOLD	⊢ ( 𝑁 ∈ 𝑉 → ( ·𝑖 ‘ 𝐺 ) = ( ·𝑖 ‘ 𝑇 ) )
7	2 6	syl5eq	⊢ ( 𝑁 ∈ 𝑉 → , = ( ·𝑖 ‘ 𝑇 ) )