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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1pvsca.6 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
r1pvsca.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
r1pvsca.10 ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
r1pvsca.1 ⊢ × = ( ·𝑠 ‘ 𝑃 )
r1pvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
r1pvsca.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
Assertion r1pvsca ( 𝜑 → ( ( 𝐵 × 𝐴 ) 𝐸 𝐷 ) = ( 𝐵 × ( 𝐴 𝐸 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5 r1pvsca.6 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 r1pvsca.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7 r1pvsca.10 ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
8 r1pvsca.1 ⊢ × = ( ·𝑠 ‘ 𝑃 )
9 r1pvsca.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
10 r1pvsca.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
11 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
12 11 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
13 5 6 7 12 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
14 1 2 3 uc1pcl ⊢ ( 𝐷 ∈ 𝑁 → 𝐷 ∈ 𝑈 )
15 7 14 syl ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
16 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
17 1 16 2 9 8 ply1ass23l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐵 ∈ 𝐾 ∧ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) ) → ( ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) = ( 𝐵 × ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
18 5 10 13 15 17 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) = ( 𝐵 × ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
19 18 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( 𝐵 × ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
20 1 2 3 11 5 6 7 8 9 10 q1pvsca ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) = ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) )
21 20 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) = ( ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) )
22 21 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( 𝐵 × ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
23 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
24 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
25 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
26 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
27 5 26 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
28 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
29 5 28 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
30 29 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
31 9 30 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
32 10 31 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
33 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
34 5 33 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
35 2 16 34 13 15 ringcld ⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 )
36 2 8 23 24 25 27 32 6 35 lmodsubdi ⊢ ( 𝜑 → ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( 𝐵 × ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
37 19 22 36 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
38 2 23 8 24 27 32 6 lmodvscld ⊢ ( 𝜑 → ( 𝐵 × 𝐴 ) ∈ 𝑈 )
39 4 1 2 11 16 25 r1pval ⊢ ( ( ( 𝐵 × 𝐴 ) ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) → ( ( 𝐵 × 𝐴 ) 𝐸 𝐷 ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
40 38 15 39 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) 𝐸 𝐷 ) = ( ( 𝐵 × 𝐴 ) ( -g ‘ 𝑃 ) ( ( ( 𝐵 × 𝐴 ) ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
41 4 1 2 11 16 25 r1pval ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) → ( 𝐴 𝐸 𝐷 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
42 6 15 41 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐷 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
43 42 oveq2d ⊢ ( 𝜑 → ( 𝐵 × ( 𝐴 𝐸 𝐷 ) ) = ( 𝐵 × ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
44 37 40 43 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) 𝐸 𝐷 ) = ( 𝐵 × ( 𝐴 𝐸 𝐷 ) ) )