Theorem coe1zfv

Description: The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	coe1zfv.1	|- P = ( Poly1 ` R )
	coe1zfv.2	|- Z = ( 0g ` P )
	coe1zfv.3	|- .0. = ( 0g ` R )
	coe1zfv.4	|- ( ph -> R e. Ring )
	coe1zfv.5	|- ( ph -> N e. NN0 )
Assertion	coe1zfv	|- ( ph -> ( ( coe1 ` Z ) ` N ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		coe1zfv.1	|- P = ( Poly1 ` R )
2		coe1zfv.2	|- Z = ( 0g ` P )
3		coe1zfv.3	|- .0. = ( 0g ` R )
4		coe1zfv.4	|- ( ph -> R e. Ring )
5		coe1zfv.5	|- ( ph -> N e. NN0 )
6	1 2 3	coe1z	|- ( R e. Ring -> ( coe1 ` Z ) = ( NN0 X. { .0. } ) )
7	4 6	syl	|- ( ph -> ( coe1 ` Z ) = ( NN0 X. { .0. } ) )
8	7	fveq1d	|- ( ph -> ( ( coe1 ` Z ) ` N ) = ( ( NN0 X. { .0. } ) ` N ) )
9	3	fvexi	|- .0. e. _V
10	9	fvconst2	|- ( N e. NN0 -> ( ( NN0 X. { .0. } ) ` N ) = .0. )
11	5 10	syl	|- ( ph -> ( ( NN0 X. { .0. } ) ` N ) = .0. )
12	8 11	eqtrd	|- ( ph -> ( ( coe1 ` Z ) ` N ) = .0. )