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 𝐴 = ( 𝑁 Mat 𝑅 )
m2pmfzmap.b 𝐵 = ( Base ‘ 𝐴 )
m2pmfzmap.p 𝑃 = ( Poly1𝑅 )
m2pmfzmap.y 𝑌 = ( 𝑁 Mat 𝑃 )
m2pmfzmap.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
m2pmfzmapfsupp.x 𝑋 = ( var1𝑅 )
m2pmfzmapfsupp.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
m2pmfzgsumcl.m · = ( ·𝑠𝑌 )
Assertion m2pmfzgsumcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 m2pmfzmap.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 m2pmfzmap.b 𝐵 = ( Base ‘ 𝐴 )
3 m2pmfzmap.p 𝑃 = ( Poly1𝑅 )
4 m2pmfzmap.y 𝑌 = ( 𝑁 Mat 𝑃 )
5 m2pmfzmap.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 m2pmfzmapfsupp.x 𝑋 = ( var1𝑅 )
7 m2pmfzmapfsupp.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8 m2pmfzgsumcl.m · = ( ·𝑠𝑌 )
9 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
10 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
11 3 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12 10 11 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
13 4 matring ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝑌 ∈ Ring )
14 12 13 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
15 ringcmn ( 𝑌 ∈ Ring → 𝑌 ∈ CMnd )
16 14 15 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ CMnd )
17 16 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ CMnd )
18 17 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ CMnd )
19 fzfid ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... 𝑠 ) ∈ Fin )
20 simpll1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑁 ∈ Fin )
21 12 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑃 ∈ Ring )
22 21 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑃 ∈ Ring )
23 10 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑅 ∈ Ring )
24 23 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
25 elfznn0 ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
26 eqid ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
27 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
28 3 6 26 7 27 ply1moncl ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
29 24 25 28 syl2an ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
30 10 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
31 30 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
32 simpl ( ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
33 31 32 anim12i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
34 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
35 33 34 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
36 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) )
37 36 anim1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
38 1 2 3 4 5 m2pmfzmap ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
39 35 37 38 syl2an2r ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
40 27 4 9 8 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑖 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ ( 𝑏𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
41 20 22 29 39 40 syl22anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
42 41 ralrimiva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑠 ) ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
43 9 18 19 42 gsummptcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ0𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 𝑋 ) · ( 𝑇 ‘ ( 𝑏𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )