Proof of Theorem r1padd1
| Step | Hyp | Ref
| Expression |
| 1 | | r1padd1.1 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷)) |
| 2 | | r1padd1.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 3 | | r1padd1.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑁) |
| 4 | | r1padd1.p |
. . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝑅) |
| 5 | | r1padd1.u |
. . . . . . . . 9
⊢ 𝑈 = (Base‘𝑃) |
| 6 | | r1padd1.n |
. . . . . . . . 9
⊢ 𝑁 =
(Unic1p‘𝑅) |
| 7 | 4, 5, 6 | uc1pcl 26183 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑁 → 𝐷 ∈ 𝑈) |
| 8 | 3, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
| 9 | | r1padd1.e |
. . . . . . . 8
⊢ 𝐸 = (rem1p‘𝑅) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
(-g‘𝑃) = (-g‘𝑃) |
| 13 | 9, 4, 5, 10, 11, 12 | r1pval 26197 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈) → (𝐴𝐸𝐷) = (𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 14 | 2, 8, 13 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 15 | | r1padd1.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| 16 | 9, 4, 5, 10, 11, 12 | r1pval 26197 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈) → (𝐵𝐸𝐷) = (𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 17 | 15, 8, 16 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐵𝐸𝐷) = (𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 18 | 1, 14, 17 | 3eqtr3d 2785 |
. . . . 5
⊢ (𝜑 → (𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = (𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 19 | 18 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶) = ((𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 20 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑃) = (invg‘𝑃) |
| 21 | | r1padd1.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 22 | 4 | ply1ring 22249 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Ring) |
| 24 | 10, 4, 5, 6 | q1pcl 26196 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁) → (𝐴(quot1p‘𝑅)𝐷) ∈ 𝑈) |
| 25 | 21, 2, 3, 24 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐴(quot1p‘𝑅)𝐷) ∈ 𝑈) |
| 26 | 5, 11, 20, 23, 25, 8 | ringmneg1 20301 |
. . . . . 6
⊢ (𝜑 →
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷) = ((invg‘𝑃)‘((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 27 | 26 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐶) +
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷)) = ((𝐴 + 𝐶) +
((invg‘𝑃)‘((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 28 | | r1padd1.2 |
. . . . . . 7
⊢ + =
(+g‘𝑃) |
| 29 | 23 | ringgrpd 20239 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Grp) |
| 30 | | r1padd1.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
| 31 | 5, 28, 29, 2, 30 | grpcld 18965 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐶) ∈ 𝑈) |
| 32 | 5, 11, 23, 25, 8 | ringcld 20257 |
. . . . . 6
⊢ (𝜑 → ((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈) |
| 33 | 5, 28, 20, 12 | grpsubval 19003 |
. . . . . 6
⊢ (((𝐴 + 𝐶) ∈ 𝑈 ∧ ((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈) → ((𝐴 + 𝐶)(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐴 + 𝐶) +
((invg‘𝑃)‘((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 34 | 31, 32, 33 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐶)(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐴 + 𝐶) +
((invg‘𝑃)‘((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 35 | 23 | ringabld 20280 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Abel) |
| 36 | 5, 28, 12 | abladdsub 19830 |
. . . . . 6
⊢ ((𝑃 ∈ Abel ∧ (𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ∧ ((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈)) → ((𝐴 + 𝐶)(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 37 | 35, 2, 30, 32, 36 | syl13anc 1374 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐶)(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 38 | 27, 34, 37 | 3eqtr2d 2783 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐶) +
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷)) = ((𝐴(-g‘𝑃)((𝐴(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 39 | 10, 4, 5, 6 | q1pcl 26196 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁) → (𝐵(quot1p‘𝑅)𝐷) ∈ 𝑈) |
| 40 | 21, 15, 3, 39 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐵(quot1p‘𝑅)𝐷) ∈ 𝑈) |
| 41 | 5, 11, 20, 23, 40, 8 | ringmneg1 20301 |
. . . . . 6
⊢ (𝜑 →
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷) = ((invg‘𝑃)‘((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷))) |
| 42 | 41 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((𝐵 + 𝐶) +
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷)) = ((𝐵 + 𝐶) +
((invg‘𝑃)‘((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 43 | 5, 28, 29, 15, 30 | grpcld 18965 |
. . . . . 6
⊢ (𝜑 → (𝐵 + 𝐶) ∈ 𝑈) |
| 44 | 5, 11, 23, 40, 8 | ringcld 20257 |
. . . . . 6
⊢ (𝜑 → ((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈) |
| 45 | 5, 28, 20, 12 | grpsubval 19003 |
. . . . . 6
⊢ (((𝐵 + 𝐶) ∈ 𝑈 ∧ ((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈) → ((𝐵 + 𝐶)(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐵 + 𝐶) +
((invg‘𝑃)‘((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 46 | 43, 44, 45 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝐵 + 𝐶)(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐵 + 𝐶) +
((invg‘𝑃)‘((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)))) |
| 47 | 5, 28, 12 | abladdsub 19830 |
. . . . . 6
⊢ ((𝑃 ∈ Abel ∧ (𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ∧ ((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷) ∈ 𝑈)) → ((𝐵 + 𝐶)(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 48 | 35, 15, 30, 44, 47 | syl13anc 1374 |
. . . . 5
⊢ (𝜑 → ((𝐵 + 𝐶)(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) = ((𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 49 | 42, 46, 48 | 3eqtr2d 2783 |
. . . 4
⊢ (𝜑 → ((𝐵 + 𝐶) +
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷)) = ((𝐵(-g‘𝑃)((𝐵(quot1p‘𝑅)𝐷)(.r‘𝑃)𝐷)) + 𝐶)) |
| 50 | 19, 38, 49 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐶) +
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷)) = ((𝐵 + 𝐶) +
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷))) |
| 51 | 50 | oveq1d 7446 |
. 2
⊢ (𝜑 → (((𝐴 + 𝐶) +
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷))𝐸𝐷) = (((𝐵 + 𝐶) +
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷))𝐸𝐷)) |
| 52 | 5, 20, 29, 25 | grpinvcld 19006 |
. . 3
⊢ (𝜑 →
((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷)) ∈ 𝑈) |
| 53 | 4, 5, 6, 9, 28, 11, 21, 31, 3, 52 | r1pcyc 33627 |
. 2
⊢ (𝜑 → (((𝐴 + 𝐶) +
(((invg‘𝑃)‘(𝐴(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷))𝐸𝐷) = ((𝐴 + 𝐶)𝐸𝐷)) |
| 54 | 5, 20, 29, 40 | grpinvcld 19006 |
. . 3
⊢ (𝜑 →
((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷)) ∈ 𝑈) |
| 55 | 4, 5, 6, 9, 28, 11, 21, 43, 3, 54 | r1pcyc 33627 |
. 2
⊢ (𝜑 → (((𝐵 + 𝐶) +
(((invg‘𝑃)‘(𝐵(quot1p‘𝑅)𝐷))(.r‘𝑃)𝐷))𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) |
| 56 | 51, 53, 55 | 3eqtr3d 2785 |
1
⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) |