coe1zfv

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

Step	Hyp	Ref	Expression
1		coe1zfv.1	$⊢ P = {Poly}_{1} (R)$
2		coe1zfv.2	$⊢ Z = 0_{P}$
3		coe1zfv.3	$⊢ \underset{˙}{0} = 0_{R}$
4		coe1zfv.4	$⊢ φ \to R \in Ring$
5		coe1zfv.5	$⊢ φ \to N \in ℕ_{0}$
6	1 2 3	coe1z	$⊢ R \in Ring \to {coe}_{1} (Z) = ℕ_{0} \times \{\underset{˙}{0}\}$
7	4 6	syl	$⊢ φ \to {coe}_{1} (Z) = ℕ_{0} \times \{\underset{˙}{0}\}$
8	7	fveq1d	$⊢ φ \to {coe}_{1} (Z) (N) = (ℕ_{0} \times \{\underset{˙}{0}\}) (N)$
9	3	fvexi	$⊢ \underset{˙}{0} \in V$
10	9	fvconst2	$⊢ N \in ℕ_{0} \to (ℕ_{0} \times \{\underset{˙}{0}\}) (N) = \underset{˙}{0}$
11	5 10	syl	$⊢ φ \to (ℕ_{0} \times \{\underset{˙}{0}\}) (N) = \underset{˙}{0}$
12	8 11	eqtrd	$⊢ φ \to {coe}_{1} (Z) (N) = \underset{˙}{0}$

Metamath Proof Explorer