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 
|- 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. )