Theorem mplmon2mul

Description: Product of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	mplmon2cl.p	$$⊢P=I\mathrm{mPoly}R$$
	mplmon2cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplmon2cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplmon2cl.c	$$⊢C={\mathrm{Base}}_R$$
	mplmon2cl.i	$$⊢\phi \to I\in W$$
	mplmon2mul.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mplmon2mul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	mplmon2mul.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mplmon2mul.x	$$⊢\phi \to X\in D$$
	mplmon2mul.y	$$⊢\phi \to Y\in D$$
	mplmon2mul.f	$$⊢\phi \to F\in C$$
	mplmon2mul.g	$$⊢\phi \to G\in C$$
Assertion	mplmon2mul	$$⊢\phi \to \left(y\in D⟼if\left(y=X,F,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,G,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,F\underset{\dot{}}{·}G,\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplmon2cl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplmon2cl.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplmon2cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplmon2cl.c	$$⊢C={\mathrm{Base}}_R$$
5		mplmon2cl.i	$$⊢\phi \to I\in W$$
6		mplmon2mul.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		mplmon2mul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
8		mplmon2mul.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9		mplmon2mul.x	$$⊢\phi \to X\in D$$
10		mplmon2mul.y	$$⊢\phi \to Y\in D$$
11		mplmon2mul.f	$$⊢\phi \to F\in C$$
12		mplmon2mul.g	$$⊢\phi \to G\in C$$
13	1	mplassa	$$⊢\left(I\in W\wedge R\in \mathrm{CRing}\right)\to P\in \mathrm{AssAlg}$$
14	5 6 13	syl2anc	$$⊢\phi \to P\in \mathrm{AssAlg}$$
15	1 5 6	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
16	15	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
17	4 16	syl5eq	$$⊢\phi \to C={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
18	11 17	eleqtrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
19		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
20		eqid	$$⊢1_R=1_R$$
21		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
22	6 21	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
23	1 19 3 20 2 5 22 9	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
24		assalmod	$$⊢P\in \mathrm{AssAlg}\to P\in \mathrm{LMod}$$
25	14 24	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
26	12 17	eleqtrd	$$⊢\phi \to G\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
27	1 19 3 20 2 5 22 10	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
28		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
29		eqid	$$⊢{\cdot }_P={\cdot }_P$$
30		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
31	19 28 29 30	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge G\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\right)\to G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
32	25 26 27 31	syl3anc	$$⊢\phi \to G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
33	19 28 30 29 7	assaass	$$⊢\left(P\in \mathrm{AssAlg}\wedge \left(F\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\wedge G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\right)\right)\to \left(F{\cdot }_P\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=F{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)$$
34	14 18 23 32 33	syl13anc	$$⊢\phi \to \left(F{\cdot }_P\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=F{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)$$
35	19 28 30 29 7	assaassr	$$⊢\left(P\in \mathrm{AssAlg}\wedge \left(G\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\wedge \left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\right)\right)\to \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
36	14 26 23 27 35	syl13anc	$$⊢\phi \to \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
37	36	oveq2d	$$⊢\phi \to F{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)=F{\cdot }_P\left(G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)$$
38	1 19 3 20 2 5 22 9 7 10	mplmonmul	$$⊢\phi \to \left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)$$
39	38	oveq2d	$$⊢\phi \to G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=G{\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)$$
40	39	oveq2d	$$⊢\phi \to F{\cdot }_P\left(G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)=F{\cdot }_P\left(G{\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
41	2	psrbagaddcl	$$⊢\left(X\in D\wedge Y\in D\right)\to X{+}_{f}Y\in D$$
42	9 10 41	syl2anc	$$⊢\phi \to X{+}_{f}Y\in D$$
43	1 19 3 20 2 5 22 42	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
44		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(P\right)}={\cdot }_{\mathrm{Scalar}\left(P\right)}$$
45	19 28 29 30 44	lmodvsass	$$⊢\left(P\in \mathrm{LMod}\wedge \left(F\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge G\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P\right)\right)\to \left(F{\cdot }_{\mathrm{Scalar}\left(P\right)}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)=F{\cdot }_P\left(G{\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
46	25 18 26 43 45	syl13anc	$$⊢\phi \to \left(F{\cdot }_{\mathrm{Scalar}\left(P\right)}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)=F{\cdot }_P\left(G{\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)\right)$$
47	15	fveq2d	$$⊢\phi \to {\cdot }_R={\cdot }_{\mathrm{Scalar}\left(P\right)}$$
48	8 47	syl5req	$$⊢\phi \to {\cdot }_{\mathrm{Scalar}\left(P\right)}=\underset{\dot{}}{·}$$
49	48	oveqd	$$⊢\phi \to F{\cdot }_{\mathrm{Scalar}\left(P\right)}G=F\underset{\dot{}}{·}G$$
50	49	oveq1d	$$⊢\phi \to \left(F{\cdot }_{\mathrm{Scalar}\left(P\right)}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)=\left(F\underset{\dot{}}{·}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)$$
51	40 46 50	3eqtr2d	$$⊢\phi \to F{\cdot }_P\left(G{\cdot }_P\left(\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)\right)=\left(F\underset{\dot{}}{·}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)$$
52	34 37 51	3eqtrd	$$⊢\phi \to \left(F{\cdot }_P\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=\left(F\underset{\dot{}}{·}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)$$
53	1 29 2 20 3 4 5 22 9 11	mplmon2	$$⊢\phi \to F{\cdot }_P\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X,F,\underset{\dot{}}{0}\right)\right)$$
54	1 29 2 20 3 4 5 22 10 12	mplmon2	$$⊢\phi \to G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=Y,G,\underset{\dot{}}{0}\right)\right)$$
55	53 54	oveq12d	$$⊢\phi \to \left(F{\cdot }_P\left(y\in D⟼if\left(y=X,1_R,\underset{\dot{}}{0}\right)\right)\right)\underset{\dot{}}{\bullet }\left(G{\cdot }_P\left(y\in D⟼if\left(y=Y,1_R,\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y=X,F,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,G,\underset{\dot{}}{0}\right)\right)$$
56	4 8	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\wedge G\in C\right)\to F\underset{\dot{}}{·}G\in C$$
57	22 11 12 56	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}G\in C$$
58	1 29 2 20 3 4 5 22 42 57	mplmon2	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right){\cdot }_P\left(y\in D⟼if\left(y=X{+}_{f}Y,1_R,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,F\underset{\dot{}}{·}G,\underset{\dot{}}{0}\right)\right)$$
59	52 55 58	3eqtr3d	$$⊢\phi \to \left(y\in D⟼if\left(y=X,F,\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{\bullet }\left(y\in D⟼if\left(y=Y,G,\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,F\underset{\dot{}}{·}G,\underset{\dot{}}{0}\right)\right)$$