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

Metamath Proof Explorer

Theorem coe1id

Description: Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019)

Ref Expression
Hypotheses coe1id.p 
|- P = ( Poly1 ` R )
coe1id.i 
|- I = ( 1r ` P )
coe1id.0 
|- .0. = ( 0g ` R )
coe1id.1 
|- .1. = ( 1r ` R )
Assertion coe1id 
|- ( R e. Ring -> ( coe1 ` I ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 coe1id.p 
 |-  P = ( Poly1 ` R )
2 coe1id.i 
 |-  I = ( 1r ` P )
3 coe1id.0 
 |-  .0. = ( 0g ` R )
4 coe1id.1 
 |-  .1. = ( 1r ` R )
5 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
6 1 5 4 2 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` .1. ) = I )
7 6 eqcomd 
 |-  ( R e. Ring -> I = ( ( algSc ` P ) ` .1. ) )
8 7 fveq2d 
 |-  ( R e. Ring -> ( coe1 ` I ) = ( coe1 ` ( ( algSc ` P ) ` .1. ) ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
11 1 5 9 3 coe1scl 
 |-  ( ( R e. Ring /\ .1. e. ( Base ` R ) ) -> ( coe1 ` ( ( algSc ` P ) ` .1. ) ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )
12 10 11 mpdan 
 |-  ( R e. Ring -> ( coe1 ` ( ( algSc ` P ) ` .1. ) ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )
13 8 12 eqtrd 
 |-  ( R e. Ring -> ( coe1 ` I ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )