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

Metamath Proof Explorer

Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015) (Proof shortened by SN, 12-Mar-2025)

Ref Expression
Hypotheses ply1scl.p 
|- P = ( Poly1 ` R )
ply1scl.a 
|- A = ( algSc ` P )
ply1scl1.o 
|- .1. = ( 1r ` R )
ply1scl1.n 
|- N = ( 1r ` P )
Assertion ply1scl1 
|- ( R e. Ring -> ( A ` .1. ) = N )

Proof

Step Hyp Ref Expression
1 ply1scl.p 
 |-  P = ( Poly1 ` R )
2 ply1scl.a 
 |-  A = ( algSc ` P )
3 ply1scl1.o 
 |-  .1. = ( 1r ` R )
4 ply1scl1.n 
 |-  N = ( 1r ` P )
5 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
6 5 fveq2d 
 |-  ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
7 3 6 eqtrid 
 |-  ( R e. Ring -> .1. = ( 1r ` ( Scalar ` P ) ) )
8 7 fveq2d 
 |-  ( R e. Ring -> ( A ` .1. ) = ( A ` ( 1r ` ( Scalar ` P ) ) ) )
9 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
10 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
11 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 2 9 10 11 ascl1 
 |-  ( R e. Ring -> ( A ` ( 1r ` ( Scalar ` P ) ) ) = ( 1r ` P ) )
13 8 12 eqtrd 
 |-  ( R e. Ring -> ( A ` .1. ) = ( 1r ` P ) )
14 13 4 eqtr4di 
 |-  ( R e. Ring -> ( A ` .1. ) = N )