coemulc

Description: The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014)

		Ref	Expression
	Assertion	coemulc	$⊢ (A \in ℂ \land F \in Poly (S)) \to coeff ((ℂ \times \{A\}) \times_{f} F) = (ℕ_{0} \times \{A\}) \times_{f} coeff (F)$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ ℂ \subseteq ℂ$
2		plyconst	$⊢ (ℂ \subseteq ℂ \land A \in ℂ) \to ℂ \times \{A\} \in Poly (ℂ)$
3	1 2	mpan	$⊢ A \in ℂ \to ℂ \times \{A\} \in Poly (ℂ)$
4		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
5	4	sseli	$⊢ F \in Poly (S) \to F \in Poly (ℂ)$
6		plymulcl	$⊢ (ℂ \times \{A\} \in Poly (ℂ) \land F \in Poly (ℂ)) \to (ℂ \times \{A\}) \times_{f} F \in Poly (ℂ)$
7	3 5 6	syl2an	$⊢ (A \in ℂ \land F \in Poly (S)) \to (ℂ \times \{A\}) \times_{f} F \in Poly (ℂ)$
8		eqid	$⊢ coeff ((ℂ \times \{A\}) \times_{f} F) = coeff ((ℂ \times \{A\}) \times_{f} F)$
9	8	coef3	$⊢ (ℂ \times \{A\}) \times_{f} F \in Poly (ℂ) \to coeff ((ℂ \times \{A\}) \times_{f} F) : ℕ_{0} ⟶ ℂ$
10		ffn	$⊢ coeff ((ℂ \times \{A\}) \times_{f} F) : ℕ_{0} ⟶ ℂ \to coeff ((ℂ \times \{A\}) \times_{f} F) Fn ℕ_{0}$
11	7 9 10	3syl	$⊢ (A \in ℂ \land F \in Poly (S)) \to coeff ((ℂ \times \{A\}) \times_{f} F) Fn ℕ_{0}$
12		fconstg	$⊢ A \in ℂ \to (ℕ_{0} \times \{A\}) : ℕ_{0} ⟶ \{A\}$
13	12	adantr	$⊢ (A \in ℂ \land F \in Poly (S)) \to (ℕ_{0} \times \{A\}) : ℕ_{0} ⟶ \{A\}$
14	13	ffnd	$⊢ (A \in ℂ \land F \in Poly (S)) \to (ℕ_{0} \times \{A\}) Fn ℕ_{0}$
15		eqid	$⊢ coeff (F) = coeff (F)$
16	15	coef3	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ ℂ$
17	16	adantl	$⊢ (A \in ℂ \land F \in Poly (S)) \to coeff (F) : ℕ_{0} ⟶ ℂ$
18	17	ffnd	$⊢ (A \in ℂ \land F \in Poly (S)) \to coeff (F) Fn ℕ_{0}$
19		nn0ex	$⊢ ℕ_{0} \in V$
20	19	a1i	$⊢ (A \in ℂ \land F \in Poly (S)) \to ℕ_{0} \in V$
21		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
22	14 18 20 20 21	offn	$⊢ (A \in ℂ \land F \in Poly (S)) \to ((ℕ_{0} \times \{A\}) \times_{f} coeff (F)) Fn ℕ_{0}$
23	3	ad2antrr	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to ℂ \times \{A\} \in Poly (ℂ)$
24		eqid	$⊢ coeff (ℂ \times \{A\}) = coeff (ℂ \times \{A\})$
25	24	coefv0	$⊢ ℂ \times \{A\} \in Poly (ℂ) \to (ℂ \times \{A\}) (0) = coeff (ℂ \times \{A\}) (0)$
26	23 25	syl	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to (ℂ \times \{A\}) (0) = coeff (ℂ \times \{A\}) (0)$
27		simpll	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to A \in ℂ$
28		0cn	$⊢ 0 \in ℂ$
29		fvconst2g	$⊢ (A \in ℂ \land 0 \in ℂ) \to (ℂ \times \{A\}) (0) = A$
30	27 28 29	sylancl	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to (ℂ \times \{A\}) (0) = A$
31	26 30	eqtr3d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (ℂ \times \{A\}) (0) = A$
32		simpr	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
33	32	nn0cnd	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to n \in ℂ$
34	33	subid1d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to n - 0 = n$
35	34	fveq2d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (F) (n - 0) = coeff (F) (n)$
36	31 35	oveq12d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0) = A coeff (F) (n)$
37	5	ad2antlr	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to F \in Poly (ℂ)$
38	24 15	coemul	$⊢ (ℂ \times \{A\} \in Poly (ℂ) \land F \in Poly (ℂ) \land n \in ℕ_{0}) \to coeff ((ℂ \times \{A\}) \times_{f} F) (n) = \sum_{k = 0}^{n} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k)$
39	23 37 32 38	syl3anc	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff ((ℂ \times \{A\}) \times_{f} F) (n) = \sum_{k = 0}^{n} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k)$
40		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
41	32 40	eleqtrdi	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to n \in ℤ_{\geq 0}$
42		fzss2	$⊢ n \in ℤ_{\geq 0} \to (0 \dots 0) \subseteq (0 \dots n)$
43	41 42	syl	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to (0 \dots 0) \subseteq (0 \dots n)$
44		elfz1eq	$⊢ k \in (0 \dots 0) \to k = 0$
45	44	adantl	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots 0)) \to k = 0$
46		fveq2	$⊢ k = 0 \to coeff (ℂ \times \{A\}) (k) = coeff (ℂ \times \{A\}) (0)$
47		oveq2	$⊢ k = 0 \to n - k = n - 0$
48	47	fveq2d	$⊢ k = 0 \to coeff (F) (n - k) = coeff (F) (n - 0)$
49	46 48	oveq12d	$⊢ k = 0 \to coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0)$
50	45 49	syl	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots 0)) \to coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0)$
51	17	ffvelcdmda	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (F) (n) \in ℂ$
52	27 51	mulcld	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to A coeff (F) (n) \in ℂ$
53	36 52	eqeltrd	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0) \in ℂ$
54	53	adantr	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots 0)) \to coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0) \in ℂ$
55	50 54	eqeltrd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in (0 \dots 0)) \to coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) \in ℂ$
56		eldifn	$⊢ k \in ((0 \dots n) ∖ (0 \dots 0)) \to \neg k \in (0 \dots 0)$
57	56	adantl	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to \neg k \in (0 \dots 0)$
58		eldifi	$⊢ k \in ((0 \dots n) ∖ (0 \dots 0)) \to k \in (0 \dots n)$
59		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
60	58 59	syl	$⊢ k \in ((0 \dots n) ∖ (0 \dots 0)) \to k \in ℕ_{0}$
61		eqid	$⊢ \deg (ℂ \times \{A\}) = \deg (ℂ \times \{A\})$
62	24 61	dgrub	$⊢ (ℂ \times \{A\} \in Poly (ℂ) \land k \in ℕ_{0} \land coeff (ℂ \times \{A\}) (k) \neq 0) \to k \leq \deg (ℂ \times \{A\})$
63	62	3expia	$⊢ (ℂ \times \{A\} \in Poly (ℂ) \land k \in ℕ_{0}) \to (coeff (ℂ \times \{A\}) (k) \neq 0 \to k \leq \deg (ℂ \times \{A\}))$
64	23 60 63	syl2an	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (coeff (ℂ \times \{A\}) (k) \neq 0 \to k \leq \deg (ℂ \times \{A\}))$
65		0dgr	$⊢ A \in ℂ \to \deg (ℂ \times \{A\}) = 0$
66	65	ad3antrrr	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to \deg (ℂ \times \{A\}) = 0$
67	66	breq2d	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (k \leq \deg (ℂ \times \{A\}) \leftrightarrow k \leq 0)$
68	60	adantl	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to k \in ℕ_{0}$
69		nn0le0eq0	$⊢ k \in ℕ_{0} \to (k \leq 0 \leftrightarrow k = 0)$
70	68 69	syl	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (k \leq 0 \leftrightarrow k = 0)$
71	67 70	bitrd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (k \leq \deg (ℂ \times \{A\}) \leftrightarrow k = 0)$
72	64 71	sylibd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (coeff (ℂ \times \{A\}) (k) \neq 0 \to k = 0)$
73		id	$⊢ k = 0 \to k = 0$
74		0z	$⊢ 0 \in ℤ$
75		elfz3	$⊢ 0 \in ℤ \to 0 \in (0 \dots 0)$
76	74 75	ax-mp	$⊢ 0 \in (0 \dots 0)$
77	73 76	eqeltrdi	$⊢ k = 0 \to k \in (0 \dots 0)$
78	72 77	syl6	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (coeff (ℂ \times \{A\}) (k) \neq 0 \to k \in (0 \dots 0))$
79	78	necon1bd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to (\neg k \in (0 \dots 0) \to coeff (ℂ \times \{A\}) (k) = 0)$
80	57 79	mpd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to coeff (ℂ \times \{A\}) (k) = 0$
81	80	oveq1d	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = 0 \cdot coeff (F) (n - k)$
82	17	adantr	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (F) : ℕ_{0} ⟶ ℂ$
83		fznn0sub	$⊢ k \in (0 \dots n) \to n - k \in ℕ_{0}$
84	58 83	syl	$⊢ k \in ((0 \dots n) ∖ (0 \dots 0)) \to n - k \in ℕ_{0}$
85		ffvelcdm	$⊢ (coeff (F) : ℕ_{0} ⟶ ℂ \land n - k \in ℕ_{0}) \to coeff (F) (n - k) \in ℂ$
86	82 84 85	syl2an	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to coeff (F) (n - k) \in ℂ$
87	86	mul02d	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to 0 \cdot coeff (F) (n - k) = 0$
88	81 87	eqtrd	$⊢ (((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \land k \in ((0 \dots n) ∖ (0 \dots 0))) \to coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = 0$
89		fzfid	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to (0 \dots n) \in Fin$
90	43 55 88 89	fsumss	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to \sum_{k = 0}^{0} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = \sum_{k = 0}^{n} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k)$
91	49	fsum1	$⊢ (0 \in ℤ \land coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0) \in ℂ) \to \sum_{k = 0}^{0} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0)$
92	74 53 91	sylancr	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to \sum_{k = 0}^{0} coeff (ℂ \times \{A\}) (k) coeff (F) (n - k) = coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0)$
93	39 90 92	3eqtr2d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff ((ℂ \times \{A\}) \times_{f} F) (n) = coeff (ℂ \times \{A\}) (0) coeff (F) (n - 0)$
94		simpl	$⊢ (A \in ℂ \land F \in Poly (S)) \to A \in ℂ$
95		eqidd	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff (F) (n) = coeff (F) (n)$
96	20 94 18 95	ofc1	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to ((ℕ_{0} \times \{A\}) \times_{f} coeff (F)) (n) = A coeff (F) (n)$
97	36 93 96	3eqtr4d	$⊢ ((A \in ℂ \land F \in Poly (S)) \land n \in ℕ_{0}) \to coeff ((ℂ \times \{A\}) \times_{f} F) (n) = ((ℕ_{0} \times \{A\}) \times_{f} coeff (F)) (n)$
98	11 22 97	eqfnfvd	$⊢ (A \in ℂ \land F \in Poly (S)) \to coeff ((ℂ \times \{A\}) \times_{f} F) = (ℕ_{0} \times \{A\}) \times_{f} coeff (F)$

Metamath Proof Explorer

Theorem coemulc

Proof