Proof of Theorem q1pdir
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | q1pdir.r | . 2
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 2 |  | r1padd1.u | . . 3
⊢ 𝑈 = (Base‘𝑃) | 
| 3 |  | q1pdir.1 | . . 3
⊢  + =
(+g‘𝑃) | 
| 4 |  | r1padd1.p | . . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) | 
| 5 | 4 | ply1ring 22250 | . . . . 5
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 6 | 1, 5 | syl 17 | . . . 4
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 7 | 6 | ringgrpd 20240 | . . 3
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 8 |  | q1pdir.a | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝑈) | 
| 9 |  | q1pdir.b | . . 3
⊢ (𝜑 → 𝐵 ∈ 𝑈) | 
| 10 | 2, 3, 7, 8, 9 | grpcld 18966 | . 2
⊢ (𝜑 → (𝐴 + 𝐵) ∈ 𝑈) | 
| 11 |  | q1pdir.c | . 2
⊢ (𝜑 → 𝐶 ∈ 𝑁) | 
| 12 |  | q1pdir.d | . . . . 5
⊢  / =
(quot1p‘𝑅) | 
| 13 |  | r1padd1.n | . . . . 5
⊢ 𝑁 =
(Unic1p‘𝑅) | 
| 14 | 12, 4, 2, 13 | q1pcl 26197 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → (𝐴 / 𝐶) ∈ 𝑈) | 
| 15 | 1, 8, 11, 14 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝐴 / 𝐶) ∈ 𝑈) | 
| 16 | 12, 4, 2, 13 | q1pcl 26197 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → (𝐵 / 𝐶) ∈ 𝑈) | 
| 17 | 1, 9, 11, 16 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝐵 / 𝐶) ∈ 𝑈) | 
| 18 | 2, 3, 7, 15, 17 | grpcld 18966 | . 2
⊢ (𝜑 → ((𝐴 / 𝐶) + (𝐵 / 𝐶)) ∈ 𝑈) | 
| 19 | 4, 2, 13 | uc1pcl 26184 | . . . . . . . 8
⊢ (𝐶 ∈ 𝑁 → 𝐶 ∈ 𝑈) | 
| 20 | 11, 19 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑈) | 
| 21 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘𝑃) = (.r‘𝑃) | 
| 22 | 2, 3, 21 | ringdir 20260 | . . . . . . 7
⊢ ((𝑃 ∈ Ring ∧ ((𝐴 / 𝐶) ∈ 𝑈 ∧ (𝐵 / 𝐶) ∈ 𝑈 ∧ 𝐶 ∈ 𝑈)) → (((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶) = (((𝐴 / 𝐶)(.r‘𝑃)𝐶) + ((𝐵 / 𝐶)(.r‘𝑃)𝐶))) | 
| 23 | 6, 15, 17, 20, 22 | syl13anc 1373 | . . . . . 6
⊢ (𝜑 → (((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶) = (((𝐴 / 𝐶)(.r‘𝑃)𝐶) + ((𝐵 / 𝐶)(.r‘𝑃)𝐶))) | 
| 24 | 23 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶)) = ((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶)(.r‘𝑃)𝐶) + ((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 25 | 6 | ringabld 20281 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ Abel) | 
| 26 | 2, 21, 6, 15, 20 | ringcld 20258 | . . . . . 6
⊢ (𝜑 → ((𝐴 / 𝐶)(.r‘𝑃)𝐶) ∈ 𝑈) | 
| 27 | 2, 21, 6, 17, 20 | ringcld 20258 | . . . . . 6
⊢ (𝜑 → ((𝐵 / 𝐶)(.r‘𝑃)𝐶) ∈ 𝑈) | 
| 28 |  | eqid 2736 | . . . . . . 7
⊢
(-g‘𝑃) = (-g‘𝑃) | 
| 29 | 2, 3, 28 | ablsub4 19829 | . . . . . 6
⊢ ((𝑃 ∈ Abel ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) ∧ (((𝐴 / 𝐶)(.r‘𝑃)𝐶) ∈ 𝑈 ∧ ((𝐵 / 𝐶)(.r‘𝑃)𝐶) ∈ 𝑈)) → ((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶)(.r‘𝑃)𝐶) + ((𝐵 / 𝐶)(.r‘𝑃)𝐶))) = ((𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) + (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 30 | 25, 8, 9, 26, 27, 29 | syl122anc 1380 | . . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶)(.r‘𝑃)𝐶) + ((𝐵 / 𝐶)(.r‘𝑃)𝐶))) = ((𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) + (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 31 | 24, 30 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶)) = ((𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) + (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 32 | 31 | fveq2d 6909 | . . 3
⊢ (𝜑 →
((deg1‘𝑅)‘((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶))) = ((deg1‘𝑅)‘((𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) + (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶))))) | 
| 33 |  | eqid 2736 | . . . 4
⊢
(deg1‘𝑅) = (deg1‘𝑅) | 
| 34 |  | eqid 2736 | . . . . . . 7
⊢
(rem1p‘𝑅) = (rem1p‘𝑅) | 
| 35 | 34, 4, 2, 12, 21, 28 | r1pval 26198 | . . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈) → (𝐴(rem1p‘𝑅)𝐶) = (𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶))) | 
| 36 | 8, 20, 35 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴(rem1p‘𝑅)𝐶) = (𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶))) | 
| 37 | 34, 4, 2, 13 | r1pcl 26199 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → (𝐴(rem1p‘𝑅)𝐶) ∈ 𝑈) | 
| 38 | 1, 8, 11, 37 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐴(rem1p‘𝑅)𝐶) ∈ 𝑈) | 
| 39 | 36, 38 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) ∈ 𝑈) | 
| 40 | 34, 4, 2, 12, 21, 28 | r1pval 26198 | . . . . . 6
⊢ ((𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈) → (𝐵(rem1p‘𝑅)𝐶) = (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶))) | 
| 41 | 9, 20, 40 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐵(rem1p‘𝑅)𝐶) = (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶))) | 
| 42 | 34, 4, 2, 13 | r1pcl 26199 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → (𝐵(rem1p‘𝑅)𝐶) ∈ 𝑈) | 
| 43 | 1, 9, 11, 42 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐵(rem1p‘𝑅)𝐶) ∈ 𝑈) | 
| 44 | 41, 43 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)) ∈ 𝑈) | 
| 45 | 33, 4, 2 | deg1xrcl 26122 | . . . . 5
⊢ (𝐶 ∈ 𝑈 → ((deg1‘𝑅)‘𝐶) ∈
ℝ*) | 
| 46 | 20, 45 | syl 17 | . . . 4
⊢ (𝜑 →
((deg1‘𝑅)‘𝐶) ∈
ℝ*) | 
| 47 | 36 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐴(rem1p‘𝑅)𝐶)) = ((deg1‘𝑅)‘(𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 48 | 34, 4, 2, 13, 33 | r1pdeglt 26200 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → ((deg1‘𝑅)‘(𝐴(rem1p‘𝑅)𝐶)) < ((deg1‘𝑅)‘𝐶)) | 
| 49 | 1, 8, 11, 48 | syl3anc 1372 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐴(rem1p‘𝑅)𝐶)) < ((deg1‘𝑅)‘𝐶)) | 
| 50 | 47, 49 | eqbrtrrd 5166 | . . . 4
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶))) < ((deg1‘𝑅)‘𝐶)) | 
| 51 | 41 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐵(rem1p‘𝑅)𝐶)) = ((deg1‘𝑅)‘(𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) | 
| 52 | 34, 4, 2, 13, 33 | r1pdeglt 26200 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → ((deg1‘𝑅)‘(𝐵(rem1p‘𝑅)𝐶)) < ((deg1‘𝑅)‘𝐶)) | 
| 53 | 1, 9, 11, 52 | syl3anc 1372 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐵(rem1p‘𝑅)𝐶)) < ((deg1‘𝑅)‘𝐶)) | 
| 54 | 51, 53 | eqbrtrrd 5166 | . . . 4
⊢ (𝜑 →
((deg1‘𝑅)‘(𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶))) < ((deg1‘𝑅)‘𝐶)) | 
| 55 | 4, 33, 1, 2, 3, 39,
44, 46, 50, 54 | deg1addlt 33621 | . . 3
⊢ (𝜑 →
((deg1‘𝑅)‘((𝐴(-g‘𝑃)((𝐴 / 𝐶)(.r‘𝑃)𝐶)) + (𝐵(-g‘𝑃)((𝐵 / 𝐶)(.r‘𝑃)𝐶)))) < ((deg1‘𝑅)‘𝐶)) | 
| 56 | 32, 55 | eqbrtrd 5164 | . 2
⊢ (𝜑 →
((deg1‘𝑅)‘((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶))) < ((deg1‘𝑅)‘𝐶)) | 
| 57 | 12, 4, 2, 33, 28, 21, 13 | q1peqb 26196 | . . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐴 + 𝐵) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) → ((((𝐴 / 𝐶) + (𝐵 / 𝐶)) ∈ 𝑈 ∧ ((deg1‘𝑅)‘((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶))) < ((deg1‘𝑅)‘𝐶)) ↔ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))) | 
| 58 | 57 | biimpa 476 | . 2
⊢ (((𝑅 ∈ Ring ∧ (𝐴 + 𝐵) ∈ 𝑈 ∧ 𝐶 ∈ 𝑁) ∧ (((𝐴 / 𝐶) + (𝐵 / 𝐶)) ∈ 𝑈 ∧ ((deg1‘𝑅)‘((𝐴 + 𝐵)(-g‘𝑃)(((𝐴 / 𝐶) + (𝐵 / 𝐶))(.r‘𝑃)𝐶))) < ((deg1‘𝑅)‘𝐶))) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | 
| 59 | 1, 10, 11, 18, 56, 58 | syl32anc 1379 | 1
⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) |