pmatcollpw3fi1lem1

Description: Lemma 1 for pmatcollpw3fi1 . (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw.c	$⊢ C = N Mat P$
	pmatcollpw.b	$⊢ B = {Base}_{C}$
	pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
	pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw.x	$⊢ X = {var}_{1} (R)$
	pmatcollpw.t	$⊢ T = N matToPolyMat R$
	pmatcollpw3.a	$⊢ A = N Mat R$
	pmatcollpw3.d	$⊢ D = {Base}_{A}$
	pmatcollpw3fi1lem1.0	$⊢ \underset{˙}{0} = 0_{A}$
	pmatcollpw3fi1lem1.h	$⊢ H = (l \in (0 \dots 1) ⟼ if (l = 0, G (0), \underset{˙}{0}))$
Assertion	pmatcollpw3fi1lem1	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}}) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = {\sum_{C}}_{n = 0}^{1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw.c	$⊢ C = N Mat P$
3		pmatcollpw.b	$⊢ B = {Base}_{C}$
4		pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
5		pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw.x	$⊢ X = {var}_{1} (R)$
7		pmatcollpw.t	$⊢ T = N matToPolyMat R$
8		pmatcollpw3.a	$⊢ A = N Mat R$
9		pmatcollpw3.d	$⊢ D = {Base}_{A}$
10		pmatcollpw3fi1lem1.0	$⊢ \underset{˙}{0} = 0_{A}$
11		pmatcollpw3fi1lem1.h	$⊢ H = (l \in (0 \dots 1) ⟼ if (l = 0, G (0), \underset{˙}{0}))$
12		simpr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))$
13	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
14		ringmnd	$⊢ C \in Ring \to C \in Mnd$
15	13 14	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in Mnd$
16	15	adantr	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to C \in Mnd$
17		ringcmn	$⊢ C \in Ring \to C \in CMnd$
18	13 17	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in CMnd$
19	18	adantr	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to C \in CMnd$
20		snfi	$⊢ \{0\} \in Fin$
21	20	a1i	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \{0\} \in Fin$
22		simplll	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to N \in Fin$
23		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to R \in Ring$
24		elmapi	$⊢ G \in (D^{\{0\}}) \to G : \{0\} ⟶ D$
25	24	adantl	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to G : \{0\} ⟶ D$
26	25	ffvelrnda	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to G (n) \in D$
27		elsni	$⊢ n \in \{0\} \to n = 0$
28		0nn0	$⊢ 0 \in ℕ_{0}$
29	27 28	eqeltrdi	$⊢ n \in \{0\} \to n \in ℕ_{0}$
30	29	adantl	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to n \in ℕ_{0}$
31	8 9 7 1 2 3 4 5 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (G (n) \in D \land n \in ℕ_{0})) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (G (n)) \in B$
32	22 23 26 30 31	syl22anc	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (G (n)) \in B$
33	32	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \forall n \in \{0\} (n \underset{˙}{\times} X) \underset{˙}{*} T (G (n)) \in B$
34	3 19 21 33	gsummptcl	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (G (n))) \in B$
35		eqid	$⊢ +_{C} = +_{C}$
36		eqid	$⊢ 0_{C} = 0_{C}$
37	3 35 36	mndrid	$⊢ (C \in Mnd \land \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n))) \in B) \to (\underset{n \in \{0\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) +_{C} 0_{C} = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (G (n)))$
38	16 34 37	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to (\underset{n \in \{0\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) +_{C} 0_{C} = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))$
39		fz0sn	$⊢ (0 \dots 0) = \{0\}$
40	39	eqcomi	$⊢ \{0\} = (0 \dots 0)$
41	40	a1i	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \{0\} = (0 \dots 0)$
42		simpr	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to l = n$
43	27	ad2antlr	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to n = 0$
44	42 43	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to l = 0$
45	44	iftrued	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to if (l = 0, G (0), \underset{˙}{0}) = G (0)$
46		fveq2	$⊢ n = 0 \to G (n) = G (0)$
47	46	eqcomd	$⊢ n = 0 \to G (0) = G (n)$
48	27 47	syl	$⊢ n \in \{0\} \to G (0) = G (n)$
49	48	ad2antlr	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to G (0) = G (n)$
50	45 49	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \land l = n) \to if (l = 0, G (0), \underset{˙}{0}) = G (n)$
51		1nn0	$⊢ 1 \in ℕ_{0}$
52	51	a1i	$⊢ n = 0 \to 1 \in ℕ_{0}$
53		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
54	52 53	eleqtrdi	$⊢ n = 0 \to 1 \in ℤ_{\geq 0}$
55		eluzfz1	$⊢ 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots 1)$
56	54 55	syl	$⊢ n = 0 \to 0 \in (0 \dots 1)$
57		eleq1	$⊢ n = 0 \to (n \in (0 \dots 1) \leftrightarrow 0 \in (0 \dots 1))$
58	56 57	mpbird	$⊢ n = 0 \to n \in (0 \dots 1)$
59	27 58	syl	$⊢ n \in \{0\} \to n \in (0 \dots 1)$
60	59	adantl	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to n \in (0 \dots 1)$
61		ffvelrn	$⊢ (G : \{0\} ⟶ D \land n \in \{0\}) \to G (n) \in D$
62	61	ex	$⊢ G : \{0\} ⟶ D \to (n \in \{0\} \to G (n) \in D)$
63	24 62	syl	$⊢ G \in (D^{\{0\}}) \to (n \in \{0\} \to G (n) \in D)$
64	63	adantl	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to (n \in \{0\} \to G (n) \in D)$
65	64	imp	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to G (n) \in D$
66	11 50 60 65	fvmptd2	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to H (n) = G (n)$
67	66	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to G (n) = H (n)$
68	67	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to T (G (n)) = T (H (n))$
69	68	oveq2d	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in \{0\}) \to (n \underset{˙}{\times} X) \underset{˙}{} T (G (n)) = (n \underset{˙}{\times} X) \underset{˙}{} T (H (n))$
70	41 69	mpteq12dva	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to (n \in \{0\} ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (G (n))) = (n \in (0 \dots 0) ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$
71	70	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n))) = {\sum_{C}}_{n = 0}^{0} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$
72		ovexd	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to 0 + 1 \in V$
73	3 36	mndidcl	$⊢ C \in Mnd \to 0_{C} \in B$
74	15 73	syl	$⊢ (N \in Fin \land R \in Ring) \to 0_{C} \in B$
75	74	adantr	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to 0_{C} \in B$
76		0p1e1	$⊢ 0 + 1 = 1$
77	76	eqeq2i	$⊢ n = 0 + 1 \leftrightarrow n = 1$
78		ax-1ne0	$⊢ 1 \neq 0$
79	78	neii	$⊢ \neg 1 = 0$
80		eqeq1	$⊢ n = 1 \to (n = 0 \leftrightarrow 1 = 0)$
81	79 80	mtbiri	$⊢ n = 1 \to \neg n = 0$
82	77 81	sylbi	$⊢ n = 0 + 1 \to \neg n = 0$
83	82	ad2antlr	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \land l = n) \to \neg n = 0$
84		eqeq1	$⊢ l = n \to (l = 0 \leftrightarrow n = 0)$
85	84	notbid	$⊢ l = n \to (\neg l = 0 \leftrightarrow \neg n = 0)$
86	85	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \land l = n) \to (\neg l = 0 \leftrightarrow \neg n = 0)$
87	83 86	mpbird	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \land l = n) \to \neg l = 0$
88	87	iffalsed	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \land l = n) \to if (l = 0, G (0), \underset{˙}{0}) = \underset{˙}{0}$
89	88 10	eqtrdi	$⊢ ((((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \land l = n) \to if (l = 0, G (0), \underset{˙}{0}) = 0_{A}$
90	51	a1i	$⊢ n = 1 \to 1 \in ℕ_{0}$
91	90 53	eleqtrdi	$⊢ n = 1 \to 1 \in ℤ_{\geq 0}$
92		eluzfz2	$⊢ 1 \in ℤ_{\geq 0} \to 1 \in (0 \dots 1)$
93	91 92	syl	$⊢ n = 1 \to 1 \in (0 \dots 1)$
94		eleq1	$⊢ n = 1 \to (n \in (0 \dots 1) \leftrightarrow 1 \in (0 \dots 1))$
95	93 94	mpbird	$⊢ n = 1 \to n \in (0 \dots 1)$
96	77 95	sylbi	$⊢ n = 0 + 1 \to n \in (0 \dots 1)$
97	96	adantl	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to n \in (0 \dots 1)$
98		fvexd	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to 0_{A} \in V$
99	11 89 97 98	fvmptd2	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to H (n) = 0_{A}$
100	99	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to T (H (n)) = T (0_{A})$
101	8	fveq2i	$⊢ 0_{A} = 0_{(N Mat R)}$
102	2	fveq2i	$⊢ 0_{C} = 0_{(N Mat P)}$
103	7 1 101 102	0mat2pmat	$⊢ (R \in Ring \land N \in Fin) \to T (0_{A}) = 0_{C}$
104	103	ancoms	$⊢ (N \in Fin \land R \in Ring) \to T (0_{A}) = 0_{C}$
105	104	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to T (0_{A}) = 0_{C}$
106	100 105	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to T (H (n)) = 0_{C}$
107	106	oveq2d	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to (n \underset{˙}{\times} X) \underset{˙}{} T (H (n)) = (n \underset{˙}{\times} X) \underset{˙}{} 0_{C}$
108	1 2	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to C \in LMod$
109	108	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to C \in LMod$
110		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to R \in Ring$
111		eleq1	$⊢ n = 1 \to (n \in ℕ_{0} \leftrightarrow 1 \in ℕ_{0})$
112	90 111	mpbird	$⊢ n = 1 \to n \in ℕ_{0}$
113	77 112	sylbi	$⊢ n = 0 + 1 \to n \in ℕ_{0}$
114	113	adantl	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to n \in ℕ_{0}$
115		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
116		eqid	$⊢ {Base}_{P} = {Base}_{P}$
117	1 6 115 5 116	ply1moncl	$⊢ (R \in Ring \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
118	110 114 117	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to n \underset{˙}{\times} X \in {Base}_{P}$
119	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
120	2	matsca2	$⊢ (N \in Fin \land P \in Ring) \to P = Scalar (C)$
121	119 120	sylan2	$⊢ (N \in Fin \land R \in Ring) \to P = Scalar (C)$
122	121	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to Scalar (C) = P$
123	122	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (C)} = {Base}_{P}$
124	123	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (n \underset{˙}{\times} X \in {Base}_{Scalar (C)} \leftrightarrow n \underset{˙}{\times} X \in {Base}_{P})$
125	124	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to (n \underset{˙}{\times} X \in {Base}_{Scalar (C)} \leftrightarrow n \underset{˙}{\times} X \in {Base}_{P})$
126	118 125	mpbird	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to n \underset{˙}{\times} X \in {Base}_{Scalar (C)}$
127		eqid	$⊢ Scalar (C) = Scalar (C)$
128		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
129	127 4 128 36	lmodvs0	$⊢ (C \in LMod \land n \underset{˙}{\times} X \in {Base}_{Scalar (C)}) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{C} = 0_{C}$
130	109 126 129	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to (n \underset{˙}{\times} X) \underset{˙}{*} 0_{C} = 0_{C}$
131	107 130	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n = 0 + 1) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (H (n)) = 0_{C}$
132	3 16 72 75 131	gsumsnd	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \underset{n \in \{0 + 1\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))) = 0_{C}$
133	132	eqcomd	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to 0_{C} = \underset{n \in \{0 + 1\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n)))$
134	71 133	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to (\underset{n \in \{0\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) +_{C} 0_{C} = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))))$
135	38 134	eqtr3d	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n))) = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))))$
136	135	adantr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n))) = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n))))$
137	12 136	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))))$
138	137	3impa	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}}) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))))$
139	28	a1i	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to 0 \in ℕ_{0}$
140		simplll	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in (0 \dots 0 + 1)) \to N \in Fin$
141		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in (0 \dots 0 + 1)) \to R \in Ring$
142		id	$⊢ G : \{0\} ⟶ D \to G : \{0\} ⟶ D$
143		c0ex	$⊢ 0 \in V$
144	143	snid	$⊢ 0 \in \{0\}$
145	144	a1i	$⊢ G : \{0\} ⟶ D \to 0 \in \{0\}$
146	142 145	ffvelrnd	$⊢ G : \{0\} ⟶ D \to G (0) \in D$
147	24 146	syl	$⊢ G \in (D^{\{0\}}) \to G (0) \in D$
148	147	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land l \in (0 \dots 1)) \to G (0) \in D$
149	8	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
150	9 10	ring0cl	$⊢ A \in Ring \to \underset{˙}{0} \in D$
151	149 150	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} \in D$
152	151	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land l \in (0 \dots 1)) \to \underset{˙}{0} \in D$
153	148 152	ifcld	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land l \in (0 \dots 1)) \to if (l = 0, G (0), \underset{˙}{0}) \in D$
154	153 11	fmptd	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to H : (0 \dots 1) ⟶ D$
155	76	oveq2i	$⊢ (0 \dots 0 + 1) = (0 \dots 1)$
156	155	feq2i	$⊢ H : (0 \dots 0 + 1) ⟶ D \leftrightarrow H : (0 \dots 1) ⟶ D$
157	154 156	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to H : (0 \dots 0 + 1) ⟶ D$
158	157	ffvelrnda	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in (0 \dots 0 + 1)) \to H (n) \in D$
159		elfznn0	$⊢ n \in (0 \dots 0 + 1) \to n \in ℕ_{0}$
160	159	adantl	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in (0 \dots 0 + 1)) \to n \in ℕ_{0}$
161	8 9 7 1 2 3 4 5 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (H (n) \in D \land n \in ℕ_{0})) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (H (n)) \in B$
162	140 141 158 160 161	syl22anc	$⊢ (((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \land n \in (0 \dots 0 + 1)) \to (n \underset{˙}{\times} X) \underset{˙}{*} T (H (n)) \in B$
163	3 35 19 139 162	gsummptfzsplit	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}})) \to {\sum_{C}}_{n = 0}^{0 + 1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n))) = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{*} T (H (n))))$
164	163	3adant3	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}}) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to {\sum_{C}}_{n = 0}^{0 + 1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n))) = ({\sum_{C}}_{n = 0}^{0}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))) +_{C} (\underset{n \in \{0 + 1\}}{\sum_{C}}, ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n))))$
165	138 164	eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}}) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = {\sum_{C}}_{n = 0}^{0 + 1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$
166	155	mpteq1i	$⊢ (n \in (0 \dots 0 + 1) ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (H (n))) = (n \in (0 \dots 1) ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$
167	166	oveq2i	$⊢ {\sum_{C}}_{n = 0}^{0 + 1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n))) = {\sum_{C}}_{n = 0}^{1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$
168	165 167	eqtrdi	$⊢ ((N \in Fin \land R \in Ring) \land G \in (D^{\{0\}}) \land M = \underset{n \in \{0\}}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (G (n)))) \to M = {\sum_{C}}_{n = 0}^{1} ((n \underset{˙}{\times} X) \underset{˙}{} T (H (n)))$

Metamath Proof Explorer

Theorem pmatcollpw3fi1lem1

Proof