Theorem plymul02

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

	Ref	Expression
Assertion	plymul02	|- ( F e. ( Poly ` S ) -> ( 0p oF x. F ) = 0p )

Proof

Step	Hyp	Ref	Expression
1		plyf	|- ( F e. ( Poly ` S ) -> F : CC --> CC )
2	1	ffvelcdmda	|- ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( F ` x ) e. CC )
3	2	mul02d	|- ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( 0 x. ( F ` x ) ) = 0 )
4	3	mpteq2dva	|- ( F e. ( Poly ` S ) -> ( x e. CC |-> ( 0 x. ( F ` x ) ) ) = ( x e. CC |-> 0 ) )
5		c0ex	|- 0 e. _V
6	5	fconst	|- ( CC X. { 0 } ) : CC --> { 0 }
7		df-0p	|- 0p = ( CC X. { 0 } )
8	7	feq1i	|- ( 0p : CC --> { 0 } <-> ( CC X. { 0 } ) : CC --> { 0 } )
9	6 8	mpbir	|- 0p : CC --> { 0 }
10		ffn	|- ( 0p : CC --> { 0 } -> 0p Fn CC )
11	9 10	mp1i	|- ( F e. ( Poly ` S ) -> 0p Fn CC )
12	1	ffnd	|- ( F e. ( Poly ` S ) -> F Fn CC )
13		cnex	|- CC e. _V
14	13	a1i	|- ( F e. ( Poly ` S ) -> CC e. _V )
15		inidm	|- ( CC i^i CC ) = CC
16		0pval	|- ( x e. CC -> ( 0p ` x ) = 0 )
17	16	adantl	|- ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( 0p ` x ) = 0 )
18		eqidd	|- ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( F ` x ) = ( F ` x ) )
19	11 12 14 14 15 17 18	offval	|- ( F e. ( Poly ` S ) -> ( 0p oF x. F ) = ( x e. CC |-> ( 0 x. ( F ` x ) ) ) )
20		fconstmpt	|- ( CC X. { 0 } ) = ( x e. CC |-> 0 )
21	7 20	eqtri	|- 0p = ( x e. CC |-> 0 )
22	21	a1i	|- ( F e. ( Poly ` S ) -> 0p = ( x e. CC |-> 0 ) )
23	4 19 22	3eqtr4d	|- ( F e. ( Poly ` S ) -> ( 0p oF x. F ) = 0p )