Theorem tngvsca

Description: The scalar multiplication 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$$
	tngvsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	tngvsca	$$⊢N\in V\to \underset{\dot{}}{·}={\cdot }_T$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tngvsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
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	simp2i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
6	5	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\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	simp2i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
9	8	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
10	1 3 6 9	tnglem	$$⊢N\in V\to {\cdot }_G={\cdot }_T$$
11	2 10	eqtrid	$$⊢N\in V\to \underset{\dot{}}{·}={\cdot }_T$$