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 ffvelrn ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 0 ) ∈ ℂ )
15 12 13 14 sylancl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ‘ 0 ) ∈ ℂ )
16 15 ad2antrr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( deg ‘ 𝐹 ) = 0 ) ∧ 𝑧 ∈ ℂ ) → ( ( coeff ‘ 𝐹 ) ‘ 0 ) ∈ ℂ )
17 16 mulid1d ( ( ( 𝐹 ∈ ( 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 ffvelrn ( ( 𝐹 : ℂ ⟶ ℂ ∧ 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 ) } ) ) )