Metamath Proof Explorer

Theorem ply1sclrmsm

Description: The ring multiplication of a polynomial with a scalar polynomial is equal to the scalar multiplication of the polynomial with the corresponding scalar. (Contributed by AV, 14-Aug-2019)

Ref Expression
Hypotheses ply1sclrmsm.k 
|- K = ( Base ` R )
ply1sclrmsm.p 
|- P = ( Poly1 ` R )
ply1sclrmsm.b 
|- E = ( Base ` P )
ply1sclrmsm.x 
|- X = ( var1 ` R )
ply1sclrmsm.s 
|- .x. = ( .s ` P )
ply1sclrmsm.m 
|- .X. = ( .r ` P )
ply1sclrmsm.n 
|- N = ( mulGrp ` P )
ply1sclrmsm.e 
|- .^ = ( .g ` N )
ply1sclrmsm.a 
|- A = ( algSc ` P )
Assertion ply1sclrmsm 
|- ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( ( A ` F ) .X. Z ) = ( F .x. Z ) )

Proof

Step Hyp Ref Expression
1 ply1sclrmsm.k 
 |-  K = ( Base ` R )
2 ply1sclrmsm.p 
 |-  P = ( Poly1 ` R )
3 ply1sclrmsm.b 
 |-  E = ( Base ` P )
4 ply1sclrmsm.x 
 |-  X = ( var1 ` R )
5 ply1sclrmsm.s 
 |-  .x. = ( .s ` P )
6 ply1sclrmsm.m 
 |-  .X. = ( .r ` P )
7 ply1sclrmsm.n 
 |-  N = ( mulGrp ` P )
8 ply1sclrmsm.e 
 |-  .^ = ( .g ` N )
9 ply1sclrmsm.a 
 |-  A = ( algSc ` P )
10 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
11 10 fveq2d 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
12 1 11 syl5eq 
 |-  ( R e. Ring -> K = ( Base ` ( Scalar ` P ) ) )
13 12 eleq2d 
 |-  ( R e. Ring -> ( F e. K <-> F e. ( Base ` ( Scalar ` P ) ) ) )
14 13 biimpa 
 |-  ( ( R e. Ring /\ F e. K ) -> F e. ( Base ` ( Scalar ` P ) ) )
15 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
16 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
17 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
18 9 15 16 5 17 asclval 
 |-  ( F e. ( Base ` ( Scalar ` P ) ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
19 14 18 syl 
 |-  ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
20 19 3adant3 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) )
21 20 oveq1d 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( ( A ` F ) .X. Z ) = ( ( F .x. ( 1r ` P ) ) .X. Z ) )
22 simp1 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> R e. Ring )
23 1 eleq2i 
 |-  ( F e. K <-> F e. ( Base ` R ) )
24 23 biimpi 
 |-  ( F e. K -> F e. ( Base ` R ) )
25 24 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> F e. ( Base ` R ) )
26 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
27 3 17 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. E )
28 26 27 syl 
 |-  ( R e. Ring -> ( 1r ` P ) e. E )
29 28 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( 1r ` P ) e. E )
30 simp3 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> Z e. E )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 2 6 3 31 5 ply1ass23l 
 |-  ( ( R e. Ring /\ ( F e. ( Base ` R ) /\ ( 1r ` P ) e. E /\ Z e. E ) ) -> ( ( F .x. ( 1r ` P ) ) .X. Z ) = ( F .x. ( ( 1r ` P ) .X. Z ) ) )
33 22 25 29 30 32 syl13anc 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( ( F .x. ( 1r ` P ) ) .X. Z ) = ( F .x. ( ( 1r ` P ) .X. Z ) ) )
34 3 6 17 ringlidm 
 |-  ( ( P e. Ring /\ Z e. E ) -> ( ( 1r ` P ) .X. Z ) = Z )
35 26 34 sylan 
 |-  ( ( R e. Ring /\ Z e. E ) -> ( ( 1r ` P ) .X. Z ) = Z )
36 35 3adant2 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( ( 1r ` P ) .X. Z ) = Z )
37 36 oveq2d 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( F .x. ( ( 1r ` P ) .X. Z ) ) = ( F .x. Z ) )
38 21 33 37 3eqtrd 
 |-  ( ( R e. Ring /\ F e. K /\ Z e. E ) -> ( ( A ` F ) .X. Z ) = ( F .x. Z ) )