Theorem plymul02

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

	Ref	Expression
Assertion	plymul02	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0𝑝 ∘f · 𝐹 ) = 0𝑝 )

Proof

Step	Hyp	Ref	Expression
1		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
2	1	ffvelrnda	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
3	2	mul02d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 0 · ( 𝐹 ‘ 𝑥 ) ) = 0 )
4	3	mpteq2dva	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑥 ∈ ℂ ↦ ( 0 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
5		c0ex	⊢ 0 ∈ V
6	5	fconst	⊢ ( ℂ × { 0 } ) : ℂ ⟶ { 0 }
7		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
8	7	feq1i	⊢ ( 0𝑝 : ℂ ⟶ { 0 } ↔ ( ℂ × { 0 } ) : ℂ ⟶ { 0 } )
9	6 8	mpbir	⊢ 0𝑝 : ℂ ⟶ { 0 }
10		ffn	⊢ ( 0𝑝 : ℂ ⟶ { 0 } → 0𝑝 Fn ℂ )
11	9 10	mp1i	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0𝑝 Fn ℂ )
12	1	ffnd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 Fn ℂ )
13		cnex	⊢ ℂ ∈ V
14	13	a1i	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ℂ ∈ V )
15		inidm	⊢ ( ℂ ∩ ℂ ) = ℂ
16		0pval	⊢ ( 𝑥 ∈ ℂ → ( 0𝑝 ‘ 𝑥 ) = 0 )
17	16	adantl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 0𝑝 ‘ 𝑥 ) = 0 )
18		eqidd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19	11 12 14 14 15 17 18	offval	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0𝑝 ∘f · 𝐹 ) = ( 𝑥 ∈ ℂ ↦ ( 0 · ( 𝐹 ‘ 𝑥 ) ) ) )
20		fconstmpt	⊢ ( ℂ × { 0 } ) = ( 𝑥 ∈ ℂ ↦ 0 )
21	7 20	eqtri	⊢ 0𝑝 = ( 𝑥 ∈ ℂ ↦ 0 )
22	21	a1i	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0𝑝 = ( 𝑥 ∈ ℂ ↦ 0 ) )
23	4 19 22	3eqtr4d	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0𝑝 ∘f · 𝐹 ) = 0𝑝 )