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	$⊢ Y = {Poly}_{1} (R)$
		ply1plusg.s	$⊢ S = 1_{𝑜} mPoly R$
		ply1vscafval.n	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	Assertion	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{S}$

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	$⊢ Y = {Poly}_{1} (R)$
2		ply1plusg.s	$⊢ S = 1_{𝑜} mPoly R$
3		ply1vscafval.n	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
4		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
5		eqid	$⊢ \cdot_{S} = \cdot_{S}$
6	2 4 5	mplvsca2	$⊢ \cdot_{S} = \cdot_{(1_{𝑜} mPwSer R)}$
7		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
8		eqid	$⊢ \cdot_{{PwSer}_{1} (R)} = \cdot_{{PwSer}_{1} (R)}$
9	7 4 8	psr1vsca	$⊢ \cdot_{{PwSer}_{1} (R)} = \cdot_{(1_{𝑜} mPwSer R)}$
10		fvex	$⊢ {Base}_{(1_{𝑜} mPoly R)} \in V$
11	1 7	ply1val	$⊢ Y = {PwSer}_{1} (R) ↾_{𝑠} {Base}_{(1_{𝑜} mPoly R)}$
12	11 8	ressvsca	$⊢ {Base}_{(1_{𝑜} mPoly R)} \in V \to \cdot_{{PwSer}_{1} (R)} = \cdot_{Y}$
13	10 12	ax-mp	$⊢ \cdot_{{PwSer}_{1} (R)} = \cdot_{Y}$
14	6 9 13	3eqtr2i	$⊢ \cdot_{S} = \cdot_{Y}$
15	3 14	eqtr4i	$⊢ \underset{˙}{\cdot} = \cdot_{S}$