Metamath Proof Explorer

Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015)

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 3 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
7 1 ply1sca2 
 |-  ( _I ` R ) = ( Scalar ` P )
8 df-base 
 |-  Base = Slot 1
9 8 5 strfvi 
 |-  ( Base ` R ) = ( Base ` ( _I ` R ) )
10 eqid 
 |-  ( .s ` P ) = ( .s ` P )
11 2 7 9 10 4 asclval 
 |-  ( .1. e. ( Base ` R ) -> ( A ` .1. ) = ( .1. ( .s ` P ) N ) )
12 6 11 syl 
 |-  ( R e. Ring -> ( A ` .1. ) = ( .1. ( .s ` P ) N ) )
13 fvi 
 |-  ( R e. Ring -> ( _I ` R ) = R )
14 13 fveq2d 
 |-  ( R e. Ring -> ( 1r ` ( _I ` R ) ) = ( 1r ` R ) )
15 14 3 eqtr4di 
 |-  ( R e. Ring -> ( 1r ` ( _I ` R ) ) = .1. )
16 15 oveq1d 
 |-  ( R e. Ring -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = ( .1. ( .s ` P ) N ) )
17 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
18 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
19 eqid 
 |-  ( Base ` P ) = ( Base ` P )
20 19 4 ringidcl 
 |-  ( P e. Ring -> N e. ( Base ` P ) )
21 18 20 syl 
 |-  ( R e. Ring -> N e. ( Base ` P ) )
22 eqid 
 |-  ( 1r ` ( _I ` R ) ) = ( 1r ` ( _I ` R ) )
23 19 7 10 22 lmodvs1 
 |-  ( ( P e. LMod /\ N e. ( Base ` P ) ) -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = N )
24 17 21 23 syl2anc 
 |-  ( R e. Ring -> ( ( 1r ` ( _I ` R ) ) ( .s ` P ) N ) = N )
25 12 16 24 3eqtr2d 
 |-  ( R e. Ring -> ( A ` .1. ) = N )