Step | Hyp | Ref
| Expression |
1 | | mxidlirredi.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | mxidlirredi.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
3 | 2 | idomringd 21257 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | mxidlirredi.1 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) |
5 | | mxidlirredi.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
6 | 5 | mxidlnr 33190 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) |
7 | 3, 4, 6 | syl2anc 583 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ 𝐵) |
8 | | eqid 2728 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
9 | | mxidlirredi.k |
. . . . . 6
⊢ 𝐾 = (RSpan‘𝑅) |
10 | | mxidlirredi.m |
. . . . . 6
⊢ 𝑀 = (𝐾‘{𝑋}) |
11 | 8, 9, 10, 5, 1, 2 | unitpidl1 33152 |
. . . . 5
⊢ (𝜑 → (𝑀 = 𝐵 ↔ 𝑋 ∈ (Unit‘𝑅))) |
12 | 11 | necon3abid 2974 |
. . . 4
⊢ (𝜑 → (𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ (Unit‘𝑅))) |
13 | 7, 12 | mpbid 231 |
. . 3
⊢ (𝜑 → ¬ 𝑋 ∈ (Unit‘𝑅)) |
14 | 1, 13 | eldifd 3958 |
. 2
⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ (Unit‘𝑅))) |
15 | 3 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑅 ∈ Ring) |
16 | 4 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
17 | | simplr 768 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) |
18 | 17 | eldifad 3959 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑔 ∈ 𝐵) |
19 | 18 | snssd 4813 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → {𝑔} ⊆ 𝐵) |
20 | | eqid 2728 |
. . . . . . . . . 10
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
21 | 9, 5, 20 | rspcl 21131 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ {𝑔} ⊆ 𝐵) → (𝐾‘{𝑔}) ∈ (LIdeal‘𝑅)) |
22 | 15, 19, 21 | syl2anc 583 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → (𝐾‘{𝑔}) ∈ (LIdeal‘𝑅)) |
23 | 3 | ad4antr 731 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → 𝑅 ∈ Ring) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑅 ∈ Ring) |
25 | | simp-5r 785 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) |
26 | 25 | eldifad 3959 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑔 ∈ 𝐵) |
27 | | eqid 2728 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
28 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑞 ∈ 𝐵) |
29 | | simp-6r 787 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) |
30 | 29 | eldifad 3959 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑓 ∈ 𝐵) |
31 | 5, 27, 24, 28, 30 | ringcld 20199 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → (𝑞(.r‘𝑅)𝑓) ∈ 𝐵) |
32 | | oveq1 7427 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑞(.r‘𝑅)𝑓) → (𝑦(.r‘𝑅)𝑔) = ((𝑞(.r‘𝑅)𝑓)(.r‘𝑅)𝑔)) |
33 | 32 | eqeq2d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑞(.r‘𝑅)𝑓) → (𝑥 = (𝑦(.r‘𝑅)𝑔) ↔ 𝑥 = ((𝑞(.r‘𝑅)𝑓)(.r‘𝑅)𝑔))) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) ∧ 𝑦 = (𝑞(.r‘𝑅)𝑓)) → (𝑥 = (𝑦(.r‘𝑅)𝑔) ↔ 𝑥 = ((𝑞(.r‘𝑅)𝑓)(.r‘𝑅)𝑔))) |
35 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → (𝑓(.r‘𝑅)𝑔) = 𝑋) |
36 | 35 | oveq2d 7436 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → (𝑞(.r‘𝑅)(𝑓(.r‘𝑅)𝑔)) = (𝑞(.r‘𝑅)𝑋)) |
37 | 5, 27, 24, 28, 30, 26 | ringassd 20197 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → ((𝑞(.r‘𝑅)𝑓)(.r‘𝑅)𝑔) = (𝑞(.r‘𝑅)(𝑓(.r‘𝑅)𝑔))) |
38 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑥 = (𝑞(.r‘𝑅)𝑋)) |
39 | 36, 37, 38 | 3eqtr4rd 2779 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑥 = ((𝑞(.r‘𝑅)𝑓)(.r‘𝑅)𝑔)) |
40 | 31, 34, 39 | rspcedvd 3611 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → ∃𝑦 ∈ 𝐵 𝑥 = (𝑦(.r‘𝑅)𝑔)) |
41 | 5, 27, 9 | rspsnel 33096 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ (𝐾‘{𝑔}) ↔ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦(.r‘𝑅)𝑔))) |
42 | 41 | biimpar 477 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵) ∧ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦(.r‘𝑅)𝑔)) → 𝑥 ∈ (𝐾‘{𝑔})) |
43 | 24, 26, 40, 42 | syl21anc 837 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) ∧ 𝑞 ∈ 𝐵) ∧ 𝑥 = (𝑞(.r‘𝑅)𝑋)) → 𝑥 ∈ (𝐾‘{𝑔})) |
44 | 1 | ad4antr 731 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → 𝑋 ∈ 𝐵) |
45 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → 𝑥 ∈ 𝑀) |
46 | 45, 10 | eleqtrdi 2839 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → 𝑥 ∈ (𝐾‘{𝑋})) |
47 | 5, 27, 9 | rspsnel 33096 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ (𝐾‘{𝑋}) ↔ ∃𝑞 ∈ 𝐵 𝑥 = (𝑞(.r‘𝑅)𝑋))) |
48 | 47 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ (𝐾‘{𝑋})) → ∃𝑞 ∈ 𝐵 𝑥 = (𝑞(.r‘𝑅)𝑋)) |
49 | 23, 44, 46, 48 | syl21anc 837 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → ∃𝑞 ∈ 𝐵 𝑥 = (𝑞(.r‘𝑅)𝑋)) |
50 | 43, 49 | r19.29a 3159 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑥 ∈ 𝑀) → 𝑥 ∈ (𝐾‘{𝑔})) |
51 | 50 | ex 412 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝐾‘{𝑔}))) |
52 | 51 | ssrdv 3986 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑀 ⊆ (𝐾‘{𝑔})) |
53 | 9, 5 | rspssid 21132 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ {𝑔} ⊆ 𝐵) → {𝑔} ⊆ (𝐾‘{𝑔})) |
54 | | vex 3475 |
. . . . . . . . . . . 12
⊢ 𝑔 ∈ V |
55 | 54 | snss 4790 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (𝐾‘{𝑔}) ↔ {𝑔} ⊆ (𝐾‘{𝑔})) |
56 | 53, 55 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ {𝑔} ⊆ 𝐵) → 𝑔 ∈ (𝐾‘{𝑔})) |
57 | 15, 19, 56 | syl2anc 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑔 ∈ (𝐾‘{𝑔})) |
58 | | df-idom 21232 |
. . . . . . . . . . . . . . 15
⊢ IDomn =
(CRing ∩ Domn) |
59 | 2, 58 | eleqtrdi 2839 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn)) |
60 | 59 | elin1d 4198 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ CRing) |
61 | 60 | ad6antr 735 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑅 ∈ CRing) |
62 | | simplr 768 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑟 ∈ 𝐵) |
63 | | simp-6r 787 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) |
64 | 63 | eldifad 3959 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑓 ∈ 𝐵) |
65 | | mxidlirredi.0 |
. . . . . . . . . . . . . 14
⊢ 0 =
(0g‘𝑅) |
66 | 18 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑔 ∈ 𝐵) |
67 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → 𝑔 = 0 ) |
68 | 67 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → (𝑓(.r‘𝑅)𝑔) = (𝑓(.r‘𝑅) 0 )) |
69 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → (𝑓(.r‘𝑅)𝑔) = 𝑋) |
70 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑅 ∈ Ring) |
71 | 70 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → 𝑅 ∈ Ring) |
72 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → 𝑓 ∈ 𝐵) |
73 | 5, 27, 65 | ringrz 20230 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵) → (𝑓(.r‘𝑅) 0 ) = 0 ) |
74 | 71, 72, 73 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → (𝑓(.r‘𝑅) 0 ) = 0 ) |
75 | 68, 69, 74 | 3eqtr3d 2776 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → 𝑋 = 0 ) |
76 | | mxidlirredi.y |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ≠ 0 ) |
77 | 76 | neneqd 2942 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ 𝑋 = 0 ) |
78 | 77 | ad7antr 737 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) ∧ 𝑔 = 0 ) → ¬ 𝑋 = 0 ) |
79 | 75, 78 | pm2.65da 816 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → ¬ 𝑔 = 0 ) |
80 | 79 | neqned 2944 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑔 ≠ 0 ) |
81 | | eldifsn 4791 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝐵 ∖ { 0 }) ↔ (𝑔 ∈ 𝐵 ∧ 𝑔 ≠ 0 )) |
82 | 66, 80, 81 | sylanbrc 582 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑔 ∈ (𝐵 ∖ { 0 })) |
83 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑅 ∈ Ring) |
84 | 5, 27, 83, 62, 64 | ringcld 20199 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑟(.r‘𝑅)𝑓) ∈ 𝐵) |
85 | | eqid 2728 |
. . . . . . . . . . . . . . . . 17
⊢
(1r‘𝑅) = (1r‘𝑅) |
86 | 5, 85 | ringidcl 20202 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
87 | 3, 86 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
88 | 87 | ad6antr 735 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (1r‘𝑅) ∈ 𝐵) |
89 | 2 | ad6antr 735 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑅 ∈ IDomn) |
90 | 5, 27, 85, 83, 66 | ringlidmd 20208 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → ((1r‘𝑅)(.r‘𝑅)𝑔) = 𝑔) |
91 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑔 = (𝑟(.r‘𝑅)𝑋)) |
92 | 5, 27, 83, 62, 64, 66 | ringassd 20197 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → ((𝑟(.r‘𝑅)𝑓)(.r‘𝑅)𝑔) = (𝑟(.r‘𝑅)(𝑓(.r‘𝑅)𝑔))) |
93 | | simp-4r 783 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑓(.r‘𝑅)𝑔) = 𝑋) |
94 | 93 | oveq2d 7436 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑟(.r‘𝑅)(𝑓(.r‘𝑅)𝑔)) = (𝑟(.r‘𝑅)𝑋)) |
95 | 92, 94 | eqtr2d 2769 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑟(.r‘𝑅)𝑋) = ((𝑟(.r‘𝑅)𝑓)(.r‘𝑅)𝑔)) |
96 | 90, 91, 95 | 3eqtrrd 2773 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → ((𝑟(.r‘𝑅)𝑓)(.r‘𝑅)𝑔) = ((1r‘𝑅)(.r‘𝑅)𝑔)) |
97 | 5, 65, 27, 82, 84, 88, 89, 96 | idomrcan 32962 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑟(.r‘𝑅)𝑓) = (1r‘𝑅)) |
98 | 8, 85 | 1unit 20313 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
99 | 3, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1r‘𝑅) ∈ (Unit‘𝑅)) |
100 | 99 | ad6antr 735 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (1r‘𝑅) ∈ (Unit‘𝑅)) |
101 | 97, 100 | eqeltrd 2829 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → (𝑟(.r‘𝑅)𝑓) ∈ (Unit‘𝑅)) |
102 | 8, 27, 5 | unitmulclb 20320 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → ((𝑟(.r‘𝑅)𝑓) ∈ (Unit‘𝑅) ↔ (𝑟 ∈ (Unit‘𝑅) ∧ 𝑓 ∈ (Unit‘𝑅)))) |
103 | 102 | simplbda 499 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) ∧ (𝑟(.r‘𝑅)𝑓) ∈ (Unit‘𝑅)) → 𝑓 ∈ (Unit‘𝑅)) |
104 | 61, 62, 64, 101, 103 | syl31anc 1371 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) ∧ 𝑟 ∈ 𝐵) ∧ 𝑔 = (𝑟(.r‘𝑅)𝑋)) → 𝑓 ∈ (Unit‘𝑅)) |
105 | 1 | ad4antr 731 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑋 ∈ 𝐵) |
106 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑔 ∈ 𝑀) |
107 | 106, 10 | eleqtrdi 2839 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑔 ∈ (𝐾‘{𝑋})) |
108 | 5, 27, 9 | rspsnel 33096 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑔 ∈ (𝐾‘{𝑋}) ↔ ∃𝑟 ∈ 𝐵 𝑔 = (𝑟(.r‘𝑅)𝑋))) |
109 | 108 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) ∧ 𝑔 ∈ (𝐾‘{𝑋})) → ∃𝑟 ∈ 𝐵 𝑔 = (𝑟(.r‘𝑅)𝑋)) |
110 | 70, 105, 107, 109 | syl21anc 837 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → ∃𝑟 ∈ 𝐵 𝑔 = (𝑟(.r‘𝑅)𝑋)) |
111 | 104, 110 | r19.29a 3159 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑓 ∈ (Unit‘𝑅)) |
112 | | simp-4r 783 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) |
113 | 112 | eldifbd 3960 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) ∧ 𝑔 ∈ 𝑀) → ¬ 𝑓 ∈ (Unit‘𝑅)) |
114 | 111, 113 | pm2.65da 816 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → ¬ 𝑔 ∈ 𝑀) |
115 | 57, 114 | eldifd 3958 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑔 ∈ ((𝐾‘{𝑔}) ∖ 𝑀)) |
116 | 5, 15, 16, 22, 52, 115 | mxidlmaxv 33194 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → (𝐾‘{𝑔}) = 𝐵) |
117 | | eqid 2728 |
. . . . . . . 8
⊢ (𝐾‘{𝑔}) = (𝐾‘{𝑔}) |
118 | 2 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑅 ∈ IDomn) |
119 | 8, 9, 117, 5, 18, 118 | unitpidl1 33152 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → ((𝐾‘{𝑔}) = 𝐵 ↔ 𝑔 ∈ (Unit‘𝑅))) |
120 | 116, 119 | mpbid 231 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → 𝑔 ∈ (Unit‘𝑅)) |
121 | 17 | eldifbd 3960 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ (𝑓(.r‘𝑅)𝑔) = 𝑋) → ¬ 𝑔 ∈ (Unit‘𝑅)) |
122 | 120, 121 | pm2.65da 816 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))) → ¬ (𝑓(.r‘𝑅)𝑔) = 𝑋) |
123 | 122 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐵 ∖ (Unit‘𝑅)) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅)))) → ¬ (𝑓(.r‘𝑅)𝑔) = 𝑋) |
124 | 123 | neqned 2944 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐵 ∖ (Unit‘𝑅)) ∧ 𝑔 ∈ (𝐵 ∖ (Unit‘𝑅)))) → (𝑓(.r‘𝑅)𝑔) ≠ 𝑋) |
125 | 124 | ralrimivva 3197 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))∀𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))(𝑓(.r‘𝑅)𝑔) ≠ 𝑋) |
126 | | eqid 2728 |
. . 3
⊢
(Irred‘𝑅) =
(Irred‘𝑅) |
127 | | eqid 2728 |
. . 3
⊢ (𝐵 ∖ (Unit‘𝑅)) = (𝐵 ∖ (Unit‘𝑅)) |
128 | 5, 8, 126, 127, 27 | isirred 20358 |
. 2
⊢ (𝑋 ∈ (Irred‘𝑅) ↔ (𝑋 ∈ (𝐵 ∖ (Unit‘𝑅)) ∧ ∀𝑓 ∈ (𝐵 ∖ (Unit‘𝑅))∀𝑔 ∈ (𝐵 ∖ (Unit‘𝑅))(𝑓(.r‘𝑅)𝑔) ≠ 𝑋)) |
129 | 14, 125, 128 | sylanbrc 582 |
1
⊢ (𝜑 → 𝑋 ∈ (Irred‘𝑅)) |