Step | Hyp | Ref
| Expression |
1 | | mxidlirred.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | mxidlirred.k |
. . 3
⊢ 𝐾 = (RSpan‘𝑅) |
3 | | mxidlirred.0 |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | | mxidlirred.m |
. . 3
⊢ 𝑀 = (𝐾‘{𝑋}) |
5 | | mxidlirred.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ PID) |
6 | | df-pid 21222 |
. . . . . 6
⊢ PID =
(IDomn ∩ LPIR) |
7 | 5, 6 | eleqtrdi 2838 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ (IDomn ∩ LPIR)) |
8 | 7 | elin1d 4194 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ IDomn) |
9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ IDomn) |
10 | | mxidlirred.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ∈ 𝐵) |
12 | | mxidlirred.y |
. . . 4
⊢ (𝜑 → 𝑋 ≠ 0 ) |
13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ≠ 0 ) |
14 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
15 | 1, 2, 3, 4, 9, 11,
13, 14 | mxidlirredi 33120 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑋 ∈ (Irred‘𝑅)) |
16 | | eqid 2727 |
. . . . . . . . . . 11
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
17 | | simplr 768 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑥 ∈ 𝐵) |
18 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑥 ∈ 𝐵) |
19 | 10 | ad8antr 739 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑋 ∈ 𝐵) |
20 | | eqid 2727 |
. . . . . . . . . . 11
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
21 | | eqid 2727 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
22 | 8 | idomringd 21244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) |
23 | 22 | ad4antr 731 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑅 ∈ Ring) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑅 ∈ Ring) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑅 ∈ Ring) |
26 | | simplr 768 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑡 ∈ 𝐵) |
27 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑋 = (𝑡(.r‘𝑅)𝑥)) |
28 | | simp-8r 791 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑋 ∈ (Irred‘𝑅)) |
29 | 27, 28 | eqeltrrd 2829 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝑡(.r‘𝑅)𝑥) ∈ (Irred‘𝑅)) |
30 | | eqid 2727 |
. . . . . . . . . . . . . 14
⊢
(Irred‘𝑅) =
(Irred‘𝑅) |
31 | 30, 1, 20, 21 | irredmul 20357 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ (𝑡(.r‘𝑅)𝑥) ∈ (Irred‘𝑅)) → (𝑡 ∈ (Unit‘𝑅) ∨ 𝑥 ∈ (Unit‘𝑅))) |
32 | 26, 18, 29, 31 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝑡 ∈ (Unit‘𝑅) ∨ 𝑥 ∈ (Unit‘𝑅))) |
33 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑘 = (𝐾‘{𝑥})) |
34 | 33 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑘 = (𝐾‘{𝑥})) |
35 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
36 | | annim 403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ⊆ 𝑘 ∧ ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)) ↔ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
37 | 35, 36 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (𝑀 ⊆ 𝑘 ∧ ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
38 | 37 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)) |
39 | | ioran 982 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑘 = 𝑀 ∨ 𝑘 = 𝐵) ↔ (¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵)) |
40 | 38, 39 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵)) |
41 | 40 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ 𝑘 = 𝐵) |
42 | 41 | neqned 2942 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ≠ 𝐵) |
43 | 42 | ad4antr 731 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑘 ≠ 𝐵) |
44 | 34, 43 | eqnetrrd 3004 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝐾‘{𝑥}) ≠ 𝐵) |
45 | 44 | neneqd 2940 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → ¬ (𝐾‘{𝑥}) = 𝐵) |
46 | | eqid 2727 |
. . . . . . . . . . . . . 14
⊢ (𝐾‘{𝑥}) = (𝐾‘{𝑥}) |
47 | 8 | ad8antr 739 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑅 ∈ IDomn) |
48 | 20, 2, 46, 1, 18, 47 | unitpidl1 33075 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → ((𝐾‘{𝑥}) = 𝐵 ↔ 𝑥 ∈ (Unit‘𝑅))) |
49 | 45, 48 | mtbid 324 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → ¬ 𝑥 ∈ (Unit‘𝑅)) |
50 | 32, 49 | olcnd 876 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑡 ∈ (Unit‘𝑅)) |
51 | 27 | eqcomd 2733 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝑡(.r‘𝑅)𝑥) = 𝑋) |
52 | 1, 2, 16, 18, 19, 20, 21, 25, 50, 51 | dvdsruassoi 33028 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝑥(∥r‘𝑅)𝑋 ∧ 𝑋(∥r‘𝑅)𝑥)) |
53 | 1, 2, 16, 18, 19, 25 | rspsnasso 33031 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → ((𝑥(∥r‘𝑅)𝑋 ∧ 𝑋(∥r‘𝑅)𝑥) ↔ (𝐾‘{𝑋}) = (𝐾‘{𝑥}))) |
54 | 52, 53 | mpbid 231 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝐾‘{𝑋}) = (𝐾‘{𝑥})) |
55 | 54, 34 | eqtr4d 2770 |
. . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → (𝐾‘{𝑋}) = 𝑘) |
56 | 4, 55 | eqtr2id 2780 |
. . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑘 = 𝑀) |
57 | 40 | simpld 494 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ¬ 𝑘 = 𝑀) |
58 | 57 | ad4antr 731 |
. . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → ¬ 𝑘 = 𝑀) |
59 | 56, 58 | pm2.21dd 194 |
. . . . . 6
⊢
(((((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) ∧ 𝑡 ∈ 𝐵) ∧ 𝑋 = (𝑡(.r‘𝑅)𝑥)) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
60 | 37 | simpld 494 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑀 ⊆ 𝑘) |
61 | 60 | ad2antrr 725 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑀 ⊆ 𝑘) |
62 | 10 | snssd 4808 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑋} ⊆ 𝐵) |
63 | 2, 1 | rspssid 21121 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ {𝑋} ⊆ 𝐵) → {𝑋} ⊆ (𝐾‘{𝑋})) |
64 | 22, 62, 63 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋})) |
65 | 64, 4 | sseqtrrdi 4029 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑋} ⊆ 𝑀) |
66 | | snssg 4783 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → (𝑋 ∈ 𝑀 ↔ {𝑋} ⊆ 𝑀)) |
67 | 66 | biimpar 477 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐵 ∧ {𝑋} ⊆ 𝑀) → 𝑋 ∈ 𝑀) |
68 | 10, 65, 67 | syl2anc 583 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑀) |
69 | 68 | ad6antr 735 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ 𝑀) |
70 | 61, 69 | sseldd 3979 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ 𝑘) |
71 | 70, 33 | eleqtrd 2830 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑋 ∈ (𝐾‘{𝑥})) |
72 | 1, 21, 2 | rspsnel 33023 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑋 ∈ (𝐾‘{𝑥}) ↔ ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(.r‘𝑅)𝑥))) |
73 | 72 | biimpa 476 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑋 ∈ (𝐾‘{𝑥})) → ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(.r‘𝑅)𝑥)) |
74 | 24, 17, 71, 73 | syl21anc 837 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → ∃𝑡 ∈ 𝐵 𝑋 = (𝑡(.r‘𝑅)𝑥)) |
75 | 59, 74 | r19.29a 3157 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 = (𝐾‘{𝑥})) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
76 | | simplr 768 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ∈ (LIdeal‘𝑅)) |
77 | 7 | elin2d 4195 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ LPIR) |
78 | | eqid 2727 |
. . . . . . . . . . 11
⊢
(LPIdeal‘𝑅) =
(LPIdeal‘𝑅) |
79 | | eqid 2727 |
. . . . . . . . . . 11
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
80 | 78, 79 | islpir 21207 |
. . . . . . . . . 10
⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧
(LIdeal‘𝑅) =
(LPIdeal‘𝑅))) |
81 | 80 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑅 ∈ LPIR →
(LIdeal‘𝑅) =
(LPIdeal‘𝑅)) |
82 | 77, 81 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (LIdeal‘𝑅) = (LPIdeal‘𝑅)) |
83 | 82 | ad4antr 731 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → (LIdeal‘𝑅) = (LPIdeal‘𝑅)) |
84 | 76, 83 | eleqtrd 2830 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑘 ∈ (LPIdeal‘𝑅)) |
85 | 78, 2, 1 | islpidl 21204 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑘 ∈ (LPIdeal‘𝑅) ↔ ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥}))) |
86 | 85 | biimpa 476 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LPIdeal‘𝑅)) → ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥})) |
87 | 23, 84, 86 | syl2anc 583 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → ∃𝑥 ∈ 𝐵 𝑘 = (𝐾‘{𝑥})) |
88 | 75, 87 | r19.29a 3157 |
. . . 4
⊢
(((((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
89 | | mxidlirred.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) |
90 | 89 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) |
91 | 30, 20 | irrednu 20353 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (Irred‘𝑅) → ¬ 𝑋 ∈ (Unit‘𝑅)) |
92 | 91 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → ¬ 𝑋 ∈ (Unit‘𝑅)) |
93 | 20, 2, 4, 1, 10, 8 | unitpidl1 33075 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 = 𝐵 ↔ 𝑋 ∈ (Unit‘𝑅))) |
94 | 93 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → (𝑀 = 𝐵 ↔ 𝑋 ∈ (Unit‘𝑅))) |
95 | 94 | necon3abid 2972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → (𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ (Unit‘𝑅))) |
96 | 92, 95 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → 𝑀 ≠ 𝐵) |
97 | 96 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) |
98 | 90, 97 | jca 511 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵)) |
99 | 1 | ismxidl 33111 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))) |
100 | 22, 99 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))) |
101 | | df-3an 1087 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) ↔ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))) |
102 | 100, 101 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))) |
103 | 102 | notbid 318 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝑀 ∈ (MaxIdeal‘𝑅) ↔ ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))))) |
104 | 103 | biimpa 476 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))) |
105 | 104 | adantlr 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ((𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵) ∧ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)))) |
106 | 98, 105 | mpnanrd 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
107 | | rexnal 3095 |
. . . . 5
⊢
(∃𝑘 ∈
(LIdeal‘𝑅) ¬
(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵)) ↔ ¬ ∀𝑘 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
108 | 106, 107 | sylibr 233 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → ∃𝑘 ∈ (LIdeal‘𝑅) ¬ (𝑀 ⊆ 𝑘 → (𝑘 = 𝑀 ∨ 𝑘 = 𝐵))) |
109 | 88, 108 | r19.29a 3157 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) ∧ ¬ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
110 | 109 | pm2.18da 799 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (Irred‘𝑅)) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
111 | 15, 110 | impbida 800 |
1
⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ 𝑋 ∈ (Irred‘𝑅))) |