Metamath Proof Explorer

Theorem m2pmfzgsumcl

Description: Closure of the sum of scaled transformed matrices. (Contributed by AV, 4-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 m2pmfzmap.a 
 |-  A = ( N Mat R )
2 m2pmfzmap.b 
 |-  B = ( Base ` A )
3 m2pmfzmap.p 
 |-  P = ( Poly1 ` R )
4 m2pmfzmap.y 
 |-  Y = ( N Mat P )
5 m2pmfzmap.t 
 |-  T = ( N matToPolyMat R )
6 m2pmfzmapfsupp.x 
 |-  X = ( var1 ` R )
7 m2pmfzmapfsupp.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
8 m2pmfzgsumcl.m 
 |-  .x. = ( .s ` Y )
9 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
10 crngring 
 |-  ( R e. CRing -> R e. Ring )
11 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 10 11 syl 
 |-  ( R e. CRing -> P e. Ring )
13 4 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. Ring )
14 12 13 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
15 ringcmn 
 |-  ( Y e. Ring -> Y e. CMnd )
16 14 15 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. CMnd )
17 16 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
18 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. CMnd )
19 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... s ) e. Fin )
20 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 )
21 12 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
22 21 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> P e. Ring )
23 10 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
24 23 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
25 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
26 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
27 eqid 
 |-  ( Base ` P ) = ( Base ` P )
28 3 6 26 7 27 ply1moncl 
 |-  ( ( R e. Ring /\ i e. NN0 ) -> ( i .^ X ) e. ( Base ` P ) )
29 24 25 28 syl2an 
 |-  ( ( ( ( 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 ) )
30 10 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
31 30 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
32 simpl 
 |-  ( ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
33 31 32 anim12i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ s e. NN0 ) )
34 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) <-> ( ( N e. Fin /\ R e. Ring ) /\ s e. NN0 ) )
35 33 34 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( N e. Fin /\ R e. Ring /\ s e. NN0 ) )
36 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 ) ) )
37 36 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 ) ) )
38 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 ) )
39 35 37 38 syl2an2r 
 |-  ( ( ( ( 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 ) )
40 27 4 9 8 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( i .^ X ) e. ( Base ` P ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
41 20 22 29 39 40 syl22anc 
 |-  ( ( ( ( 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 ) )
42 41 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 0 ... s ) ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
43 9 18 19 42 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )