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