Theorem coe1zfv

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

	Ref	Expression
Hypotheses	coe1zfv.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1zfv.2	$$⊢Z=0_P$$
	coe1zfv.3	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1zfv.4	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1zfv.5	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	coe1zfv	$$⊢\phi \to {\mathrm{coe}}_1\left(Z\right)\left(N\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		coe1zfv.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		coe1zfv.2	$$⊢Z=0_P$$
3		coe1zfv.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		coe1zfv.4	$$⊢\phi \to R\in \mathrm{Ring}$$
5		coe1zfv.5	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6	1 2 3	coe1z	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(Z\right)={\mathbb{N}}_0\times \left\{\underset{\dot{}}{0}\right\}$$
7	4 6	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(Z\right)={\mathbb{N}}_0\times \left\{\underset{\dot{}}{0}\right\}$$
8	7	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(Z\right)\left(N\right)=\left({\mathbb{N}}_0\times \left\{\underset{\dot{}}{0}\right\}\right)\left(N\right)$$
9	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	9	fvconst2	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{\underset{\dot{}}{0}\right\}\right)\left(N\right)=\underset{\dot{}}{0}$$
11	5 10	syl	$$⊢\phi \to \left({\mathbb{N}}_0\times \left\{\underset{\dot{}}{0}\right\}\right)\left(N\right)=\underset{\dot{}}{0}$$
12	8 11	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(Z\right)\left(N\right)=\underset{\dot{}}{0}$$