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 ‘ 𝑌 ) )