coe1tmmul2

Description: Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	coe1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
	coe1tm.k	$⊢ K = {Base}_{R}$
	coe1tm.p	$⊢ P = {Poly}_{1} (R)$
	coe1tm.x	$⊢ X = {var}_{1} (R)$
	coe1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	coe1tm.n	$⊢ N = {mulGrp}_{P}$
	coe1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
	coe1tmmul.b	$⊢ B = {Base}_{P}$
	coe1tmmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	coe1tmmul.u	$⊢ \underset{˙}{\times} = \cdot_{R}$
	coe1tmmul.a	$⊢ φ \to A \in B$
	coe1tmmul.r	$⊢ φ \to R \in Ring$
	coe1tmmul.c	$⊢ φ \to C \in K$
	coe1tmmul.d	$⊢ φ \to D \in ℕ_{0}$
Assertion	coe1tmmul2	$⊢ φ \to {coe}_{1} (A \underset{˙}{∙} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))) = (x \in ℕ_{0} ⟼ if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
2		coe1tm.k	$⊢ K = {Base}_{R}$
3		coe1tm.p	$⊢ P = {Poly}_{1} (R)$
4		coe1tm.x	$⊢ X = {var}_{1} (R)$
5		coe1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		coe1tm.n	$⊢ N = {mulGrp}_{P}$
7		coe1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
8		coe1tmmul.b	$⊢ B = {Base}_{P}$
9		coe1tmmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
10		coe1tmmul.u	$⊢ \underset{˙}{\times} = \cdot_{R}$
11		coe1tmmul.a	$⊢ φ \to A \in B$
12		coe1tmmul.r	$⊢ φ \to R \in Ring$
13		coe1tmmul.c	$⊢ φ \to C \in K$
14		coe1tmmul.d	$⊢ φ \to D \in ℕ_{0}$
15	2 3 4 5 6 7 8	ply1tmcl	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B$
16	12 13 14 15	syl3anc	$⊢ φ \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B$
17	3 9 10 8	coe1mul	$⊢ (R \in Ring \land A \in B \land C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B) \to {coe}_{1} (A \underset{˙}{∙} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)))$
18	12 11 16 17	syl3anc	$⊢ φ \to {coe}_{1} (A \underset{˙}{∙} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)))$
19		eqeq2	$⊢ {coe}_{1} (A) (x - D) \underset{˙}{\times} C = if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}) \to ({\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = {coe}_{1} (A) (x - D) \underset{˙}{\times} C \leftrightarrow {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}))$
20		eqeq2	$⊢ \underset{˙}{0} = if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}) \to ({\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = \underset{˙}{0} \leftrightarrow {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}))$
21	12	adantr	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to R \in Ring$
22		ringmnd	$⊢ R \in Ring \to R \in Mnd$
23	21 22	syl	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to R \in Mnd$
24		ovex	$⊢ (0 \dots x) \in V$
25	24	a1i	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (0 \dots x) \in V$
26		simprr	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to D \leq x$
27	14	adantr	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to D \in ℕ_{0}$
28		simprl	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x \in ℕ_{0}$
29		nn0sub	$⊢ (D \in ℕ_{0} \land x \in ℕ_{0}) \to (D \leq x \leftrightarrow x - D \in ℕ_{0})$
30	27 28 29	syl2anc	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (D \leq x \leftrightarrow x - D \in ℕ_{0})$
31	26 30	mpbid	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x - D \in ℕ_{0}$
32	27	nn0ge0d	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to 0 \leq D$
33		nn0re	$⊢ x \in ℕ_{0} \to x \in ℝ$
34	33	ad2antrl	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x \in ℝ$
35	14	nn0red	$⊢ φ \to D \in ℝ$
36	35	adantr	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to D \in ℝ$
37	34 36	subge02d	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (0 \leq D \leftrightarrow x - D \leq x)$
38	32 37	mpbid	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x - D \leq x$
39		fznn0	$⊢ x \in ℕ_{0} \to (x - D \in (0 \dots x) \leftrightarrow (x - D \in ℕ_{0} \land x - D \leq x))$
40	39	ad2antrl	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (x - D \in (0 \dots x) \leftrightarrow (x - D \in ℕ_{0} \land x - D \leq x))$
41	31 38 40	mpbir2and	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x - D \in (0 \dots x)$
42	12	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to R \in Ring$
43		eqid	$⊢ {coe}_{1} (A) = {coe}_{1} (A)$
44	43 8 3 2	coe1f	$⊢ A \in B \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
45	11 44	syl	$⊢ φ \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
46	45	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
47		elfznn0	$⊢ y \in (0 \dots x) \to y \in ℕ_{0}$
48	47	adantl	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to y \in ℕ_{0}$
49	46 48	ffvelrnd	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (A) (y) \in K$
50		eqid	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))$
51	50 8 3 2	coe1f	$⊢ C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K$
52	16 51	syl	$⊢ φ \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K$
53	52	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K$
54		fznn0sub	$⊢ y \in (0 \dots x) \to x - y \in ℕ_{0}$
55	54	adantl	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to x - y \in ℕ_{0}$
56	53 55	ffvelrnd	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) \in K$
57	2 10	ringcl	$⊢ (R \in Ring \land {coe}_{1} (A) (y) \in K \land {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) \in K) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) \in K$
58	42 49 56 57	syl3anc	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) \in K$
59	58	fmpttd	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) : (0 \dots x) ⟶ K$
60	12	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to R \in Ring$
61	13	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to C \in K$
62	14	ad2antrr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to D \in ℕ_{0}$
63		eldifi	$⊢ y \in ((0 \dots x) ∖ \{x - D\}) \to y \in (0 \dots x)$
64	63 54	syl	$⊢ y \in ((0 \dots x) ∖ \{x - D\}) \to x - y \in ℕ_{0}$
65	64	adantl	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to x - y \in ℕ_{0}$
66		eldifsn	$⊢ y \in ((0 \dots x) ∖ \{x - D\}) \leftrightarrow (y \in (0 \dots x) \land y \neq x - D)$
67		simplrl	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to x \in ℕ_{0}$
68	67	nn0cnd	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to x \in ℂ$
69	47	nn0cnd	$⊢ y \in (0 \dots x) \to y \in ℂ$
70	69	adantl	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to y \in ℂ$
71	68 70	nncand	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to x - (x - y) = y$
72	71	eqcomd	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to y = x - (x - y)$
73		oveq2	$⊢ D = x - y \to x - D = x - (x - y)$
74	73	eqeq2d	$⊢ D = x - y \to (y = x - D \leftrightarrow y = x - (x - y))$
75	72 74	syl5ibrcom	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to (D = x - y \to y = x - D)$
76	75	necon3d	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to (y \neq x - D \to D \neq x - y)$
77	76	impr	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land (y \in (0 \dots x) \land y \neq x - D)) \to D \neq x - y$
78	66 77	sylan2b	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to D \neq x - y$
79	1 2 3 4 5 6 7 60 61 62 65 78	coe1tmfv2	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = \underset{˙}{0}$
80	79	oveq2d	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0}$
81	2 10 1	ringrz	$⊢ (R \in Ring \land {coe}_{1} (A) (y) \in K) \to {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
82	42 49 81	syl2anc	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in (0 \dots x)) \to {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
83	63 82	sylan2	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
84	80 83	eqtrd	$⊢ ((φ \land (x \in ℕ_{0} \land D \leq x)) \land y \in ((0 \dots x) ∖ \{x - D\})) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = \underset{˙}{0}$
85	84 25	suppss2	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) supp \underset{˙}{0} \subseteq \{x - D\}$
86	2 1 23 25 41 59 85	gsumpt	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) (x - D)$
87		fveq2	$⊢ y = x - D \to {coe}_{1} (A) (y) = {coe}_{1} (A) (x - D)$
88		oveq2	$⊢ y = x - D \to x - y = x - (x - D)$
89	88	fveq2d	$⊢ y = x - D \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D))$
90	87 89	oveq12d	$⊢ y = x - D \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = {coe}_{1} (A) (x - D) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D))$
91		eqid	$⊢ (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y))$
92		ovex	$⊢ {coe}_{1} (A) (x - D) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D)) \in V$
93	90 91 92	fvmpt	$⊢ x - D \in (0 \dots x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) (x - D) = {coe}_{1} (A) (x - D) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D))$
94	41 93	syl	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) (x - D) = {coe}_{1} (A) (x - D) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D))$
95	28	nn0cnd	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x \in ℂ$
96	27	nn0cnd	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to D \in ℂ$
97	95 96	nncand	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to x - (x - D) = D$
98	97	fveq2d	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D)) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D)$
99	13	adantr	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to C \in K$
100	1 2 3 4 5 6 7	coe1tmfv1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) = C$
101	21 99 27 100	syl3anc	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) = C$
102	98 101	eqtrd	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D)) = C$
103	102	oveq2d	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {coe}_{1} (A) (x - D) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - (x - D)) = {coe}_{1} (A) (x - D) \underset{˙}{\times} C$
104	86 94 103	3eqtrd	$⊢ (φ \land (x \in ℕ_{0} \land D \leq x)) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = {coe}_{1} (A) (x - D) \underset{˙}{\times} C$
105	104	anassrs	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = {coe}_{1} (A) (x - D) \underset{˙}{\times} C$
106	12	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to R \in Ring$
107	13	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to C \in K$
108	14	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to D \in ℕ_{0}$
109	54	ad2antll	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x - y \in ℕ_{0}$
110	54	nn0red	$⊢ y \in (0 \dots x) \to x - y \in ℝ$
111	110	ad2antll	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x - y \in ℝ$
112	33	ad2antlr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x \in ℝ$
113	35	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to D \in ℝ$
114	47	ad2antll	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to y \in ℕ_{0}$
115	114	nn0ge0d	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to 0 \leq y$
116	47	nn0red	$⊢ y \in (0 \dots x) \to y \in ℝ$
117	116	ad2antll	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to y \in ℝ$
118	112 117	subge02d	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to (0 \leq y \leftrightarrow x - y \leq x)$
119	115 118	mpbid	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x - y \leq x$
120		simprl	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to \neg D \leq x$
121	112 113	ltnled	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to (x < D \leftrightarrow \neg D \leq x)$
122	120 121	mpbird	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x < D$
123	111 112 113 119 122	lelttrd	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to x - y < D$
124	111 123	gtned	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to D \neq x - y$
125	1 2 3 4 5 6 7 106 107 108 109 124	coe1tmfv2	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = \underset{˙}{0}$
126	125	oveq2d	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0}$
127	45	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
128	127 114	ffvelrnd	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (A) (y) \in K$
129	106 128 81	syl2anc	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (A) (y) \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
130	126 129	eqtrd	$⊢ ((φ \land x \in ℕ_{0}) \land (\neg D \leq x \land y \in (0 \dots x))) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = \underset{˙}{0}$
131	130	anassrs	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y) = \underset{˙}{0}$
132	131	mpteq2dva	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = (y \in (0 \dots x) ⟼ \underset{˙}{0})$
133	132	oveq2d	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = {\sum_{R}}_{y = 0}^{x} \underset{˙}{0}$
134	12 22	syl	$⊢ φ \to R \in Mnd$
135	1	gsumz	$⊢ (R \in Mnd \land (0 \dots x) \in V) \to {\sum_{R}}_{y = 0}^{x} \underset{˙}{0} = \underset{˙}{0}$
136	134 24 135	sylancl	$⊢ φ \to {\sum_{R}}_{y = 0}^{x} \underset{˙}{0} = \underset{˙}{0}$
137	136	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} \underset{˙}{0} = \underset{˙}{0}$
138	133 137	eqtrd	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = \underset{˙}{0}$
139	19 20 105 138	ifbothda	$⊢ (φ \land x \in ℕ_{0}) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y)) = if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0})$
140	139	mpteq2dva	$⊢ φ \to (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (A) (y) \underset{˙}{\times} {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (x - y))) = (x \in ℕ_{0} ⟼ if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}))$
141	18 140	eqtrd	$⊢ φ \to {coe}_{1} (A \underset{˙}{∙} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))) = (x \in ℕ_{0} ⟼ if (D \leq x, {coe}_{1} (A) (x - D) \underset{˙}{\times} C, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem coe1tmmul2

Proof