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 = {Poly}_{1} (R)$
	m2pmfzmap.y	$⊢ Y = N Mat P$
	m2pmfzmap.t	$⊢ T = N matToPolyMat R$
	m2pmfzmapfsupp.x	$⊢ X = {var}_{1} (R)$
	m2pmfzmapfsupp.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	m2pmfzgsumcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
Assertion	m2pmfzgsumcl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y}$

Proof

Step	Hyp	Ref	Expression
1		m2pmfzmap.a	$⊢ A = N Mat R$
2		m2pmfzmap.b	$⊢ B = {Base}_{A}$
3		m2pmfzmap.p	$⊢ P = {Poly}_{1} (R)$
4		m2pmfzmap.y	$⊢ Y = N Mat P$
5		m2pmfzmap.t	$⊢ T = N matToPolyMat R$
6		m2pmfzmapfsupp.x	$⊢ X = {var}_{1} (R)$
7		m2pmfzmapfsupp.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
8		m2pmfzgsumcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
10		crngring	$⊢ R \in CRing \to R \in Ring$
11	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
12	10 11	syl	$⊢ R \in CRing \to P \in Ring$
13	4	matring	$⊢ (N \in Fin \land P \in Ring) \to Y \in Ring$
14	12 13	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
15		ringcmn	$⊢ Y \in Ring \to Y \in CMnd$
16	14 15	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in CMnd$
17	16	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in CMnd$
18	17	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to Y \in CMnd$
19		fzfid	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (0 \dots s) \in Fin$
20		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to N \in Fin$
21	12	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
22	21	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to P \in Ring$
23	10	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
24	23	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to R \in Ring$
25		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
26		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
27		eqid	$⊢ {Base}_{P} = {Base}_{P}$
28	3 6 26 7 27	ply1moncl	$⊢ (R \in Ring \land i \in ℕ_{0}) \to i \underset{˙}{\times} X \in {Base}_{P}$
29	24 25 28	syl2an	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{P}$
30	10	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
31	30	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
32		simpl	$⊢ (s \in ℕ_{0} \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
33	31 32	anim12i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to ((N \in Fin \land R \in Ring) \land s \in ℕ_{0})$
34		df-3an	$⊢ (N \in Fin \land R \in Ring \land s \in ℕ_{0}) \leftrightarrow ((N \in Fin \land R \in Ring) \land s \in ℕ_{0})$
35	33 34	sylibr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
36		simprr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to b \in (B^{(0 \dots s)})$
37	36	anim1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))$
38	1 2 3 4 5	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))) \to T (b (i)) \in {Base}_{Y}$
39	35 37 38	syl2an2r	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (b (i)) \in {Base}_{Y}$
40	27 4 9 8	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (i \underset{˙}{\times} X \in {Base}_{P} \land T (b (i)) \in {Base}_{Y})) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
41	20 22 29 39 40	syl22anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
42	41	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to \forall i \in (0 \dots s) (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
43	9 18 19 42	gsummptcl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y}$

Metamath Proof Explorer

Theorem m2pmfzgsumcl

Proof