coe1mul3

Description: The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1mul3.s	$⊢ Y = {Poly}_{1} (R)$
	coe1mul3.t	$⊢ \underset{˙}{∙} = \cdot_{Y}$
	coe1mul3.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	coe1mul3.b	$⊢ B = {Base}_{Y}$
	coe1mul3.d	$⊢ D = \deg_{1} (R)$
	coe1mul3.r	$⊢ φ \to R \in Ring$
	coe1mul3.f1	$⊢ φ \to F \in B$
	coe1mul3.f2	$⊢ φ \to I \in ℕ_{0}$
	coe1mul3.f3	$⊢ φ \to D (F) \leq I$
	coe1mul3.g1	$⊢ φ \to G \in B$
	coe1mul3.g2	$⊢ φ \to J \in ℕ_{0}$
	coe1mul3.g3	$⊢ φ \to D (G) \leq J$
Assertion	coe1mul3	$⊢ φ \to {coe}_{1} (F \underset{˙}{∙} G) (I + J) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (J)$

Proof

Step	Hyp	Ref	Expression
1		coe1mul3.s	$⊢ Y = {Poly}_{1} (R)$
2		coe1mul3.t	$⊢ \underset{˙}{∙} = \cdot_{Y}$
3		coe1mul3.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		coe1mul3.b	$⊢ B = {Base}_{Y}$
5		coe1mul3.d	$⊢ D = \deg_{1} (R)$
6		coe1mul3.r	$⊢ φ \to R \in Ring$
7		coe1mul3.f1	$⊢ φ \to F \in B$
8		coe1mul3.f2	$⊢ φ \to I \in ℕ_{0}$
9		coe1mul3.f3	$⊢ φ \to D (F) \leq I$
10		coe1mul3.g1	$⊢ φ \to G \in B$
11		coe1mul3.g2	$⊢ φ \to J \in ℕ_{0}$
12		coe1mul3.g3	$⊢ φ \to D (G) \leq J$
13	1 2 3 4	coe1mul	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{∙} G) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y)))$
14	6 7 10 13	syl3anc	$⊢ φ \to {coe}_{1} (F \underset{˙}{∙} G) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y)))$
15	14	fveq1d	$⊢ φ \to {coe}_{1} (F \underset{˙}{∙} G) (I + J) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y))) (I + J)$
16	8 11	nn0addcld	$⊢ φ \to I + J \in ℕ_{0}$
17		oveq2	$⊢ x = I + J \to (0 \dots x) = (0 \dots I + J)$
18		fvoveq1	$⊢ x = I + J \to {coe}_{1} (G) (x - y) = {coe}_{1} (G) (I + J - y)$
19	18	oveq2d	$⊢ x = I + J \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y) = {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)$
20	17 19	mpteq12dv	$⊢ x = I + J \to (y \in (0 \dots x) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y)) = (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y))$
21	20	oveq2d	$⊢ x = I + J \to {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y)) = {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y))$
22		eqid	$⊢ (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y))) = (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y)))$
23		ovex	$⊢ {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) \in V$
24	21 22 23	fvmpt	$⊢ I + J \in ℕ_{0} \to (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y))) (I + J) = {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y))$
25	16 24	syl	$⊢ φ \to (x \in ℕ_{0} ⟼ {\sum_{R}}_{y = 0}^{x} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (x - y))) (I + J) = {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y))$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27		eqid	$⊢ 0_{R} = 0_{R}$
28		ringmnd	$⊢ R \in Ring \to R \in Mnd$
29	6 28	syl	$⊢ φ \to R \in Mnd$
30		ovexd	$⊢ φ \to (0 \dots I + J) \in V$
31	8	nn0red	$⊢ φ \to I \in ℝ$
32		nn0addge1	$⊢ (I \in ℝ \land J \in ℕ_{0}) \to I \leq I + J$
33	31 11 32	syl2anc	$⊢ φ \to I \leq I + J$
34		fznn0	$⊢ I + J \in ℕ_{0} \to (I \in (0 \dots I + J) \leftrightarrow (I \in ℕ_{0} \land I \leq I + J))$
35	16 34	syl	$⊢ φ \to (I \in (0 \dots I + J) \leftrightarrow (I \in ℕ_{0} \land I \leq I + J))$
36	8 33 35	mpbir2and	$⊢ φ \to I \in (0 \dots I + J)$
37	6	adantr	$⊢ (φ \land y \in (0 \dots I + J)) \to R \in Ring$
38		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
39	38 4 1 26	coe1f	$⊢ F \in B \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
40	7 39	syl	$⊢ φ \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
41		elfznn0	$⊢ y \in (0 \dots I + J) \to y \in ℕ_{0}$
42		ffvelcdm	$⊢ ({coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R} \land y \in ℕ_{0}) \to {coe}_{1} (F) (y) \in {Base}_{R}$
43	40 41 42	syl2an	$⊢ (φ \land y \in (0 \dots I + J)) \to {coe}_{1} (F) (y) \in {Base}_{R}$
44		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
45	44 4 1 26	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
46	10 45	syl	$⊢ φ \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
47		fznn0sub	$⊢ y \in (0 \dots I + J) \to I + J - y \in ℕ_{0}$
48		ffvelcdm	$⊢ ({coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R} \land I + J - y \in ℕ_{0}) \to {coe}_{1} (G) (I + J - y) \in {Base}_{R}$
49	46 47 48	syl2an	$⊢ (φ \land y \in (0 \dots I + J)) \to {coe}_{1} (G) (I + J - y) \in {Base}_{R}$
50	26 3	ringcl	$⊢ (R \in Ring \land {coe}_{1} (F) (y) \in {Base}_{R} \land {coe}_{1} (G) (I + J - y) \in {Base}_{R}) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) \in {Base}_{R}$
51	37 43 49 50	syl3anc	$⊢ (φ \land y \in (0 \dots I + J)) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) \in {Base}_{R}$
52	51	fmpttd	$⊢ φ \to (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) : (0 \dots I + J) ⟶ {Base}_{R}$
53		eldifsn	$⊢ y \in ((0 \dots I + J) ∖ \{I\}) \leftrightarrow (y \in (0 \dots I + J) \land y \neq I)$
54	41	adantl	$⊢ (φ \land y \in (0 \dots I + J)) \to y \in ℕ_{0}$
55	54	nn0red	$⊢ (φ \land y \in (0 \dots I + J)) \to y \in ℝ$
56	31	adantr	$⊢ (φ \land y \in (0 \dots I + J)) \to I \in ℝ$
57	55 56	lttri2d	$⊢ (φ \land y \in (0 \dots I + J)) \to (y \neq I \leftrightarrow (y < I \lor I < y))$
58	10	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to G \in B$
59	47	adantl	$⊢ (φ \land y \in (0 \dots I + J)) \to I + J - y \in ℕ_{0}$
60	59	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to I + J - y \in ℕ_{0}$
61	5 1 4	deg1xrcl	$⊢ G \in B \to D (G) \in ℝ^{*}$
62	10 61	syl	$⊢ φ \to D (G) \in ℝ^{*}$
63	62	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to D (G) \in ℝ^{*}$
64	11	nn0red	$⊢ φ \to J \in ℝ$
65	64	rexrd	$⊢ φ \to J \in ℝ^{*}$
66	65	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to J \in ℝ^{*}$
67	16	nn0red	$⊢ φ \to I + J \in ℝ$
68	67	adantr	$⊢ (φ \land y \in (0 \dots I + J)) \to I + J \in ℝ$
69	68 55	resubcld	$⊢ (φ \land y \in (0 \dots I + J)) \to I + J - y \in ℝ$
70	69	rexrd	$⊢ (φ \land y \in (0 \dots I + J)) \to I + J - y \in ℝ^{*}$
71	70	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to I + J - y \in ℝ^{*}$
72	12	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to D (G) \leq J$
73	64	adantr	$⊢ (φ \land y \in (0 \dots I + J)) \to J \in ℝ$
74	55 56 73	ltadd1d	$⊢ (φ \land y \in (0 \dots I + J)) \to (y < I \leftrightarrow y + J < I + J)$
75	55 73 68	ltaddsub2d	$⊢ (φ \land y \in (0 \dots I + J)) \to (y + J < I + J \leftrightarrow J < I + J - y)$
76	74 75	bitrd	$⊢ (φ \land y \in (0 \dots I + J)) \to (y < I \leftrightarrow J < I + J - y)$
77	76	biimpa	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to J < I + J - y$
78	63 66 71 72 77	xrlelttrd	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to D (G) < I + J - y$
79	5 1 4 27 44	deg1lt	$⊢ (G \in B \land I + J - y \in ℕ_{0} \land D (G) < I + J - y) \to {coe}_{1} (G) (I + J - y) = 0_{R}$
80	58 60 78 79	syl3anc	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to {coe}_{1} (G) (I + J - y) = 0_{R}$
81	80	oveq2d	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = {coe}_{1} (F) (y) \underset{˙}{\cdot} 0_{R}$
82	26 3 27	ringrz	$⊢ (R \in Ring \land {coe}_{1} (F) (y) \in {Base}_{R}) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} 0_{R} = 0_{R}$
83	37 43 82	syl2anc	$⊢ (φ \land y \in (0 \dots I + J)) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} 0_{R} = 0_{R}$
84	83	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} 0_{R} = 0_{R}$
85	81 84	eqtrd	$⊢ ((φ \land y \in (0 \dots I + J)) \land y < I) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
86	7	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to F \in B$
87	54	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to y \in ℕ_{0}$
88	5 1 4	deg1xrcl	$⊢ F \in B \to D (F) \in ℝ^{*}$
89	7 88	syl	$⊢ φ \to D (F) \in ℝ^{*}$
90	89	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to D (F) \in ℝ^{*}$
91	31	rexrd	$⊢ φ \to I \in ℝ^{*}$
92	91	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to I \in ℝ^{*}$
93	55	rexrd	$⊢ (φ \land y \in (0 \dots I + J)) \to y \in ℝ^{*}$
94	93	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to y \in ℝ^{*}$
95	9	ad2antrr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to D (F) \leq I$
96		simpr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to I < y$
97	90 92 94 95 96	xrlelttrd	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to D (F) < y$
98	5 1 4 27 38	deg1lt	$⊢ (F \in B \land y \in ℕ_{0} \land D (F) < y) \to {coe}_{1} (F) (y) = 0_{R}$
99	86 87 97 98	syl3anc	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to {coe}_{1} (F) (y) = 0_{R}$
100	99	oveq1d	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R} \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)$
101	26 3 27	ringlz	$⊢ (R \in Ring \land {coe}_{1} (G) (I + J - y) \in {Base}_{R}) \to 0_{R} \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
102	37 49 101	syl2anc	$⊢ (φ \land y \in (0 \dots I + J)) \to 0_{R} \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
103	102	adantr	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to 0_{R} \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
104	100 103	eqtrd	$⊢ ((φ \land y \in (0 \dots I + J)) \land I < y) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
105	85 104	jaodan	$⊢ ((φ \land y \in (0 \dots I + J)) \land (y < I \lor I < y)) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
106	105	ex	$⊢ (φ \land y \in (0 \dots I + J)) \to ((y < I \lor I < y) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R})$
107	57 106	sylbid	$⊢ (φ \land y \in (0 \dots I + J)) \to (y \neq I \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R})$
108	107	impr	$⊢ (φ \land (y \in (0 \dots I + J) \land y \neq I)) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
109	53 108	sylan2b	$⊢ (φ \land y \in ((0 \dots I + J) ∖ \{I\})) \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = 0_{R}$
110	109 30	suppss2	$⊢ φ \to (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) supp 0_{R} \subseteq \{I\}$
111	26 27 29 30 36 52 110	gsumpt	$⊢ φ \to {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) = (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) (I)$
112		fveq2	$⊢ y = I \to {coe}_{1} (F) (y) = {coe}_{1} (F) (I)$
113		oveq2	$⊢ y = I \to I + J - y = I + J - I$
114	113	fveq2d	$⊢ y = I \to {coe}_{1} (G) (I + J - y) = {coe}_{1} (G) (I + J - I)$
115	112 114	oveq12d	$⊢ y = I \to {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - I)$
116		eqid	$⊢ (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) = (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y))$
117		ovex	$⊢ {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - I) \in V$
118	115 116 117	fvmpt	$⊢ I \in (0 \dots I + J) \to (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) (I) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - I)$
119	36 118	syl	$⊢ φ \to (y \in (0 \dots I + J) ⟼ {coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) (I) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - I)$
120	8	nn0cnd	$⊢ φ \to I \in ℂ$
121	11	nn0cnd	$⊢ φ \to J \in ℂ$
122	120 121	pncan2d	$⊢ φ \to I + J - I = J$
123	122	fveq2d	$⊢ φ \to {coe}_{1} (G) (I + J - I) = {coe}_{1} (G) (J)$
124	123	oveq2d	$⊢ φ \to {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - I) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (J)$
125	111 119 124	3eqtrd	$⊢ φ \to {\sum_{R}}_{y = 0}^{I + J} ({coe}_{1} (F) (y) \underset{˙}{\cdot} {coe}_{1} (G) (I + J - y)) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (J)$
126	15 25 125	3eqtrd	$⊢ φ \to {coe}_{1} (F \underset{˙}{∙} G) (I + J) = {coe}_{1} (F) (I) \underset{˙}{\cdot} {coe}_{1} (G) (J)$

Metamath Proof Explorer

Theorem coe1mul3

Proof