Theorem plymul02

Description: Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018)

	Ref	Expression
Assertion	plymul02	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0_{𝑝}{\times }_{f}F=0_{𝑝}$$

Proof

Step	Hyp	Ref	Expression
1		plyf	$$⊢F\in \mathrm{Poly}\left(S\right)\to F:ℂ⟶ℂ$$
2	1	ffvelcdmda	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge x\in ℂ\right)\to F\left(x\right)\in ℂ$$
3	2	mul02d	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge x\in ℂ\right)\to 0\cdot F\left(x\right)=0$$
4	3	mpteq2dva	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(x\in ℂ⟼0\cdot F\left(x\right)\right)=\left(x\in ℂ⟼0\right)$$
5		c0ex	$$⊢0\in \mathrm{V}$$
6	5	fconst	$$⊢\left(ℂ\times \left\{0\right\}\right):ℂ⟶\left\{0\right\}$$
7		df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$
8	7	feq1i	$$⊢0_{𝑝}:ℂ⟶\left\{0\right\}\leftrightarrow \left(ℂ\times \left\{0\right\}\right):ℂ⟶\left\{0\right\}$$
9	6 8	mpbir	$$⊢0_{𝑝}:ℂ⟶\left\{0\right\}$$
10		ffn	$$⊢0_{𝑝}:ℂ⟶\left\{0\right\}\to 0_{𝑝}Fnℂ$$
11	9 10	mp1i	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0_{𝑝}Fnℂ$$
12	1	ffnd	$$⊢F\in \mathrm{Poly}\left(S\right)\to FFnℂ$$
13		cnex	$$⊢ℂ\in \mathrm{V}$$
14	13	a1i	$$⊢F\in \mathrm{Poly}\left(S\right)\to ℂ\in \mathrm{V}$$
15		inidm	$$⊢ℂ\cap ℂ=ℂ$$
16		0pval	$$⊢x\in ℂ\to 0_{𝑝}\left(x\right)=0$$
17	16	adantl	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge x\in ℂ\right)\to 0_{𝑝}\left(x\right)=0$$
18		eqidd	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge x\in ℂ\right)\to F\left(x\right)=F\left(x\right)$$
19	11 12 14 14 15 17 18	offval	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0_{𝑝}{\times }_{f}F=\left(x\in ℂ⟼0\cdot F\left(x\right)\right)$$
20		fconstmpt	$$⊢ℂ\times \left\{0\right\}=\left(x\in ℂ⟼0\right)$$
21	7 20	eqtri	$$⊢0_{𝑝}=\left(x\in ℂ⟼0\right)$$
22	21	a1i	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0_{𝑝}=\left(x\in ℂ⟼0\right)$$
23	4 19 22	3eqtr4d	$$⊢F\in \mathrm{Poly}\left(S\right)\to 0_{𝑝}{\times }_{f}F=0_{𝑝}$$