Metamath Proof Explorer

Theorem ply1scl0

Description: The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses ply1scl.p 
|- P = ( Poly1 ` R )
ply1scl.a 
|- A = ( algSc ` P )
ply1scl0.z 
|- .0. = ( 0g ` R )
ply1scl0.y 
|- Y = ( 0g ` P )
Assertion ply1scl0 
|- ( R e. Ring -> ( A ` .0. ) = Y )

Proof

Step Hyp Ref Expression
1 ply1scl.p 
 |-  P = ( Poly1 ` R )
2 ply1scl.a 
 |-  A = ( algSc ` P )
3 ply1scl0.z 
 |-  .0. = ( 0g ` R )
4 ply1scl0.y 
 |-  Y = ( 0g ` P )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 3 ring0cl 
 |-  ( R e. Ring -> .0. 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 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
12 2 7 9 10 11 asclval 
 |-  ( .0. e. ( Base ` R ) -> ( A ` .0. ) = ( .0. ( .s ` P ) ( 1r ` P ) ) )
13 6 12 syl 
 |-  ( R e. Ring -> ( A ` .0. ) = ( .0. ( .s ` P ) ( 1r ` P ) ) )
14 fvi 
 |-  ( R e. Ring -> ( _I ` R ) = R )
15 14 fveq2d 
 |-  ( R e. Ring -> ( 0g ` ( _I ` R ) ) = ( 0g ` R ) )
16 3 15 eqtr4id 
 |-  ( R e. Ring -> .0. = ( 0g ` ( _I ` R ) ) )
17 16 oveq1d 
 |-  ( R e. Ring -> ( .0. ( .s ` P ) ( 1r ` P ) ) = ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) )
18 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
19 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
20 eqid 
 |-  ( Base ` P ) = ( Base ` P )
21 20 11 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
22 19 21 syl 
 |-  ( R e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
23 eqid 
 |-  ( 0g ` ( _I ` R ) ) = ( 0g ` ( _I ` R ) )
24 20 7 10 23 4 lmod0vs 
 |-  ( ( P e. LMod /\ ( 1r ` P ) e. ( Base ` P ) ) -> ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) = Y )
25 18 22 24 syl2anc 
 |-  ( R e. Ring -> ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) = Y )
26 13 17 25 3eqtrd 
 |-  ( R e. Ring -> ( A ` .0. ) = Y )