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 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( deg ‘ 𝐹 ) = 0 ↔ 𝐹 = ( ℂ × { ( 𝐹 ‘ 0 ) } ) ) )

Proof

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