Metamath Proof Explorer

Theorem q1pvsca

Description: Scalar multiplication property of the polynomial division. (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 )
q1pdir.d 
|- ./ = ( quot1p ` R )
q1pdir.r 
|- ( ph -> R e. Ring )
q1pdir.a 
|- ( ph -> A e. U )
q1pdir.c 
|- ( ph -> C e. N )
q1pvsca.1 
|- .X. = ( .s ` P )
q1pvsca.k 
|- K = ( Base ` R )
q1pvsca.8 
|- ( ph -> B e. K )
Assertion q1pvsca 
|- ( ph -> ( ( B .X. A ) ./ C ) = ( B .X. ( A ./ C ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 q1pdir.d 
 |-  ./ = ( quot1p ` R )
5 q1pdir.r 
 |-  ( ph -> R e. Ring )
6 q1pdir.a 
 |-  ( ph -> A e. U )
7 q1pdir.c 
 |-  ( ph -> C e. N )
8 q1pvsca.1 
 |-  .X. = ( .s ` P )
9 q1pvsca.k 
 |-  K = ( Base ` R )
10 q1pvsca.8 
 |-  ( ph -> B e. K )
11 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
12 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
13 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
14 5 13 syl 
 |-  ( ph -> P e. LMod )
15 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
16 5 15 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
17 16 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
18 9 17 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` P ) ) )
19 10 18 eleqtrd 
 |-  ( ph -> B e. ( Base ` ( Scalar ` P ) ) )
20 2 11 8 12 14 19 6 lmodvscld 
 |-  ( ph -> ( B .X. A ) e. U )
21 4 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ C e. N ) -> ( A ./ C ) e. U )
22 5 6 7 21 syl3anc 
 |-  ( ph -> ( A ./ C ) e. U )
23 2 11 8 12 14 19 22 lmodvscld 
 |-  ( ph -> ( B .X. ( A ./ C ) ) e. U )
24 14 lmodgrpd 
 |-  ( ph -> P e. Grp )
25 eqid 
 |-  ( .r ` P ) = ( .r ` P )
26 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
27 5 26 syl 
 |-  ( ph -> P e. Ring )
28 1 2 3 uc1pcl 
 |-  ( C e. N -> C e. U )
29 7 28 syl 
 |-  ( ph -> C e. U )
30 2 25 27 23 29 ringcld 
 |-  ( ph -> ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) e. U )
31 eqid 
 |-  ( -g ` P ) = ( -g ` P )
32 2 31 grpsubcl 
 |-  ( ( P e. Grp /\ ( B .X. A ) e. U /\ ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) e. U ) -> ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) e. U )
33 24 20 30 32 syl3anc 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) e. U )
34 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
35 34 1 2 deg1xrcl 
 |-  ( ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) e. U -> ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) e. RR* )
36 33 35 syl 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) e. RR* )
37 eqid 
 |-  ( rem1p ` R ) = ( rem1p ` R )
38 37 1 2 4 25 31 r1pval 
 |-  ( ( A e. U /\ C e. U ) -> ( A ( rem1p ` R ) C ) = ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) )
39 6 29 38 syl2anc 
 |-  ( ph -> ( A ( rem1p ` R ) C ) = ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) )
40 2 25 27 22 29 ringcld 
 |-  ( ph -> ( ( A ./ C ) ( .r ` P ) C ) e. U )
41 2 31 grpsubcl 
 |-  ( ( P e. Grp /\ A e. U /\ ( ( A ./ C ) ( .r ` P ) C ) e. U ) -> ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) e. U )
42 24 6 40 41 syl3anc 
 |-  ( ph -> ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) e. U )
43 39 42 eqeltrd 
 |-  ( ph -> ( A ( rem1p ` R ) C ) e. U )
44 34 1 2 deg1xrcl 
 |-  ( ( A ( rem1p ` R ) C ) e. U -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) e. RR* )
45 43 44 syl 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) e. RR* )
46 34 1 2 deg1xrcl 
 |-  ( C e. U -> ( ( deg1 ` R ) ` C ) e. RR* )
47 29 46 syl 
 |-  ( ph -> ( ( deg1 ` R ) ` C ) e. RR* )
48 1 34 5 2 9 8 10 42 deg1vscale 
 |-  ( ph -> ( ( deg1 ` R ) ` ( B .X. ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) ) <_ ( ( deg1 ` R ) ` ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) )
49 1 25 2 9 8 ply1ass23l 
 |-  ( ( R e. Ring /\ ( B e. K /\ ( A ./ C ) e. U /\ C e. U ) ) -> ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) = ( B .X. ( ( A ./ C ) ( .r ` P ) C ) ) )
50 5 10 22 29 49 syl13anc 
 |-  ( ph -> ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) = ( B .X. ( ( A ./ C ) ( .r ` P ) C ) ) )
51 50 oveq2d 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) = ( ( B .X. A ) ( -g ` P ) ( B .X. ( ( A ./ C ) ( .r ` P ) C ) ) ) )
52 2 8 11 12 31 14 19 6 40 lmodsubdi 
 |-  ( ph -> ( B .X. ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) = ( ( B .X. A ) ( -g ` P ) ( B .X. ( ( A ./ C ) ( .r ` P ) C ) ) ) )
53 51 52 eqtr4d 
 |-  ( ph -> ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) = ( B .X. ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) )
54 53 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) = ( ( deg1 ` R ) ` ( B .X. ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) ) )
55 39 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) = ( ( deg1 ` R ) ` ( A ( -g ` P ) ( ( A ./ C ) ( .r ` P ) C ) ) ) )
56 48 54 55 3brtr4d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) <_ ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) )
57 37 1 2 3 34 r1pdeglt 
 |-  ( ( R e. Ring /\ A e. U /\ C e. N ) -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
58 5 6 7 57 syl3anc 
 |-  ( ph -> ( ( deg1 ` R ) ` ( A ( rem1p ` R ) C ) ) < ( ( deg1 ` R ) ` C ) )
59 36 45 47 56 58 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) )
60 4 1 2 34 31 25 3 q1peqb 
 |-  ( ( R e. Ring /\ ( B .X. A ) e. U /\ C e. N ) -> ( ( ( B .X. ( A ./ C ) ) e. U /\ ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) ) <-> ( ( B .X. A ) ./ C ) = ( B .X. ( A ./ C ) ) ) )
61 60 biimpa 
 |-  ( ( ( R e. Ring /\ ( B .X. A ) e. U /\ C e. N ) /\ ( ( B .X. ( A ./ C ) ) e. U /\ ( ( deg1 ` R ) ` ( ( B .X. A ) ( -g ` P ) ( ( B .X. ( A ./ C ) ) ( .r ` P ) C ) ) ) < ( ( deg1 ` R ) ` C ) ) ) -> ( ( B .X. A ) ./ C ) = ( B .X. ( A ./ C ) ) )
62 5 20 7 23 59 61 syl32anc 
 |-  ( ph -> ( ( B .X. A ) ./ C ) = ( B .X. ( A ./ C ) ) )