Metamath Proof Explorer

Theorem cpmadugsumlemC

Description: Lemma C for cpmadugsum . (Contributed by AV, 2-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a 
|- A = ( N Mat R )
cpmadugsum.b 
|- B = ( Base ` A )
cpmadugsum.p 
|- P = ( Poly1 ` R )
cpmadugsum.y 
|- Y = ( N Mat P )
cpmadugsum.t 
|- T = ( N matToPolyMat R )
cpmadugsum.x 
|- X = ( var1 ` R )
cpmadugsum.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
cpmadugsum.m 
|- .x. = ( .s ` Y )
cpmadugsum.r 
|- .X. = ( .r ` Y )
cpmadugsum.1 
|- .1. = ( 1r ` Y )
Assertion cpmadugsumlemC 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a 
 |-  A = ( N Mat R )
2 cpmadugsum.b 
 |-  B = ( Base ` A )
3 cpmadugsum.p 
 |-  P = ( Poly1 ` R )
4 cpmadugsum.y 
 |-  Y = ( N Mat P )
5 cpmadugsum.t 
 |-  T = ( N matToPolyMat R )
6 cpmadugsum.x 
 |-  X = ( var1 ` R )
7 cpmadugsum.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
8 cpmadugsum.m 
 |-  .x. = ( .s ` Y )
9 cpmadugsum.r 
 |-  .X. = ( .r ` Y )
10 cpmadugsum.1 
 |-  .1. = ( 1r ` Y )
11 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
12 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 13 14 syl 
 |-  ( R e. CRing -> P e. Ring )
16 15 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. Ring ) )
17 4 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. Ring )
18 16 17 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
19 18 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
21 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... s ) e. _V )
22 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
23 13 22 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
24 23 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
25 16 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
26 4 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. LMod )
27 25 26 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
28 27 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. LMod )
29 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
30 eqid 
 |-  ( Base ` P ) = ( Base ` P )
31 29 30 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
32 15 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
33 29 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
34 32 33 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
35 34 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( mulGrp ` P ) e. Mnd )
36 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
37 36 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> i e. NN0 )
38 13 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
39 6 3 30 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
40 38 39 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
41 40 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> X e. ( Base ` P ) )
42 31 7 35 37 41 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
43 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
44 43 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
45 44 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
46 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
47 45 46 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
48 47 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
49 48 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
50 49 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
51 50 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
52 42 51 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
53 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> N e. Fin )
54 38 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> R e. Ring )
55 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> s e. NN0 )
56 simprr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
57 56 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) )
58 1 2 3 4 5 m2pmfzmap 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
59 53 54 55 57 58 syl31anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
60 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
61 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
62 11 60 8 61 lmodvscl 
 |-  ( ( Y e. LMod /\ ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
63 28 52 59 62 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
64 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
65 38 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
66 simprl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
67 eqid 
 |-  ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
68 fzfid 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0 ... s ) e. Fin )
69 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. _V )
70 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` Y ) e. _V )
71 67 68 69 70 fsuppmptdm 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) finSupp ( 0g ` Y ) )
72 64 65 66 56 71 syl31anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) finSupp ( 0g ` Y ) )
73 11 12 9 20 21 24 63 72 gsummulc2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( T ` M ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
74 4 matassa 
 |-  ( ( N e. Fin /\ P e. CRing ) -> Y e. AssAlg )
75 44 74 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. AssAlg )
76 75 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. AssAlg )
77 76 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. AssAlg )
78 15 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Ring )
79 78 33 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( mulGrp ` P ) e. Mnd )
80 79 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
81 80 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( mulGrp ` P ) e. Mnd )
82 31 7 81 37 41 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
83 49 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
84 82 83 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
85 23 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
86 11 60 61 8 9 assaassr 
 |-  ( ( Y e. AssAlg /\ ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) ) -> ( ( T ` M ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
87 77 84 85 59 86 syl13anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( T ` M ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
88 87 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( T ` M ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
89 88 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( T ` M ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
90 73 89 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )