Theorem psr1mulr

Description: Value of 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	$$⊢Y={\mathrm{PwSer}}_1\left(R\right)$$
	psr1plusg.s	$$⊢S=1_{𝑜}\mathrm{mPwSer}R$$
	psr1mulr.n	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
Assertion	psr1mulr	$$⊢\underset{\dot{}}{·}={\cdot }_S$$

Proof

Step	Hyp	Ref	Expression
1		psr1plusg.y	$$⊢Y={\mathrm{PwSer}}_1\left(R\right)$$
2		psr1plusg.s	$$⊢S=1_{𝑜}\mathrm{mPwSer}R$$
3		psr1mulr.n	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4	1	psr1val	$$⊢Y=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
5		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
6	5	a1i	$$⊢\top \to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
7	2 4 6	opsrmulr	$$⊢\top \to {\cdot }_S={\cdot }_Y$$
8	7	mptru	$$⊢{\cdot }_S={\cdot }_Y$$
9	3 8	eqtr4i	$$⊢\underset{\dot{}}{·}={\cdot }_S$$