Theorem coe0

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

	Ref	Expression
Assertion	coe0	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		0cnd	$$⊢\top \to 0\in ℂ$$
2		ssid	$$⊢ℂ\subseteq ℂ$$
3		ply0	$$⊢ℂ\subseteq ℂ\to 0_{𝑝}\in \mathrm{Poly}\left(ℂ\right)$$
4	2 3	ax-mp	$$⊢0_{𝑝}\in \mathrm{Poly}\left(ℂ\right)$$
5		coemulc	$$⊢\left(0\in ℂ\wedge 0_{𝑝}\in \mathrm{Poly}\left(ℂ\right)\right)\to \mathrm{coeff}\left(\left(ℂ\times \left\{0\right\}\right){\times }_f{0}_{𝑝}\right)=\left({\mathbb{N}}_0\times \left\{0\right\}\right){\times }_f\mathrm{coeff}\left(0_{𝑝}\right)$$
6	1 4 5	sylancl	$$⊢\top \to \mathrm{coeff}\left(\left(ℂ\times \left\{0\right\}\right){\times }_f{0}_{𝑝}\right)=\left({\mathbb{N}}_0\times \left\{0\right\}\right){\times }_f\mathrm{coeff}\left(0_{𝑝}\right)$$
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8	7	a1i	$$⊢\top \to ℂ\in \mathrm{V}$$
9		plyf	$$⊢0_{𝑝}\in \mathrm{Poly}\left(ℂ\right)\to 0_{𝑝}:ℂ⟶ℂ$$
10	4 9	mp1i	$$⊢\top \to 0_{𝑝}:ℂ⟶ℂ$$
11		mul02	$$⊢x\in ℂ\to 0\cdot x=0$$
12	11	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to 0\cdot x=0$$
13	8 10 1 1 12	caofid2	$$⊢\top \to \left(ℂ\times \left\{0\right\}\right){\times }_f{0}_{𝑝}=ℂ\times \left\{0\right\}$$
14		df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$
15	13 14	eqtr4di	$$⊢\top \to \left(ℂ\times \left\{0\right\}\right){\times }_f{0}_{𝑝}=0_{𝑝}$$
16	15	fveq2d	$$⊢\top \to \mathrm{coeff}\left(\left(ℂ\times \left\{0\right\}\right){\times }_f{0}_{𝑝}\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
17		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
18	17	a1i	$$⊢\top \to {\mathbb{N}}_0\in \mathrm{V}$$
19		eqid	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
20	19	coef3	$$⊢0_{𝑝}\in \mathrm{Poly}\left(ℂ\right)\to \mathrm{coeff}\left(0_{𝑝}\right):{\mathbb{N}}_0⟶ℂ$$
21	4 20	mp1i	$$⊢\top \to \mathrm{coeff}\left(0_{𝑝}\right):{\mathbb{N}}_0⟶ℂ$$
22	18 21 1 1 12	caofid2	$$⊢\top \to \left({\mathbb{N}}_0\times \left\{0\right\}\right){\times }_f\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
23	6 16 22	3eqtr3d	$$⊢\top \to \mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
24	23	mptru	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$