Metamath Proof Explorer


Theorem opsrvsca

Description: The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

Ref Expression
Hypotheses opsrbas.s
|- S = ( I mPwSer R )
opsrbas.o
|- O = ( ( I ordPwSer R ) ` T )
opsrbas.t
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrvsca
|- ( ph -> ( .s ` S ) = ( .s ` O ) )

Proof

Step Hyp Ref Expression
1 opsrbas.s
 |-  S = ( I mPwSer R )
2 opsrbas.o
 |-  O = ( ( I ordPwSer R ) ` T )
3 opsrbas.t
 |-  ( ph -> T C_ ( I X. I ) )
4 vscaid
 |-  .s = Slot ( .s ` ndx )
5 plendxnvscandx
 |-  ( le ` ndx ) =/= ( .s ` ndx )
6 5 necomi
 |-  ( .s ` ndx ) =/= ( le ` ndx )
7 1 2 3 4 6 opsrbaslem
 |-  ( ph -> ( .s ` S ) = ( .s ` O ) )