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

Metamath Proof Explorer

Theorem coe1scl

Description: Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p 
|- P = ( Poly1 ` R )
ply1scl.a 
|- A = ( algSc ` P )
coe1scl.k 
|- K = ( Base ` R )
coe1scl.z 
|- .0. = ( 0g ` R )
Assertion coe1scl 
|- ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )

Proof

Step Hyp Ref Expression
1 ply1scl.p 
 |-  P = ( Poly1 ` R )
2 ply1scl.a 
 |-  A = ( algSc ` P )
3 coe1scl.k 
 |-  K = ( Base ` R )
4 coe1scl.z 
 |-  .0. = ( 0g ` R )
5 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
6 eqid 
 |-  ( .s ` P ) = ( .s ` P )
7 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
8 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
9 3 1 5 6 7 8 2 ply1scltm 
 |-  ( ( R e. Ring /\ X e. K ) -> ( A ` X ) = ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
10 9 fveq2d 
 |-  ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
11 0nn0 
 |-  0 e. NN0
12 4 3 1 5 6 7 8 coe1tm 
 |-  ( ( R e. Ring /\ X e. K /\ 0 e. NN0 ) -> ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
13 11 12 mp3an3 
 |-  ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
14 10 13 eqtrd 
 |-  ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )