Metamath Proof Explorer

Theorem ply1sclid

Description: Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p 
|- P = ( Poly1 ` R )
ply1scl.a 
|- A = ( algSc ` P )
ply1sclid.k 
|- K = ( Base ` R )
Assertion ply1sclid 
|- ( ( R e. Ring /\ X e. K ) -> X = ( ( coe1 ` ( A ` X ) ) ` 0 ) )

Proof

Step Hyp Ref Expression
1 ply1scl.p 
 |-  P = ( Poly1 ` R )
2 ply1scl.a 
 |-  A = ( algSc ` P )
3 ply1sclid.k 
 |-  K = ( Base ` R )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 1 2 3 4 coe1scl 
 |-  ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) )
6 5 fveq1d 
 |-  ( ( R e. Ring /\ X e. K ) -> ( ( coe1 ` ( A ` X ) ) ` 0 ) = ( ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) ` 0 ) )
7 0nn0 
 |-  0 e. NN0
8 iftrue 
 |-  ( x = 0 -> if ( x = 0 , X , ( 0g ` R ) ) = X )
9 eqid 
 |-  ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) = ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) )
10 8 9 fvmptg 
 |-  ( ( 0 e. NN0 /\ X e. K ) -> ( ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) ` 0 ) = X )
11 7 10 mpan 
 |-  ( X e. K -> ( ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) ` 0 ) = X )
12 11 adantl 
 |-  ( ( R e. Ring /\ X e. K ) -> ( ( x e. NN0 |-> if ( x = 0 , X , ( 0g ` R ) ) ) ` 0 ) = X )
13 6 12 eqtr2d 
 |-  ( ( R e. Ring /\ X e. K ) -> X = ( ( coe1 ` ( A ` X ) ) ` 0 ) )