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 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
14 crngring 
 |-  ( R e. CRing -> R e. Ring )
15 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
16 14 15 syl 
 |-  ( R e. CRing -> P e. Ring )
17 16 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. Ring ) )
18 4 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. Ring )
19 17 18 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
20 19 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
22 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... s ) e. _V )
23 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
24 14 23 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
25 24 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
26 17 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
27 4 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. LMod )
28 26 27 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
29 28 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 )
30 16 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
31 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
32 31 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
33 30 32 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
34 33 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 )
35 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
36 35 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 )
37 14 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
38 eqid 
 |-  ( Base ` P ) = ( Base ` P )
39 6 3 38 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
40 37 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 38 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
43 42 7 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ i e. NN0 /\ X e. ( Base ` P ) ) -> ( i .^ X ) e. ( Base ` P ) )
44 34 36 41 43 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 ) e. ( Base ` P ) )
45 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
46 45 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
47 46 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
48 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
49 47 48 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
50 49 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
51 50 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
52 51 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
53 52 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 ) ) )
54 44 53 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 ) ) )
55 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 )
56 37 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 )
57 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 )
58 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 ) ) )
59 58 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 ) ) )
60 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 ) )
61 55 56 57 59 60 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 ) )
62 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
63 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
64 11 62 8 63 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 ) )
65 29 54 61 64 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 ) )
66 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
67 37 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
68 simprl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
69 eqid 
 |-  ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
70 fzfid 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0 ... s ) e. Fin )
71 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 )
72 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` Y ) e. _V )
73 69 70 71 72 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 ) )
74 66 67 68 58 73 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 ) )
75 11 12 13 9 21 22 25 65 74 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 ) ) ) ) ) ) )
76 4 matassa 
 |-  ( ( N e. Fin /\ P e. CRing ) -> Y e. AssAlg )
77 46 76 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. AssAlg )
78 77 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. AssAlg )
79 78 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 )
80 16 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Ring )
81 80 32 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( mulGrp ` P ) e. Mnd )
82 81 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
83 82 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 )
84 83 36 41 43 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 ) e. ( Base ` P ) )
85 51 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 ) )
86 84 85 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 ) ) )
87 24 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 ) )
88 11 62 63 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 ) ) ) ) )
89 79 86 87 61 88 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 ) ) ) ) )
90 89 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 ) ) ) ) ) )
91 90 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 ) ) ) ) ) ) )
92 75 91 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 ) ) ) ) ) ) )