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

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