Theorem coe1zfv

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

	Ref	Expression
Hypotheses	coe1zfv.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1zfv.2	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	coe1zfv.3	⊢ 0 = ( 0g ‘ 𝑅 )
	coe1zfv.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1zfv.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	coe1zfv	⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		coe1zfv.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		coe1zfv.2	⊢ 𝑍 = ( 0g ‘ 𝑃 )
3		coe1zfv.3	⊢ 0 = ( 0g ‘ 𝑅 )
4		coe1zfv.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		coe1zfv.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6	1 2 3	coe1z	⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
7	4 6	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) = ( ( ℕ0 × { 0 } ) ‘ 𝑁 ) )
9	3	fvexi	⊢ 0 ∈ V
10	9	fvconst2	⊢ ( 𝑁 ∈ ℕ0 → ( ( ℕ0 × { 0 } ) ‘ 𝑁 ) = 0 )
11	5 10	syl	⊢ ( 𝜑 → ( ( ℕ0 × { 0 } ) ‘ 𝑁 ) = 0 )
12	8 11	eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) = 0 )