coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-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	coe1tmmul	$⊢ φ \to {coe}_{1} ((C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \underset{˙}{∙} A) = (x \in ℕ_{0} ⟼ if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \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 C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in B \land A \in B) \to {coe}_{1} ((C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \underset{˙}{∙} A) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)))$
18	12 16 11 17	syl3anc	$⊢ φ \to {coe}_{1} ((C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \underset{˙}{∙} A) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)))$
19		eqeq2	$⊢ C \underset{˙}{\times} {coe}_{1} (A) (x - D) = if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}) \to ({\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = C \underset{˙}{\times} {coe}_{1} (A) (x - D) \leftrightarrow {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}))$
20		eqeq2	$⊢ \underset{˙}{0} = if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}) \to ({\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = \underset{˙}{0} \leftrightarrow {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}))$
21	12	ad2antrr	$⊢ ((φ \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		ovexd	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (0 \dots x) \in V$
25	14	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to D \in ℕ_{0}$
26		simpr	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to D \leq x$
27		fznn0	$⊢ x \in ℕ_{0} \to (D \in (0 \dots x) \leftrightarrow (D \in ℕ_{0} \land D \leq x))$
28	27	ad2antlr	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (D \in (0 \dots x) \leftrightarrow (D \in ℕ_{0} \land D \leq x))$
29	25 26 28	mpbir2and	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to D \in (0 \dots x)$
30	12	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to R \in Ring$
31		eqid	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))$
32	31 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$
33	16 32	syl	$⊢ φ \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K$
34	33	adantr	$⊢ (φ \land x \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K$
35		elfznn0	$⊢ y \in (0 \dots x) \to y \in ℕ_{0}$
36		ffvelcdm	$⊢ ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) : ℕ_{0} ⟶ K \land y \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \in K$
37	34 35 36	syl2an	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \in K$
38		eqid	$⊢ {coe}_{1} (A) = {coe}_{1} (A)$
39	38 8 3 2	coe1f	$⊢ A \in B \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
40	11 39	syl	$⊢ φ \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
41	40	adantr	$⊢ (φ \land x \in ℕ_{0}) \to {coe}_{1} (A) : ℕ_{0} ⟶ K$
42		fznn0sub	$⊢ y \in (0 \dots x) \to x - y \in ℕ_{0}$
43		ffvelcdm	$⊢ ({coe}_{1} (A) : ℕ_{0} ⟶ K \land x - y \in ℕ_{0}) \to {coe}_{1} (A) (x - y) \in K$
44	41 42 43	syl2an	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to {coe}_{1} (A) (x - y) \in K$
45	2 10	ringcl	$⊢ (R \in Ring \land {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \in K \land {coe}_{1} (A) (x - y) \in K) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) \in K$
46	30 37 44 45	syl3anc	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) \in K$
47	46	fmpttd	$⊢ (φ \land x \in ℕ_{0}) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) : (0 \dots x) ⟶ K$
48	47	adantr	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) : (0 \dots x) ⟶ K$
49	12	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to R \in Ring$
50	13	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to C \in K$
51	14	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to D \in ℕ_{0}$
52		eldifi	$⊢ y \in ((0 \dots x) ∖ \{D\}) \to y \in (0 \dots x)$
53	52 35	syl	$⊢ y \in ((0 \dots x) ∖ \{D\}) \to y \in ℕ_{0}$
54	53	adantl	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to y \in ℕ_{0}$
55		eldifsni	$⊢ y \in ((0 \dots x) ∖ \{D\}) \to y \neq D$
56	55	necomd	$⊢ y \in ((0 \dots x) ∖ \{D\}) \to D \neq y$
57	56	adantl	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to D \neq y$
58	1 2 3 4 5 6 7 49 50 51 54 57	coe1tmfv2	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) = \underset{˙}{0}$
59	58	oveq1d	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y)$
60	2 10 1	ringlz	$⊢ (R \in Ring \land {coe}_{1} (A) (x - y) \in K) \to \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
61	30 44 60	syl2anc	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
62	52 61	sylan2	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ((0 \dots x) ∖ \{D\})) \to \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
63	62	adantlr	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
64	59 63	eqtrd	$⊢ (((φ \land x \in ℕ_{0}) \land D \leq x) \land y \in ((0 \dots x) ∖ \{D\})) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
65	64 24	suppss2	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) supp \underset{˙}{0} \subseteq \{D\}$
66	2 1 23 24 29 48 65	gsumpt	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) (D)$
67		fveq2	$⊢ y = D \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D)$
68		oveq2	$⊢ y = D \to x - y = x - D$
69	68	fveq2d	$⊢ y = D \to {coe}_{1} (A) (x - y) = {coe}_{1} (A) (x - D)$
70	67 69	oveq12d	$⊢ y = D \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) \underset{˙}{\times} {coe}_{1} (A) (x - D)$
71		eqid	$⊢ (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y))$
72		ovex	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) \underset{˙}{\times} {coe}_{1} (A) (x - D) \in V$
73	70 71 72	fvmpt	$⊢ D \in (0 \dots x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) (D) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) \underset{˙}{\times} {coe}_{1} (A) (x - D)$
74	29 73	syl	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) (D) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) \underset{˙}{\times} {coe}_{1} (A) (x - D)$
75	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$
76	12 13 14 75	syl3anc	$⊢ φ \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) = C$
77	76	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) = C$
78	77	oveq1d	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (D) \underset{˙}{\times} {coe}_{1} (A) (x - D) = C \underset{˙}{\times} {coe}_{1} (A) (x - D)$
79	74 78	eqtrd	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) (D) = C \underset{˙}{\times} {coe}_{1} (A) (x - D)$
80	66 79	eqtrd	$⊢ ((φ \land x \in ℕ_{0}) \land D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = C \underset{˙}{\times} {coe}_{1} (A) (x - D)$
81	12	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to R \in Ring$
82	13	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to C \in K$
83	14	ad3antrrr	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to D \in ℕ_{0}$
84	35	adantl	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to y \in ℕ_{0}$
85		elfzle2	$⊢ y \in (0 \dots x) \to y \leq x$
86	85	adantl	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to y \leq x$
87		breq1	$⊢ D = y \to (D \leq x \leftrightarrow y \leq x)$
88	86 87	syl5ibrcom	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to (D = y \to D \leq x)$
89	88	necon3bd	$⊢ ((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \to (\neg D \leq x \to D \neq y)$
90	89	imp	$⊢ (((φ \land x \in ℕ_{0}) \land y \in (0 \dots x)) \land \neg D \leq x) \to D \neq y$
91	90	an32s	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to D \neq y$
92	1 2 3 4 5 6 7 81 82 83 84 91	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)) (y) = \underset{˙}{0}$
93	92	oveq1d	$⊢ (((φ \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)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y)$
94	61	adantlr	$⊢ (((φ \land x \in ℕ_{0}) \land \neg D \leq x) \land y \in (0 \dots x)) \to \underset{˙}{0} \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
95	93 94	eqtrd	$⊢ (((φ \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)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y) = \underset{˙}{0}$
96	95	mpteq2dva	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to (y \in (0 \dots x) ⟼ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = (y \in (0 \dots x) ⟼ \underset{˙}{0})$
97	96	oveq2d	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = {\sum_{R}}_{y = 0}^{x} \underset{˙}{0}$
98	12 22	syl	$⊢ φ \to R \in Mnd$
99	98	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to R \in Mnd$
100		ovexd	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to (0 \dots x) \in V$
101	1	gsumz	$⊢ (R \in Mnd \land (0 \dots x) \in V) \to {\sum_{R}}_{y = 0}^{x} \underset{˙}{0} = \underset{˙}{0}$
102	99 100 101	syl2anc	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} \underset{˙}{0} = \underset{˙}{0}$
103	97 102	eqtrd	$⊢ ((φ \land x \in ℕ_{0}) \land \neg D \leq x) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = \underset{˙}{0}$
104	19 20 80 103	ifbothda	$⊢ (φ \land x \in ℕ_{0}) \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y)) = if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0})$
105	104	mpteq2dva	$⊢ φ \to (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) (y) \underset{˙}{\times} {coe}_{1} (A) (x - y))) = (x \in ℕ_{0} ⟼ if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}))$
106	18 105	eqtrd	$⊢ φ \to {coe}_{1} ((C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \underset{˙}{∙} A) = (x \in ℕ_{0} ⟼ if (D \leq x, C \underset{˙}{\times} {coe}_{1} (A) (x - D), \underset{˙}{0}))$

Metamath Proof Explorer

Theorem coe1tmmul

Proof