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

Metamath Proof Explorer

Theorem r1pvsca

Description: Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1padd1.p 
|- P = ( Poly1 ` R )
r1padd1.u 
|- U = ( Base ` P )
r1padd1.n 
|- N = ( Unic1p ` R )
r1padd1.e 
|- E = ( rem1p ` R )
r1pvsca.6 
|- ( ph -> R e. Ring )
r1pvsca.7 
|- ( ph -> A e. U )
r1pvsca.10 
|- ( ph -> D e. N )
r1pvsca.1 
|- .X. = ( .s ` P )
r1pvsca.k 
|- K = ( Base ` R )
r1pvsca.2 
|- ( ph -> B e. K )
Assertion r1pvsca 
|- ( ph -> ( ( B .X. A ) E D ) = ( B .X. ( A E D ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 r1padd1.e 
 |-  E = ( rem1p ` R )
5 r1pvsca.6 
 |-  ( ph -> R e. Ring )
6 r1pvsca.7 
 |-  ( ph -> A e. U )
7 r1pvsca.10 
 |-  ( ph -> D e. N )
8 r1pvsca.1 
 |-  .X. = ( .s ` P )
9 r1pvsca.k 
 |-  K = ( Base ` R )
10 r1pvsca.2 
 |-  ( ph -> B e. K )
11 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
12 11 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ D e. N ) -> ( A ( quot1p ` R ) D ) e. U )
13 5 6 7 12 syl3anc 
 |-  ( ph -> ( A ( quot1p ` R ) D ) e. U )
14 1 2 3 uc1pcl 
 |-  ( D e. N -> D e. U )
15 7 14 syl 
 |-  ( ph -> D e. U )
16 eqid 
 |-  ( .r ` P ) = ( .r ` P )
17 1 16 2 9 8 ply1ass23l 
 |-  ( ( R e. Ring /\ ( B e. K /\ ( A ( quot1p ` R ) D ) e. U /\ D e. U ) ) -> ( ( B .X. ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) = ( B .X. ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
18 5 10 13 15 17 syl13anc 
 |-  ( ph -> ( ( B .X. ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) = ( B .X. ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
19 18 oveq2d 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( B .X. A ) ( -g ` P ) ( B .X. ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
20 1 2 3 11 5 6 7 8 9 10 q1pvsca 
 |-  ( ph -> ( ( B .X. A ) ( quot1p ` R ) D ) = ( B .X. ( A ( quot1p ` R ) D ) ) )
21 20 oveq1d 
 |-  ( ph -> ( ( ( B .X. A ) ( quot1p ` R ) D ) ( .r ` P ) D ) = ( ( B .X. ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) )
22 21 oveq2d 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( ( B .X. A ) ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) )
23 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
24 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
25 eqid 
 |-  ( -g ` P ) = ( -g ` P )
26 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
27 5 26 syl 
 |-  ( ph -> P e. LMod )
28 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
29 5 28 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
30 29 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
31 9 30 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` P ) ) )
32 10 31 eleqtrd 
 |-  ( ph -> B e. ( Base ` ( Scalar ` P ) ) )
33 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
34 5 33 syl 
 |-  ( ph -> P e. Ring )
35 2 16 34 13 15 ringcld 
 |-  ( ph -> ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) e. U )
36 2 8 23 24 25 27 32 6 35 lmodsubdi 
 |-  ( ph -> ( B .X. ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) = ( ( B .X. A ) ( -g ` P ) ( B .X. ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
37 19 22 36 3eqtr4d 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( ( B .X. A ) ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( B .X. ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
38 2 23 8 24 27 32 6 lmodvscld 
 |-  ( ph -> ( B .X. A ) e. U )
39 4 1 2 11 16 25 r1pval 
 |-  ( ( ( B .X. A ) e. U /\ D e. U ) -> ( ( B .X. A ) E D ) = ( ( B .X. A ) ( -g ` P ) ( ( ( B .X. A ) ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
40 38 15 39 syl2anc 
 |-  ( ph -> ( ( B .X. A ) E D ) = ( ( B .X. A ) ( -g ` P ) ( ( ( B .X. A ) ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
41 4 1 2 11 16 25 r1pval 
 |-  ( ( A e. U /\ D e. U ) -> ( A E D ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
42 6 15 41 syl2anc 
 |-  ( ph -> ( A E D ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
43 42 oveq2d 
 |-  ( ph -> ( B .X. ( A E D ) ) = ( B .X. ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
44 37 40 43 3eqtr4d 
 |-  ( ph -> ( ( B .X. A ) E D ) = ( B .X. ( A E D ) ) )