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 ) } ) ) )