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 
|- .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 )