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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
q1pdir.d ⊢ / = ( quot1p ‘ 𝑅 )
q1pdir.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
q1pdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
q1pdir.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑁 )
q1pvsca.1 ⊢ × = ( ·𝑠 ‘ 𝑃 )
q1pvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
q1pvsca.8 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
Assertion q1pvsca ( 𝜑 → ( ( 𝐵 × 𝐴 ) / 𝐶 ) = ( 𝐵 × ( 𝐴 / 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 q1pdir.d ⊢ / = ( quot1p ‘ 𝑅 )
5 q1pdir.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 q1pdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7 q1pdir.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑁 )
8 q1pvsca.1 ⊢ × = ( ·𝑠 ‘ 𝑃 )
9 q1pvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
10 q1pvsca.8 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
11 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
13 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
14 5 13 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
15 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
16 5 15 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
17 16 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
18 9 17 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
19 10 18 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
20 2 11 8 12 14 19 6 lmodvscld ⊢ ( 𝜑 → ( 𝐵 × 𝐴 ) ∈ 𝑈 )
21 4 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( 𝐴 / 𝐶 ) ∈ 𝑈 )
22 5 6 7 21 syl3anc ⊢ ( 𝜑 → ( 𝐴 / 𝐶 ) ∈ 𝑈 )
23 2 11 8 12 14 19 22 lmodvscld ⊢ ( 𝜑 → ( 𝐵 × ( 𝐴 / 𝐶 ) ) ∈ 𝑈 )
24 14 lmodgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
25 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
26 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
27 5 26 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
28 1 2 3 uc1pcl ⊢ ( 𝐶 ∈ 𝑁 → 𝐶 ∈ 𝑈 )
29 7 28 syl ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
30 2 25 27 23 29 ringcld ⊢ ( 𝜑 → ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 )
31 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
32 2 31 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ ( 𝐵 × 𝐴 ) ∈ 𝑈 ∧ ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 ) → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
33 24 20 30 32 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
34 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
35 34 1 2 deg1xrcl ⊢ ( ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ∈ ℝ* )
36 33 35 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ∈ ℝ* )
37 eqid ⊢ ( rem1p ‘ 𝑅 ) = ( rem1p ‘ 𝑅 )
38 37 1 2 4 25 31 r1pval ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
39 6 29 38 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
40 2 25 27 22 29 ringcld ⊢ ( 𝜑 → ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 )
41 2 31 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐴 ∈ 𝑈 ∧ ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 ) → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
42 24 6 40 41 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
43 39 42 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 )
44 34 1 2 deg1xrcl ⊢ ( ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) ∈ ℝ* )
45 43 44 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) ∈ ℝ* )
46 34 1 2 deg1xrcl ⊢ ( 𝐶 ∈ 𝑈 → ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ∈ ℝ* )
47 29 46 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ∈ ℝ* )
48 1 34 5 2 9 8 10 42 deg1vscale ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ) ≤ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
49 1 25 2 9 8 ply1ass23l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐵 ∈ 𝐾 ∧ ( 𝐴 / 𝐶 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) ) → ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) = ( 𝐵 × ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
50 5 10 22 29 49 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) = ( 𝐵 × ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
51 50 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( 𝐵 × ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
52 2 8 11 12 31 14 19 6 40 lmodsubdi ⊢ ( 𝜑 → ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( 𝐵 × ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
53 51 52 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
54 53 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ) )
55 39 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
56 48 54 55 3brtr4d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ≤ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) )
57 37 1 2 3 34 r1pdeglt ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
58 5 6 7 57 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
59 36 45 47 56 58 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
60 4 1 2 34 31 25 3 q1peqb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐵 × 𝐴 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ∈ 𝑈 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ) ↔ ( ( 𝐵 × 𝐴 ) / 𝐶 ) = ( 𝐵 × ( 𝐴 / 𝐶 ) ) ) )
61 60 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐵 × 𝐴 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) ∧ ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ∈ 𝑈 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ) ) → ( ( 𝐵 × 𝐴 ) / 𝐶 ) = ( 𝐵 × ( 𝐴 / 𝐶 ) ) )
62 5 20 7 23 59 61 syl32anc ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) / 𝐶 ) = ( 𝐵 × ( 𝐴 / 𝐶 ) ) )