This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )