Proof of Theorem r1pid2OLD
| Step | Hyp | Ref
| Expression |
| 1 | | r1pid2OLD.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 2 | 1 | idomringd 20728 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 3 | | r1pid2OLD.p |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 4 | | r1pid2OLD.q |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑁) |
| 5 | | r1padd1.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
| 6 | | r1padd1.u |
. . . . . . . 8
⊢ 𝑈 = (Base‘𝑃) |
| 7 | | r1padd1.n |
. . . . . . . 8
⊢ 𝑁 =
(Unic1p‘𝑅) |
| 8 | | eqid 2737 |
. . . . . . . 8
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
| 9 | | r1padd1.e |
. . . . . . . 8
⊢ 𝐸 = (rem1p‘𝑅) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑃) = (+g‘𝑃) |
| 12 | 5, 6, 7, 8, 9, 10,
11 | r1pid 26200 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁) → 𝐴 = (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵))) |
| 13 | 2, 3, 4, 12 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 𝐴 = (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵))) |
| 14 | 13 | eqeq2d 2748 |
. . . . 5
⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐴𝐸𝐵) = (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)))) |
| 15 | | eqcom 2744 |
. . . . 5
⊢ ((((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = (𝐴𝐸𝐵) ↔ (𝐴𝐸𝐵) = (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵))) |
| 16 | 14, 15 | bitr4di 289 |
. . . 4
⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = (𝐴𝐸𝐵))) |
| 17 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 18 | 5 | ply1ring 22249 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 19 | 2, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Ring) |
| 20 | 19 | ringgrpd 20239 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Grp) |
| 21 | 9, 5, 6, 7 | r1pcl 26198 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁) → (𝐴𝐸𝐵) ∈ 𝑈) |
| 22 | 2, 3, 4, 21 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐸𝐵) ∈ 𝑈) |
| 23 | 6, 11, 17, 20, 22 | grplidd 18987 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑃)(+g‘𝑃)(𝐴𝐸𝐵)) = (𝐴𝐸𝐵)) |
| 24 | 23 | eqeq2d 2748 |
. . . 4
⊢ (𝜑 → ((((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = ((0g‘𝑃)(+g‘𝑃)(𝐴𝐸𝐵)) ↔ (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = (𝐴𝐸𝐵))) |
| 25 | 8, 5, 6, 7 | q1pcl 26196 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁) → (𝐴(quot1p‘𝑅)𝐵) ∈ 𝑈) |
| 26 | 2, 3, 4, 25 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐴(quot1p‘𝑅)𝐵) ∈ 𝑈) |
| 27 | 5, 6, 7 | uc1pcl 26183 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑁 → 𝐵 ∈ 𝑈) |
| 28 | 4, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| 29 | 6, 10, 19, 26, 28 | ringcld 20257 |
. . . . 5
⊢ (𝜑 → ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) ∈ 𝑈) |
| 30 | 6, 17 | ring0cl 20264 |
. . . . . 6
⊢ (𝑃 ∈ Ring →
(0g‘𝑃)
∈ 𝑈) |
| 31 | 2, 18, 30 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (0g‘𝑃) ∈ 𝑈) |
| 32 | 6, 11 | grprcan 18991 |
. . . . 5
⊢ ((𝑃 ∈ Grp ∧ (((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) ∈ 𝑈 ∧ (0g‘𝑃) ∈ 𝑈 ∧ (𝐴𝐸𝐵) ∈ 𝑈)) → ((((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = ((0g‘𝑃)(+g‘𝑃)(𝐴𝐸𝐵)) ↔ ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) = (0g‘𝑃))) |
| 33 | 20, 29, 31, 22, 32 | syl13anc 1374 |
. . . 4
⊢ (𝜑 → ((((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)(+g‘𝑃)(𝐴𝐸𝐵)) = ((0g‘𝑃)(+g‘𝑃)(𝐴𝐸𝐵)) ↔ ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) = (0g‘𝑃))) |
| 34 | 16, 24, 33 | 3bitr2d 307 |
. . 3
⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) = (0g‘𝑃))) |
| 35 | | isidom 20725 |
. . . . . . . 8
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 36 | 1, 35 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 37 | 36 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 38 | 5 | ply1crng 22200 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
| 39 | 37, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ CRing) |
| 40 | 6, 10 | crngcom 20248 |
. . . . 5
⊢ ((𝑃 ∈ CRing ∧ 𝐵 ∈ 𝑈 ∧ (𝐴(quot1p‘𝑅)𝐵) ∈ 𝑈) → (𝐵(.r‘𝑃)(𝐴(quot1p‘𝑅)𝐵)) = ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)) |
| 41 | 39, 28, 26, 40 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐵(.r‘𝑃)(𝐴(quot1p‘𝑅)𝐵)) = ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵)) |
| 42 | 41 | eqeq1d 2739 |
. . 3
⊢ (𝜑 → ((𝐵(.r‘𝑃)(𝐴(quot1p‘𝑅)𝐵)) = (0g‘𝑃) ↔ ((𝐴(quot1p‘𝑅)𝐵)(.r‘𝑃)𝐵) = (0g‘𝑃))) |
| 43 | 1 | idomdomd 20726 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Domn) |
| 44 | 5 | ply1domn 26163 |
. . . . . 6
⊢ (𝑅 ∈ Domn → 𝑃 ∈ Domn) |
| 45 | 43, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Domn) |
| 46 | 5, 17, 7 | uc1pn0 26185 |
. . . . . 6
⊢ (𝐵 ∈ 𝑁 → 𝐵 ≠ (0g‘𝑃)) |
| 47 | 4, 46 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ (0g‘𝑃)) |
| 48 | | eqid 2737 |
. . . . . 6
⊢
(RLReg‘𝑃) =
(RLReg‘𝑃) |
| 49 | 6, 48, 17 | domnrrg 20713 |
. . . . 5
⊢ ((𝑃 ∈ Domn ∧ 𝐵 ∈ 𝑈 ∧ 𝐵 ≠ (0g‘𝑃)) → 𝐵 ∈ (RLReg‘𝑃)) |
| 50 | 45, 28, 47, 49 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (RLReg‘𝑃)) |
| 51 | 48, 6, 10, 17 | rrgeq0 20700 |
. . . 4
⊢ ((𝑃 ∈ Ring ∧ 𝐵 ∈ (RLReg‘𝑃) ∧ (𝐴(quot1p‘𝑅)𝐵) ∈ 𝑈) → ((𝐵(.r‘𝑃)(𝐴(quot1p‘𝑅)𝐵)) = (0g‘𝑃) ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 52 | 19, 50, 26, 51 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝐵(.r‘𝑃)(𝐴(quot1p‘𝑅)𝐵)) = (0g‘𝑃) ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 53 | 34, 42, 52 | 3bitr2d 307 |
. 2
⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 54 | 6, 10, 17, 19, 28 | ringlzd 20292 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑃)(.r‘𝑃)𝐵) = (0g‘𝑃)) |
| 55 | 54 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵)) = (𝐴(-g‘𝑃)(0g‘𝑃))) |
| 56 | | eqid 2737 |
. . . . . . . 8
⊢
(-g‘𝑃) = (-g‘𝑃) |
| 57 | 6, 17, 56 | grpsubid1 19043 |
. . . . . . 7
⊢ ((𝑃 ∈ Grp ∧ 𝐴 ∈ 𝑈) → (𝐴(-g‘𝑃)(0g‘𝑃)) = 𝐴) |
| 58 | 20, 3, 57 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴(-g‘𝑃)(0g‘𝑃)) = 𝐴) |
| 59 | 55, 58 | eqtr2d 2778 |
. . . . 5
⊢ (𝜑 → 𝐴 = (𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) |
| 60 | 59 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐴) = (𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵)))) |
| 61 | 60 | breq1d 5153 |
. . 3
⊢ (𝜑 → ((𝐷‘𝐴) < (𝐷‘𝐵) ↔ (𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) < (𝐷‘𝐵))) |
| 62 | 31 | biantrurd 532 |
. . 3
⊢ (𝜑 → ((𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) < (𝐷‘𝐵) ↔ ((0g‘𝑃) ∈ 𝑈 ∧ (𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) < (𝐷‘𝐵)))) |
| 63 | | r1pid2OLD.d |
. . . . 5
⊢ 𝐷 = (deg1‘𝑅) |
| 64 | 8, 5, 6, 63, 56, 10, 7 | q1peqb 26195 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁) → (((0g‘𝑃) ∈ 𝑈 ∧ (𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) < (𝐷‘𝐵)) ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 65 | 2, 3, 4, 64 | syl3anc 1373 |
. . 3
⊢ (𝜑 →
(((0g‘𝑃)
∈ 𝑈 ∧ (𝐷‘(𝐴(-g‘𝑃)((0g‘𝑃)(.r‘𝑃)𝐵))) < (𝐷‘𝐵)) ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 66 | 61, 62, 65 | 3bitrd 305 |
. 2
⊢ (𝜑 → ((𝐷‘𝐴) < (𝐷‘𝐵) ↔ (𝐴(quot1p‘𝑅)𝐵) = (0g‘𝑃))) |
| 67 | 53, 66 | bitr4d 282 |
1
⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵))) |