Metamath Proof Explorer

Theorem 0dgrb

Description: A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion 0dgrb ⊢ F ∈ Poly ⁡ S → deg ⁡ F = 0 ↔ F = ℂ × F ⁡ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ coeff ⁡ F = coeff ⁡ F
2 eqid ⊢ deg ⁡ F = deg ⁡ F
3 1 2 coeid ⊢ F ∈ Poly ⁡ S → F = z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k
4 3 adantr ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F = z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k
5 simplr ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → deg ⁡ F = 0
6 5 oveq2d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → 0 … deg ⁡ F = 0 … 0
7 6 sumeq1d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k = ∑ k = 0 0 coeff ⁡ F ⁡ k ⁢ z k
8 0z ⊢ 0 ∈ ℤ
9 exp0 ⊢ z ∈ ℂ → z 0 = 1
10 9 adantl ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → z 0 = 1
11 10 oveq2d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → coeff ⁡ F ⁡ 0 ⁢ z 0 = coeff ⁡ F ⁡ 0 ⋅ 1
12 1 coef3 ⊢ F ∈ Poly ⁡ S → coeff ⁡ F : ℕ 0 ⟶ ℂ
13 0nn0 ⊢ 0 ∈ ℕ 0
14 ffvelcdm ⊢ coeff ⁡ F : ℕ 0 ⟶ ℂ ∧ 0 ∈ ℕ 0 → coeff ⁡ F ⁡ 0 ∈ ℂ
15 12 13 14 sylancl ⊢ F ∈ Poly ⁡ S → coeff ⁡ F ⁡ 0 ∈ ℂ
16 15 ad2antrr ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → coeff ⁡ F ⁡ 0 ∈ ℂ
17 16 mulridd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → coeff ⁡ F ⁡ 0 ⋅ 1 = coeff ⁡ F ⁡ 0
18 11 17 eqtrd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → coeff ⁡ F ⁡ 0 ⁢ z 0 = coeff ⁡ F ⁡ 0
19 18 16 eqeltrd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → coeff ⁡ F ⁡ 0 ⁢ z 0 ∈ ℂ
20 fveq2 ⊢ k = 0 → coeff ⁡ F ⁡ k = coeff ⁡ F ⁡ 0
21 oveq2 ⊢ k = 0 → z k = z 0
22 20 21 oveq12d ⊢ k = 0 → coeff ⁡ F ⁡ k ⁢ z k = coeff ⁡ F ⁡ 0 ⁢ z 0
23 22 fsum1 ⊢ 0 ∈ ℤ ∧ coeff ⁡ F ⁡ 0 ⁢ z 0 ∈ ℂ → ∑ k = 0 0 coeff ⁡ F ⁡ k ⁢ z k = coeff ⁡ F ⁡ 0 ⁢ z 0
24 8 19 23 sylancr ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → ∑ k = 0 0 coeff ⁡ F ⁡ k ⁢ z k = coeff ⁡ F ⁡ 0 ⁢ z 0
25 24 18 eqtrd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → ∑ k = 0 0 coeff ⁡ F ⁡ k ⁢ z k = coeff ⁡ F ⁡ 0
26 7 25 eqtrd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 ∧ z ∈ ℂ → ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k = coeff ⁡ F ⁡ 0
27 26 mpteq2dva ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k = z ∈ ℂ ⟼ coeff ⁡ F ⁡ 0
28 4 27 eqtrd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F = z ∈ ℂ ⟼ coeff ⁡ F ⁡ 0
29 fconstmpt ⊢ ℂ × coeff ⁡ F ⁡ 0 = z ∈ ℂ ⟼ coeff ⁡ F ⁡ 0
30 28 29 eqtr4di ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F = ℂ × coeff ⁡ F ⁡ 0
31 30 fveq1d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F ⁡ 0 = ℂ × coeff ⁡ F ⁡ 0 ⁡ 0
32 0cn ⊢ 0 ∈ ℂ
33 fvex ⊢ coeff ⁡ F ⁡ 0 ∈ V
34 33 fvconst2 ⊢ 0 ∈ ℂ → ℂ × coeff ⁡ F ⁡ 0 ⁡ 0 = coeff ⁡ F ⁡ 0
35 32 34 ax-mp ⊢ ℂ × coeff ⁡ F ⁡ 0 ⁡ 0 = coeff ⁡ F ⁡ 0
36 31 35 eqtrdi ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F ⁡ 0 = coeff ⁡ F ⁡ 0
37 36 sneqd ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F ⁡ 0 = coeff ⁡ F ⁡ 0
38 37 xpeq2d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → ℂ × F ⁡ 0 = ℂ × coeff ⁡ F ⁡ 0
39 30 38 eqtr4d ⊢ F ∈ Poly ⁡ S ∧ deg ⁡ F = 0 → F = ℂ × F ⁡ 0
40 39 ex ⊢ F ∈ Poly ⁡ S → deg ⁡ F = 0 → F = ℂ × F ⁡ 0
41 plyf ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶ ℂ
42 ffvelcdm ⊢ F : ℂ ⟶ ℂ ∧ 0 ∈ ℂ → F ⁡ 0 ∈ ℂ
43 41 32 42 sylancl ⊢ F ∈ Poly ⁡ S → F ⁡ 0 ∈ ℂ
44 0dgr ⊢ F ⁡ 0 ∈ ℂ → deg ⁡ ℂ × F ⁡ 0 = 0
45 43 44 syl ⊢ F ∈ Poly ⁡ S → deg ⁡ ℂ × F ⁡ 0 = 0
46 fveqeq2 ⊢ F = ℂ × F ⁡ 0 → deg ⁡ F = 0 ↔ deg ⁡ ℂ × F ⁡ 0 = 0
47 45 46 syl5ibrcom ⊢ F ∈ Poly ⁡ S → F = ℂ × F ⁡ 0 → deg ⁡ F = 0
48 40 47 impbid ⊢ F ∈ Poly ⁡ S → deg ⁡ F = 0 ↔ F = ℂ × F ⁡ 0