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

Metamath Proof Explorer

Theorem ply1ascl1

Description: The multiplicative identity scalar as a univariate polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025)

Ref Expression
Hypotheses ply1ascl1.w 
|- W = ( Poly1 ` R )
ply1ascl1.a 
|- A = ( algSc ` W )
ply1ascl1.i 
|- I = ( 1r ` R )
ply1ascl1.1 
|- .1. = ( 1r ` W )
ply1ascl1.r 
|- ( ph -> R e. Ring )
Assertion ply1ascl1 
|- ( ph -> ( A ` I ) = .1. )

Proof

Step Hyp Ref Expression
1 ply1ascl1.w 
 |-  W = ( Poly1 ` R )
2 ply1ascl1.a 
 |-  A = ( algSc ` W )
3 ply1ascl1.i 
 |-  I = ( 1r ` R )
4 ply1ascl1.1 
 |-  .1. = ( 1r ` W )
5 ply1ascl1.r 
 |-  ( ph -> R e. Ring )
6 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` W ) )
7 5 6 syl 
 |-  ( ph -> R = ( Scalar ` W ) )
8 7 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` W ) ) )
9 3 8 eqtrid 
 |-  ( ph -> I = ( 1r ` ( Scalar ` W ) ) )
10 9 fveq2d 
 |-  ( ph -> ( ( algSc ` W ) ` I ) = ( ( algSc ` W ) ` ( 1r ` ( Scalar ` W ) ) ) )
11 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 1 ply1lmod 
 |-  ( R e. Ring -> W e. LMod )
14 5 13 syl 
 |-  ( ph -> W e. LMod )
15 1 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
16 5 15 syl 
 |-  ( ph -> W e. Ring )
17 11 12 14 16 ascl1 
 |-  ( ph -> ( ( algSc ` W ) ` ( 1r ` ( Scalar ` W ) ) ) = ( 1r ` W ) )
18 10 17 eqtrd 
 |-  ( ph -> ( ( algSc ` W ) ` I ) = ( 1r ` W ) )
19 2 fveq1i 
 |-  ( A ` I ) = ( ( algSc ` W ) ` I )
20 18 19 4 3eqtr4g 
 |-  ( ph -> ( A ` I ) = .1. )