Metamath Proof Explorer


Theorem psr1vsca

Description: Value of scalar multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psr1plusg.y 𝑌 = ( PwSer1𝑅 )
psr1plusg.s 𝑆 = ( 1o mPwSer 𝑅 )
psr1vscafval.n · = ( ·𝑠𝑌 )
Assertion psr1vsca · = ( ·𝑠𝑆 )

Proof

Step Hyp Ref Expression
1 psr1plusg.y 𝑌 = ( PwSer1𝑅 )
2 psr1plusg.s 𝑆 = ( 1o mPwSer 𝑅 )
3 psr1vscafval.n · = ( ·𝑠𝑌 )
4 1 psr1val 𝑌 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
5 0ss ∅ ⊆ ( 1o × 1o )
6 5 a1i ( ⊤ → ∅ ⊆ ( 1o × 1o ) )
7 2 4 6 opsrvsca ( ⊤ → ( ·𝑠𝑆 ) = ( ·𝑠𝑌 ) )
8 7 mptru ( ·𝑠𝑆 ) = ( ·𝑠𝑌 )
9 3 8 eqtr4i · = ( ·𝑠𝑆 )