Metamath Proof Explorer

Theorem mplmon2mul

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

Ref Expression
Hypotheses mplmon2cl.p 
|- P = ( I mPoly R )
mplmon2cl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplmon2cl.z 
|- .0. = ( 0g ` R )
mplmon2cl.c 
|- C = ( Base ` R )
mplmon2cl.i 
|- ( ph -> I e. W )
mplmon2mul.r 
|- ( ph -> R e. CRing )
mplmon2mul.t 
|- .xb = ( .r ` P )
mplmon2mul.u 
|- .x. = ( .r ` R )
mplmon2mul.x 
|- ( ph -> X e. D )
mplmon2mul.y 
|- ( ph -> Y e. D )
mplmon2mul.f 
|- ( ph -> F e. C )
mplmon2mul.g 
|- ( ph -> G e. C )
Assertion mplmon2mul 
|- ( ph -> ( ( y e. D |-> if ( y = X , F , .0. ) ) .xb ( y e. D |-> if ( y = Y , G , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , ( F .x. G ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mplmon2cl.p 
 |-  P = ( I mPoly R )
2 mplmon2cl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplmon2cl.z 
 |-  .0. = ( 0g ` R )
4 mplmon2cl.c 
 |-  C = ( Base ` R )
5 mplmon2cl.i 
 |-  ( ph -> I e. W )
6 mplmon2mul.r 
 |-  ( ph -> R e. CRing )
7 mplmon2mul.t 
 |-  .xb = ( .r ` P )
8 mplmon2mul.u 
 |-  .x. = ( .r ` R )
9 mplmon2mul.x 
 |-  ( ph -> X e. D )
10 mplmon2mul.y 
 |-  ( ph -> Y e. D )
11 mplmon2mul.f 
 |-  ( ph -> F e. C )
12 mplmon2mul.g 
 |-  ( ph -> G e. C )
13 1 mplassa 
 |-  ( ( I e. W /\ R e. CRing ) -> P e. AssAlg )
14 5 6 13 syl2anc 
 |-  ( ph -> P e. AssAlg )
15 1 5 6 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
16 15 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
17 4 16 syl5eq 
 |-  ( ph -> C = ( Base ` ( Scalar ` P ) ) )
18 11 17 eleqtrd 
 |-  ( ph -> F e. ( Base ` ( Scalar ` P ) ) )
19 eqid 
 |-  ( Base ` P ) = ( Base ` P )
20 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 6 21 syl 
 |-  ( ph -> R e. Ring )
23 1 19 3 20 2 5 22 9 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) )
24 assalmod 
 |-  ( P e. AssAlg -> P e. LMod )
25 14 24 syl 
 |-  ( ph -> P e. LMod )
26 12 17 eleqtrd 
 |-  ( ph -> G e. ( Base ` ( Scalar ` P ) ) )
27 1 19 3 20 2 5 22 10 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) )
28 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
29 eqid 
 |-  ( .s ` P ) = ( .s ` P )
30 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
31 19 28 29 30 lmodvscl 
 |-  ( ( P e. LMod /\ G e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) ) -> ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) e. ( Base ` P ) )
32 25 26 27 31 syl3anc 
 |-  ( ph -> ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) e. ( Base ` P ) )
33 19 28 30 29 7 assaass 
 |-  ( ( P e. AssAlg /\ ( F e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) /\ ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) e. ( Base ` P ) ) ) -> ( ( F ( .s ` P ) ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( F ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) )
34 14 18 23 32 33 syl13anc 
 |-  ( ph -> ( ( F ( .s ` P ) ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( F ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) )
35 19 28 30 29 7 assaassr 
 |-  ( ( P e. AssAlg /\ ( G e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) /\ ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) ) ) -> ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) )
36 14 26 23 27 35 syl13anc 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) )
37 36 oveq2d 
 |-  ( ph -> ( F ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) = ( F ( .s ` P ) ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) )
38 1 19 3 20 2 5 22 9 7 10 mplmonmul 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) )
39 38 oveq2d 
 |-  ( ph -> ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( G ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) )
40 39 oveq2d 
 |-  ( ph -> ( F ( .s ` P ) ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) = ( F ( .s ` P ) ( G ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) ) )
41 2 psrbagaddcl 
 |-  ( ( X e. D /\ Y e. D ) -> ( X oF + Y ) e. D )
42 9 10 41 syl2anc 
 |-  ( ph -> ( X oF + Y ) e. D )
43 1 19 3 20 2 5 22 42 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) )
44 eqid 
 |-  ( .r ` ( Scalar ` P ) ) = ( .r ` ( Scalar ` P ) )
45 19 28 29 30 44 lmodvsass 
 |-  ( ( P e. LMod /\ ( F e. ( Base ` ( Scalar ` P ) ) /\ G e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) e. ( Base ` P ) ) ) -> ( ( F ( .r ` ( Scalar ` P ) ) G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) = ( F ( .s ` P ) ( G ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) ) )
46 25 18 26 43 45 syl13anc 
 |-  ( ph -> ( ( F ( .r ` ( Scalar ` P ) ) G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) = ( F ( .s ` P ) ( G ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) ) )
47 15 fveq2d 
 |-  ( ph -> ( .r ` R ) = ( .r ` ( Scalar ` P ) ) )
48 8 47 syl5req 
 |-  ( ph -> ( .r ` ( Scalar ` P ) ) = .x. )
49 48 oveqd 
 |-  ( ph -> ( F ( .r ` ( Scalar ` P ) ) G ) = ( F .x. G ) )
50 49 oveq1d 
 |-  ( ph -> ( ( F ( .r ` ( Scalar ` P ) ) G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) = ( ( F .x. G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) )
51 40 46 50 3eqtr2d 
 |-  ( ph -> ( F ( .s ` P ) ( G ( .s ` P ) ( ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) .xb ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) ) = ( ( F .x. G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) )
52 34 37 51 3eqtrd 
 |-  ( ph -> ( ( F ( .s ` P ) ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( ( F .x. G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) )
53 1 29 2 20 3 4 5 22 9 11 mplmon2 
 |-  ( ph -> ( F ( .s ` P ) ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = X , F , .0. ) ) )
54 1 29 2 20 3 4 5 22 10 12 mplmon2 
 |-  ( ph -> ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = Y , G , .0. ) ) )
55 53 54 oveq12d 
 |-  ( ph -> ( ( F ( .s ` P ) ( y e. D |-> if ( y = X , ( 1r ` R ) , .0. ) ) ) .xb ( G ( .s ` P ) ( y e. D |-> if ( y = Y , ( 1r ` R ) , .0. ) ) ) ) = ( ( y e. D |-> if ( y = X , F , .0. ) ) .xb ( y e. D |-> if ( y = Y , G , .0. ) ) ) )
56 4 8 ringcl 
 |-  ( ( R e. Ring /\ F e. C /\ G e. C ) -> ( F .x. G ) e. C )
57 22 11 12 56 syl3anc 
 |-  ( ph -> ( F .x. G ) e. C )
58 1 29 2 20 3 4 5 22 42 57 mplmon2 
 |-  ( ph -> ( ( F .x. G ) ( .s ` P ) ( y e. D |-> if ( y = ( X oF + Y ) , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , ( F .x. G ) , .0. ) ) )
59 52 55 58 3eqtr3d 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , F , .0. ) ) .xb ( y e. D |-> if ( y = Y , G , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , ( F .x. G ) , .0. ) ) )