Metamath Proof Explorer


Theorem mplmon2mul

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

Ref Expression
Hypotheses mplmon2cl.p P=ImPolyR
mplmon2cl.d D=f0I|f-1Fin
mplmon2cl.z 0˙=0R
mplmon2cl.c C=BaseR
mplmon2cl.i φIW
mplmon2mul.r φRCRing
mplmon2mul.t ˙=P
mplmon2mul.u ·˙=R
mplmon2mul.x φXD
mplmon2mul.y φYD
mplmon2mul.f φFC
mplmon2mul.g φGC
Assertion mplmon2mul φyDify=XF0˙˙yDify=YG0˙=yDify=X+fYF·˙G0˙

Proof

Step Hyp Ref Expression
1 mplmon2cl.p P=ImPolyR
2 mplmon2cl.d D=f0I|f-1Fin
3 mplmon2cl.z 0˙=0R
4 mplmon2cl.c C=BaseR
5 mplmon2cl.i φIW
6 mplmon2mul.r φRCRing
7 mplmon2mul.t ˙=P
8 mplmon2mul.u ·˙=R
9 mplmon2mul.x φXD
10 mplmon2mul.y φYD
11 mplmon2mul.f φFC
12 mplmon2mul.g φGC
13 1 mplassa IWRCRingPAssAlg
14 5 6 13 syl2anc φPAssAlg
15 1 5 6 mplsca φR=ScalarP
16 15 fveq2d φBaseR=BaseScalarP
17 4 16 eqtrid φC=BaseScalarP
18 11 17 eleqtrd φFBaseScalarP
19 eqid BaseP=BaseP
20 eqid 1R=1R
21 crngring RCRingRRing
22 6 21 syl φRRing
23 1 19 3 20 2 5 22 9 mplmon φyDify=X1R0˙BaseP
24 assalmod PAssAlgPLMod
25 14 24 syl φPLMod
26 12 17 eleqtrd φGBaseScalarP
27 1 19 3 20 2 5 22 10 mplmon φyDify=Y1R0˙BaseP
28 eqid ScalarP=ScalarP
29 eqid P=P
30 eqid BaseScalarP=BaseScalarP
31 19 28 29 30 lmodvscl PLModGBaseScalarPyDify=Y1R0˙BasePGPyDify=Y1R0˙BaseP
32 25 26 27 31 syl3anc φGPyDify=Y1R0˙BaseP
33 19 28 30 29 7 assaass PAssAlgFBaseScalarPyDify=X1R0˙BasePGPyDify=Y1R0˙BasePFPyDify=X1R0˙˙GPyDify=Y1R0˙=FPyDify=X1R0˙˙GPyDify=Y1R0˙
34 14 18 23 32 33 syl13anc φFPyDify=X1R0˙˙GPyDify=Y1R0˙=FPyDify=X1R0˙˙GPyDify=Y1R0˙
35 19 28 30 29 7 assaassr PAssAlgGBaseScalarPyDify=X1R0˙BasePyDify=Y1R0˙BasePyDify=X1R0˙˙GPyDify=Y1R0˙=GPyDify=X1R0˙˙yDify=Y1R0˙
36 14 26 23 27 35 syl13anc φyDify=X1R0˙˙GPyDify=Y1R0˙=GPyDify=X1R0˙˙yDify=Y1R0˙
37 36 oveq2d φFPyDify=X1R0˙˙GPyDify=Y1R0˙=FPGPyDify=X1R0˙˙yDify=Y1R0˙
38 1 19 3 20 2 5 22 9 7 10 mplmonmul φyDify=X1R0˙˙yDify=Y1R0˙=yDify=X+fY1R0˙
39 38 oveq2d φGPyDify=X1R0˙˙yDify=Y1R0˙=GPyDify=X+fY1R0˙
40 39 oveq2d φFPGPyDify=X1R0˙˙yDify=Y1R0˙=FPGPyDify=X+fY1R0˙
41 2 psrbagaddcl XDYDX+fYD
42 9 10 41 syl2anc φX+fYD
43 1 19 3 20 2 5 22 42 mplmon φyDify=X+fY1R0˙BaseP
44 eqid ScalarP=ScalarP
45 19 28 29 30 44 lmodvsass PLModFBaseScalarPGBaseScalarPyDify=X+fY1R0˙BasePFScalarPGPyDify=X+fY1R0˙=FPGPyDify=X+fY1R0˙
46 25 18 26 43 45 syl13anc φFScalarPGPyDify=X+fY1R0˙=FPGPyDify=X+fY1R0˙
47 15 fveq2d φR=ScalarP
48 8 47 eqtr2id φScalarP=·˙
49 48 oveqd φFScalarPG=F·˙G
50 49 oveq1d φFScalarPGPyDify=X+fY1R0˙=F·˙GPyDify=X+fY1R0˙
51 40 46 50 3eqtr2d φFPGPyDify=X1R0˙˙yDify=Y1R0˙=F·˙GPyDify=X+fY1R0˙
52 34 37 51 3eqtrd φFPyDify=X1R0˙˙GPyDify=Y1R0˙=F·˙GPyDify=X+fY1R0˙
53 1 29 2 20 3 4 5 22 9 11 mplmon2 φFPyDify=X1R0˙=yDify=XF0˙
54 1 29 2 20 3 4 5 22 10 12 mplmon2 φGPyDify=Y1R0˙=yDify=YG0˙
55 53 54 oveq12d φFPyDify=X1R0˙˙GPyDify=Y1R0˙=yDify=XF0˙˙yDify=YG0˙
56 4 8 ringcl RRingFCGCF·˙GC
57 22 11 12 56 syl3anc φF·˙GC
58 1 29 2 20 3 4 5 22 42 57 mplmon2 φF·˙GPyDify=X+fY1R0˙=yDify=X+fYF·˙G0˙
59 52 55 58 3eqtr3d φyDify=XF0˙˙yDify=YG0˙=yDify=X+fYF·˙G0˙