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\mathrm{toNrmGrp}N$$
	tngip.2	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(G\right)$$
Assertion	tngip	$$⊢N\in V\to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tngip.2	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(G\right)$$
3		ipid	$$⊢{\cdot }_{𝑖}=\mathrm{Slot}{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
4		slotstnscsi	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\right)$$
5	4	simp3i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
6	5	necomi	$$⊢{\cdot }_{𝑖}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
7		slotsdnscsi	$$⊢\left(\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\right)$$
8	7	simp3i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
9	8	necomi	$$⊢{\cdot }_{𝑖}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
10	1 3 6 9	tnglem	$$⊢N\in V\to {\cdot }_{𝑖}\left(G\right)={\cdot }_{𝑖}\left(T\right)$$
11	2 10	eqtrid	$$⊢N\in V\to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(T\right)$$