Theorem vscaid

Description: Utility theorem: index-independent form of scalar product df-vsca . (Contributed by Mario Carneiro, 2-Oct-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Assertion	vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$

Proof

Step	Hyp	Ref	Expression
1		df-vsca	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}6$$
2		6nn	$$⊢6\in \mathbb{N}$$
3	1 2	ndxid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$