This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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