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

Metamath Proof Explorer

Theorem ply1vsca

Description: Value of scalar multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

		Ref	Expression
	Hypotheses	ply1plusg.y	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
		ply1plusg.s	⊢ 𝑆 = ( 1_o mPoly 𝑅 )
		ply1vscafval.n	⊢ · = ( ·_𝑠 ‘ 𝑌 )
	Assertion	ply1vsca	⊢ · = ( ·_𝑠 ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
2		ply1plusg.s	⊢ 𝑆 = ( 1_o mPoly 𝑅 )
3		ply1vscafval.n	⊢ · = ( ·_𝑠 ‘ 𝑌 )
4		eqid	⊢ ( 1_o mPwSer 𝑅 ) = ( 1_o mPwSer 𝑅 )
5		eqid	⊢ ( ·_𝑠 ‘ 𝑆 ) = ( ·_𝑠 ‘ 𝑆 )
6	2 4 5	mplvsca2	⊢ ( ·_𝑠 ‘ 𝑆 ) = ( ·_𝑠 ‘ ( 1_o mPwSer 𝑅 ) )
7		eqid	⊢ ( PwSer₁ ‘ 𝑅 ) = ( PwSer₁ ‘ 𝑅 )
8		eqid	⊢ ( ·_𝑠 ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ·_𝑠 ‘ ( PwSer₁ ‘ 𝑅 ) )
9	7 4 8	psr1vsca	⊢ ( ·_𝑠 ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ·_𝑠 ‘ ( 1_o mPwSer 𝑅 ) )
10		fvex	⊢ ( Base ‘ ( 1_o mPoly 𝑅 ) ) ∈ V
11	1 7	ply1val	⊢ 𝑌 = ( ( PwSer₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( 1_o mPoly 𝑅 ) ) )
12	11 8	ressvsca	⊢ ( ( Base ‘ ( 1_o mPoly 𝑅 ) ) ∈ V → ( ·_𝑠 ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ·_𝑠 ‘ 𝑌 ) )
13	10 12	ax-mp	⊢ ( ·_𝑠 ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ·_𝑠 ‘ 𝑌 )
14	6 9 13	3eqtr2i	⊢ ( ·_𝑠 ‘ 𝑆 ) = ( ·_𝑠 ‘ 𝑌 )
15	3 14	eqtr4i	⊢ · = ( ·_𝑠 ‘ 𝑆 )