Theorem coe0

Description: The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	coe0	⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )

Proof

Step	Hyp	Ref	Expression
1		0cnd	⊢ ( ⊤ → 0 ∈ ℂ )
2		ssid	⊢ ℂ ⊆ ℂ
3		ply0	⊢ ( ℂ ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ ℂ ) )
4	2 3	ax-mp	⊢ 0𝑝 ∈ ( Poly ‘ ℂ )
5		coemulc	⊢ ( ( 0 ∈ ℂ ∧ 0𝑝 ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) )
6	1 4 5	sylancl	⊢ ( ⊤ → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) )
7		cnex	⊢ ℂ ∈ V
8	7	a1i	⊢ ( ⊤ → ℂ ∈ V )
9		plyf	⊢ ( 0𝑝 ∈ ( Poly ‘ ℂ ) → 0𝑝 : ℂ ⟶ ℂ )
10	4 9	mp1i	⊢ ( ⊤ → 0𝑝 : ℂ ⟶ ℂ )
11		mul02	⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 )
12	11	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 )
13	8 10 1 1 12	caofid2	⊢ ( ⊤ → ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) = ( ℂ × { 0 } ) )
14		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
15	13 14	eqtr4di	⊢ ( ⊤ → ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) = 0𝑝 )
16	15	fveq2d	⊢ ( ⊤ → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( coeff ‘ 0𝑝 ) )
17		nn0ex	⊢ ℕ0 ∈ V
18	17	a1i	⊢ ( ⊤ → ℕ0 ∈ V )
19		eqid	⊢ ( coeff ‘ 0𝑝 ) = ( coeff ‘ 0𝑝 )
20	19	coef3	⊢ ( 0𝑝 ∈ ( Poly ‘ ℂ ) → ( coeff ‘ 0𝑝 ) : ℕ0 ⟶ ℂ )
21	4 20	mp1i	⊢ ( ⊤ → ( coeff ‘ 0𝑝 ) : ℕ0 ⟶ ℂ )
22	18 21 1 1 12	caofid2	⊢ ( ⊤ → ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) = ( ℕ0 × { 0 } ) )
23	6 16 22	3eqtr3d	⊢ ( ⊤ → ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } ) )
24	23	mptru	⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )