Theorem ply1ass23l

Description: Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	ply1ass23l.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1ass23l.t	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
	ply1ass23l.b	$$⊢B={\mathrm{Base}}_P$$
	ply1ass23l.k	$$⊢K={\mathrm{Base}}_R$$
	ply1ass23l.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
Assertion	ply1ass23l	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1ass23l.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1ass23l.t	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
3		ply1ass23l.b	$$⊢B={\mathrm{Base}}_P$$
4		ply1ass23l.k	$$⊢K={\mathrm{Base}}_R$$
5		ply1ass23l.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
7		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
8	7	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to 1_{𝑜}\in \mathrm{On}$$
9		simpl	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to R\in \mathrm{Ring}$$
10		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
12	1 11 2	ply1mulr	$$⊢\underset{\dot{}}{\times }={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
13	11 6 12	mplmulr	$$⊢\underset{\dot{}}{\times }={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	11 6 15 14	mplbasss	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\subseteq {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
17	1 3	ply1bascl2	$$⊢X\in B\to X\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	16 17	sseldi	$$⊢X\in B\to X\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
19	18	3ad2ant2	$$⊢\left(A\in K\wedge X\in B\wedge Y\in B\right)\to X\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
20	19	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to X\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
21	1 3	ply1bascl2	$$⊢Y\in B\to Y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
22	16 21	sseldi	$$⊢Y\in B\to Y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
23	22	3ad2ant3	$$⊢\left(A\in K\wedge X\in B\wedge Y\in B\right)\to Y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
24	23	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to Y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
25	1 11 5	ply1vsca	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
26	11 6 25	mplvsca2	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
27		simpr1	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to A\in K$$
28	6 8 9 10 13 14 20 24 4 26 27	psrass23l	$$⊢\left(R\in \mathrm{Ring}\wedge \left(A\in K\wedge X\in B\wedge Y\in B\right)\right)\to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$