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	|- .s = Slot ( .s ` ndx )

Proof

Step	Hyp	Ref	Expression
1		df-vsca	|- .s = Slot 6
2		6nn	|- 6 e. NN
3	1 2	ndxid	|- .s = Slot ( .s ` ndx )