ply1mulgsumlem2

	Ref	Expression
Hypotheses	ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
	ply1mulgsum.b	$⊢ B = {Base}_{P}$
	ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
	ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
	ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
	ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
	ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
	ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
	ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
Assertion	ply1mulgsumlem2	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
2		ply1mulgsum.b	$⊢ B = {Base}_{P}$
3		ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
4		ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
5		ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
6		ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
7		ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
8		ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
9		ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
10		ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
11	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem1	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists z \in ℕ_{0} \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))$
12		2nn0	$⊢ 2 \in ℕ_{0}$
13	12	a1i	$⊢ z \in ℕ_{0} \to 2 \in ℕ_{0}$
14		id	$⊢ z \in ℕ_{0} \to z \in ℕ_{0}$
15	13 14	nn0mulcld	$⊢ z \in ℕ_{0} \to 2 z \in ℕ_{0}$
16	15	ad2antrr	$⊢ ((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \to 2 z \in ℕ_{0}$
17		breq1	$⊢ s = 2 z \to (s < n \leftrightarrow 2 z < n)$
18	17	imbi1d	$⊢ s = 2 z \to ((s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \leftrightarrow (2 z < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}))$
19	18	ralbidv	$⊢ s = 2 z \to (\forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \leftrightarrow \forall n \in ℕ_{0} (2 z < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}))$
20	19	adantl	$⊢ (((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land s = 2 z) \to (\forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \leftrightarrow \forall n \in ℕ_{0} (2 z < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}))$
21		2re	$⊢ 2 \in ℝ$
22	21	a1i	$⊢ z \in ℕ_{0} \to 2 \in ℝ$
23		nn0re	$⊢ z \in ℕ_{0} \to z \in ℝ$
24	22 23	remulcld	$⊢ z \in ℕ_{0} \to 2 z \in ℝ$
25	24	ad2antrr	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to 2 z \in ℝ$
26		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
27	26	adantl	$⊢ (z \in ℕ_{0} \land n \in ℕ_{0}) \to n \in ℝ$
28	27	adantr	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to n \in ℝ$
29		elfznn0	$⊢ l \in (0 \dots n) \to l \in ℕ_{0}$
30		nn0re	$⊢ l \in ℕ_{0} \to l \in ℝ$
31	29 30	syl	$⊢ l \in (0 \dots n) \to l \in ℝ$
32	31	adantl	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to l \in ℝ$
33	25 28 32	ltsub1d	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (2 z < n \leftrightarrow 2 z - l < n - l)$
34	23	ad2antrr	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to z \in ℝ$
35	32 34 25	lesub2d	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (l \leq z \leftrightarrow 2 z - z \leq 2 z - l)$
36	35	adantr	$⊢ (((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land 2 z - l < n - l) \to (l \leq z \leftrightarrow 2 z - z \leq 2 z - l)$
37	24 23	resubcld	$⊢ z \in ℕ_{0} \to 2 z - z \in ℝ$
38	37	ad2antrr	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to 2 z - z \in ℝ$
39	24	adantr	$⊢ (z \in ℕ_{0} \land n \in ℕ_{0}) \to 2 z \in ℝ$
40		resubcl	$⊢ (2 z \in ℝ \land l \in ℝ) \to 2 z - l \in ℝ$
41	39 31 40	syl2an	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to 2 z - l \in ℝ$
42		resubcl	$⊢ (n \in ℝ \land l \in ℝ) \to n - l \in ℝ$
43	27 31 42	syl2an	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to n - l \in ℝ$
44		lelttr	$⊢ (2 z - z \in ℝ \land 2 z - l \in ℝ \land n - l \in ℝ) \to ((2 z - z \leq 2 z - l \land 2 z - l < n - l) \to 2 z - z < n - l)$
45	38 41 43 44	syl3anc	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to ((2 z - z \leq 2 z - l \land 2 z - l < n - l) \to 2 z - z < n - l)$
46		nn0cn	$⊢ z \in ℕ_{0} \to z \in ℂ$
47		2txmxeqx	$⊢ z \in ℂ \to 2 z - z = z$
48	46 47	syl	$⊢ z \in ℕ_{0} \to 2 z - z = z$
49	48	ad2antrr	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to 2 z - z = z$
50	49	breq1d	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (2 z - z < n - l \leftrightarrow z < n - l)$
51	45 50	sylibd	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to ((2 z - z \leq 2 z - l \land 2 z - l < n - l) \to z < n - l)$
52	51	expcomd	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (2 z - l < n - l \to (2 z - z \leq 2 z - l \to z < n - l))$
53	52	imp	$⊢ (((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land 2 z - l < n - l) \to (2 z - z \leq 2 z - l \to z < n - l)$
54	36 53	sylbid	$⊢ (((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land 2 z - l < n - l) \to (l \leq z \to z < n - l)$
55	54	ex	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (2 z - l < n - l \to (l \leq z \to z < n - l))$
56	33 55	sylbid	$⊢ ((z \in ℕ_{0} \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (2 z < n \to (l \leq z \to z < n - l))$
57	56	ex	$⊢ (z \in ℕ_{0} \land n \in ℕ_{0}) \to (l \in (0 \dots n) \to (2 z < n \to (l \leq z \to z < n - l)))$
58	57	com23	$⊢ (z \in ℕ_{0} \land n \in ℕ_{0}) \to (2 z < n \to (l \in (0 \dots n) \to (l \leq z \to z < n - l)))$
59	58	ex	$⊢ z \in ℕ_{0} \to (n \in ℕ_{0} \to (2 z < n \to (l \in (0 \dots n) \to (l \leq z \to z < n - l))))$
60	59	ad2antrr	$⊢ ((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \to (n \in ℕ_{0} \to (2 z < n \to (l \in (0 \dots n) \to (l \leq z \to z < n - l))))$
61	60	imp41	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (l \leq z \to z < n - l)$
62	61	impcom	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to z < n - l$
63		fznn0sub2	$⊢ l \in (0 \dots n) \to n - l \in (0 \dots n)$
64		elfznn0	$⊢ n - l \in (0 \dots n) \to n - l \in ℕ_{0}$
65		breq2	$⊢ x = n - l \to (z < x \leftrightarrow z < n - l)$
66		fveqeq2	$⊢ x = n - l \to (A (x) = 0_{R} \leftrightarrow A (n - l) = 0_{R})$
67		fveqeq2	$⊢ x = n - l \to (C (x) = 0_{R} \leftrightarrow C (n - l) = 0_{R})$
68	66 67	anbi12d	$⊢ x = n - l \to ((A (x) = 0_{R} \land C (x) = 0_{R}) \leftrightarrow (A (n - l) = 0_{R} \land C (n - l) = 0_{R}))$
69	65 68	imbi12d	$⊢ x = n - l \to ((z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \leftrightarrow (z < n - l \to (A (n - l) = 0_{R} \land C (n - l) = 0_{R})))$
70	69	rspcva	$⊢ (n - l \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \to (z < n - l \to (A (n - l) = 0_{R} \land C (n - l) = 0_{R}))$
71		simpr	$⊢ (A (n - l) = 0_{R} \land C (n - l) = 0_{R}) \to C (n - l) = 0_{R}$
72	70 71	syl6	$⊢ (n - l \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \to (z < n - l \to C (n - l) = 0_{R})$
73	72	ex	$⊢ n - l \in ℕ_{0} \to (\forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to (z < n - l \to C (n - l) = 0_{R}))$
74	63 64 73	3syl	$⊢ l \in (0 \dots n) \to (\forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to (z < n - l \to C (n - l) = 0_{R}))$
75	74	com12	$⊢ \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to (l \in (0 \dots n) \to (z < n - l \to C (n - l) = 0_{R}))$
76	75	ad4antlr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to (l \in (0 \dots n) \to (z < n - l \to C (n - l) = 0_{R}))$
77	76	imp	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (z < n - l \to C (n - l) = 0_{R})$
78	77	adantl	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to (z < n - l \to C (n - l) = 0_{R})$
79	62 78	mpd	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to C (n - l) = 0_{R}$
80	79	oveq2d	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \underset{˙}{} C (n - l) = A (l) \underset{˙}{} 0_{R}$
81		simplr1	$⊢ (((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to R \in Ring$
82	81	ad2antrr	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to R \in Ring$
83	82	adantl	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to R \in Ring$
84		simplr2	$⊢ (((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to K \in B$
85	84	adantr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to K \in B$
86	85 29	anim12i	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (K \in B \land l \in ℕ_{0})$
87	86	adantl	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to (K \in B \land l \in ℕ_{0})$
88		eqid	$⊢ {Base}_{R} = {Base}_{R}$
89	3 2 1 88	coe1fvalcl	$⊢ (K \in B \land l \in ℕ_{0}) \to A (l) \in {Base}_{R}$
90	87 89	syl	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \in {Base}_{R}$
91		eqid	$⊢ 0_{R} = 0_{R}$
92	88 8 91	ringrz	$⊢ (R \in Ring \land A (l) \in {Base}_{R}) \to A (l) \underset{˙}{*} 0_{R} = 0_{R}$
93	83 90 92	syl2anc	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \underset{˙}{*} 0_{R} = 0_{R}$
94	80 93	eqtrd	$⊢ (l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \underset{˙}{*} C (n - l) = 0_{R}$
95		ltnle	$⊢ (z \in ℝ \land l \in ℝ) \to (z < l \leftrightarrow \neg l \leq z)$
96	23 30 95	syl2an	$⊢ (z \in ℕ_{0} \land l \in ℕ_{0}) \to (z < l \leftrightarrow \neg l \leq z)$
97	96	bicomd	$⊢ (z \in ℕ_{0} \land l \in ℕ_{0}) \to (\neg l \leq z \leftrightarrow z < l)$
98	97	expcom	$⊢ l \in ℕ_{0} \to (z \in ℕ_{0} \to (\neg l \leq z \leftrightarrow z < l))$
99	98 29	syl11	$⊢ z \in ℕ_{0} \to (l \in (0 \dots n) \to (\neg l \leq z \leftrightarrow z < l))$
100	99	ad4antr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to (l \in (0 \dots n) \to (\neg l \leq z \leftrightarrow z < l))$
101	100	imp	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (\neg l \leq z \leftrightarrow z < l)$
102		breq2	$⊢ x = l \to (z < x \leftrightarrow z < l)$
103		fveqeq2	$⊢ x = l \to (A (x) = 0_{R} \leftrightarrow A (l) = 0_{R})$
104		fveqeq2	$⊢ x = l \to (C (x) = 0_{R} \leftrightarrow C (l) = 0_{R})$
105	103 104	anbi12d	$⊢ x = l \to ((A (x) = 0_{R} \land C (x) = 0_{R}) \leftrightarrow (A (l) = 0_{R} \land C (l) = 0_{R}))$
106	102 105	imbi12d	$⊢ x = l \to ((z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \leftrightarrow (z < l \to (A (l) = 0_{R} \land C (l) = 0_{R})))$
107	106	rspcva	$⊢ (l \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \to (z < l \to (A (l) = 0_{R} \land C (l) = 0_{R}))$
108		simpl	$⊢ (A (l) = 0_{R} \land C (l) = 0_{R}) \to A (l) = 0_{R}$
109	107 108	syl6	$⊢ (l \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \to (z < l \to A (l) = 0_{R})$
110	109	ex	$⊢ l \in ℕ_{0} \to (\forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to (z < l \to A (l) = 0_{R}))$
111	110 29	syl11	$⊢ \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to (l \in (0 \dots n) \to (z < l \to A (l) = 0_{R}))$
112	111	ad4antlr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to (l \in (0 \dots n) \to (z < l \to A (l) = 0_{R}))$
113	112	imp	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (z < l \to A (l) = 0_{R})$
114	101 113	sylbid	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (\neg l \leq z \to A (l) = 0_{R})$
115	114	impcom	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) = 0_{R}$
116	115	oveq1d	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \underset{˙}{} C (n - l) = 0_{R} \underset{˙}{} C (n - l)$
117	82	adantl	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to R \in Ring$
118		simplr3	$⊢ (((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to L \in B$
119	118	adantr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to L \in B$
120		fznn0sub	$⊢ l \in (0 \dots n) \to n - l \in ℕ_{0}$
121	119 120	anim12i	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to (L \in B \land n - l \in ℕ_{0})$
122	121	adantl	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to (L \in B \land n - l \in ℕ_{0})$
123	4 2 1 88	coe1fvalcl	$⊢ (L \in B \land n - l \in ℕ_{0}) \to C (n - l) \in {Base}_{R}$
124	122 123	syl	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to C (n - l) \in {Base}_{R}$
125	88 8 91	ringlz	$⊢ (R \in Ring \land C (n - l) \in {Base}_{R}) \to 0_{R} \underset{˙}{*} C (n - l) = 0_{R}$
126	117 124 125	syl2anc	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to 0_{R} \underset{˙}{*} C (n - l) = 0_{R}$
127	116 126	eqtrd	$⊢ (\neg l \leq z \land (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n))) \to A (l) \underset{˙}{*} C (n - l) = 0_{R}$
128	94 127	pm2.61ian	$⊢ (((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \land l \in (0 \dots n)) \to A (l) \underset{˙}{*} C (n - l) = 0_{R}$
129	128	mpteq2dva	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to (l \in (0 \dots n) ⟼ A (l) \underset{˙}{*} C (n - l)) = (l \in (0 \dots n) ⟼ 0_{R})$
130	129	oveq2d	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = {\sum_{R}}_{l = 0}^{n} 0_{R}$
131		ringmnd	$⊢ R \in Ring \to R \in Mnd$
132	131	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to R \in Mnd$
133		ovex	$⊢ (0 \dots n) \in V$
134	132 133	jctir	$⊢ (R \in Ring \land K \in B \land L \in B) \to (R \in Mnd \land (0 \dots n) \in V)$
135	134	ad3antlr	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to (R \in Mnd \land (0 \dots n) \in V)$
136	91	gsumz	$⊢ (R \in Mnd \land (0 \dots n) \in V) \to {\sum_{R}}_{l = 0}^{n} 0_{R} = 0_{R}$
137	135 136	syl	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to {\sum_{R}}_{l = 0}^{n} 0_{R} = 0_{R}$
138	130 137	eqtrd	$⊢ ((((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land 2 z < n) \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R}$
139	138	ex	$⊢ (((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (2 z < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$
140	139	ralrimiva	$⊢ ((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \to \forall n \in ℕ_{0} (2 z < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$
141	16 20 140	rspcedvd	$⊢ ((z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \land (R \in Ring \land K \in B \land L \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$
142	141	ex	$⊢ (z \in ℕ_{0} \land \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R}))) \to ((R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R}))$
143	142	rexlimiva	$⊢ \exists z \in ℕ_{0} \forall x \in ℕ_{0} (z < x \to (A (x) = 0_{R} \land C (x) = 0_{R})) \to ((R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R}))$
144	11 143	mpcom	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$

Metamath Proof Explorer

Theorem ply1mulgsumlem2

Proof