Theorem tngsca

Description: The scalar ring 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$$
	tngsca.2	$$⊢F=\mathrm{Scalar}\left(G\right)$$
Assertion	tngsca	$$⊢N\in V\to F=\mathrm{Scalar}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		tngbas.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		tngsca.2	$$⊢F=\mathrm{Scalar}\left(G\right)$$
3		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\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	simp1i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
6	5	necomi	$$⊢\mathrm{Scalar}\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	simp1i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
9	8	necomi	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
10	1 3 6 9	tnglem	$$⊢N\in V\to \mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(T\right)$$
11	2 10	eqtrid	$$⊢N\in V\to F=\mathrm{Scalar}\left(T\right)$$