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	⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		df-vsca	⊢ ·𝑠 = Slot 6
2		6nn	⊢ 6 ∈ ℕ
3	1 2	ndxid	⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )