Metamath Proof Explorer

Theorem q1pdir

Description: Distribution of univariate polynomial quotient over addition. (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 ⊢ ( 𝜑 → 𝐶 ∈ 𝑁 )
q1pdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
q1pdir.1 ⊢ + = ( +g ‘ 𝑃 )
Assertion q1pdir ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) )

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 q1pdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
9 q1pdir.1 ⊢ + = ( +g ‘ 𝑃 )
10 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11 5 10 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
12 11 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
13 2 9 12 6 8 grpcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ 𝑈 )
14 4 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( 𝐴 / 𝐶 ) ∈ 𝑈 )
15 5 6 7 14 syl3anc ⊢ ( 𝜑 → ( 𝐴 / 𝐶 ) ∈ 𝑈 )
16 4 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( 𝐵 / 𝐶 ) ∈ 𝑈 )
17 5 8 7 16 syl3anc ⊢ ( 𝜑 → ( 𝐵 / 𝐶 ) ∈ 𝑈 )
18 2 9 12 15 17 grpcld ⊢ ( 𝜑 → ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ∈ 𝑈 )
19 1 2 3 uc1pcl ⊢ ( 𝐶 ∈ 𝑁 → 𝐶 ∈ 𝑈 )
20 7 19 syl ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
21 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
22 2 9 21 ringdir ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝐴 / 𝐶 ) ∈ 𝑈 ∧ ( 𝐵 / 𝐶 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) ) → ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) = ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) + ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
23 11 15 17 20 22 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) = ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) + ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
24 23 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) + ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
25 11 ringabld ⊢ ( 𝜑 → 𝑃 ∈ Abel )
26 2 21 11 15 20 ringcld ⊢ ( 𝜑 → ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 )
27 2 21 11 17 20 ringcld ⊢ ( 𝜑 → ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 )
28 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
29 2 9 28 ablsub4 ⊢ ( ( 𝑃 ∈ Abel ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ∧ ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 ∧ ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ∈ 𝑈 ) ) → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) + ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) + ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
30 25 6 8 26 27 29 syl122anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) + ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) + ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
31 24 30 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) + ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) + ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ) )
33 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
34 eqid ⊢ ( rem1p ‘ 𝑅 ) = ( rem1p ‘ 𝑅 )
35 34 1 2 4 21 28 r1pval ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
36 6 20 35 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
37 34 1 2 3 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 )
38 5 6 7 37 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 )
39 36 38 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
40 34 1 2 4 21 28 r1pval ⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
41 8 20 40 syl2anc ⊢ ( 𝜑 → ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) = ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) )
42 34 1 2 3 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 )
43 5 8 7 42 syl3anc ⊢ ( 𝜑 → ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) ∈ 𝑈 )
44 41 43 eqeltrrd ⊢ ( 𝜑 → ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ∈ 𝑈 )
45 33 1 2 deg1xrcl ⊢ ( 𝐶 ∈ 𝑈 → ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ∈ ℝ* )
46 20 45 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ∈ ℝ* )
47 36 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
48 34 1 2 3 33 r1pdeglt ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
49 5 6 7 48 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
50 47 49 eqbrtrrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
51 41 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) )
52 34 1 2 3 33 r1pdeglt ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
53 5 8 7 52 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 ( rem1p ‘ 𝑅 ) 𝐶 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
54 51 53 eqbrtrrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
55 1 33 5 2 9 39 44 46 50 54 deg1addlt ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) + ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 / 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
56 32 55 eqbrtrd ⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) )
57 4 1 2 33 28 21 3 q1peqb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 + 𝐵 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) → ( ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ∈ 𝑈 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ) ↔ ( ( 𝐴 + 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ) )
58 57 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 + 𝐵 ) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁 ) ∧ ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ∈ 𝑈 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) ( .r ‘ 𝑃 ) 𝐶 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐶 ) ) ) → ( ( 𝐴 + 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) )
59 5 13 7 18 56 58 syl32anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) + ( 𝐵 / 𝐶 ) ) )