Step | Hyp | Ref
| Expression |
1 | | divrngidl.1 |
. . 3
⊢ 𝐺 = (1st ‘𝑅) |
2 | | divrngidl.2 |
. . 3
⊢ 𝐻 = (2nd ‘𝑅) |
3 | | divrngidl.4 |
. . 3
⊢ 𝑍 = (GId‘𝐺) |
4 | | divrngidl.3 |
. . 3
⊢ 𝑋 = ran 𝐺 |
5 | | eqid 2610 |
. . 3
⊢
(GId‘𝐻) =
(GId‘𝐻) |
6 | 1, 2, 3, 4, 5 | isdrngo2 32927 |
. 2
⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧
((GId‘𝐻) ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)))) |
7 | 1, 3 | idl0cl 32987 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝑖) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → 𝑍 ∈ 𝑖) |
9 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(GId‘𝐺) ∈
V |
10 | 3, 9 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
11 | 10 | snss 4259 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ 𝑖 ↔ {𝑍} ⊆ 𝑖) |
12 | | necom 2835 |
. . . . . . . . . . . 12
⊢ (𝑖 ≠ {𝑍} ↔ {𝑍} ≠ 𝑖) |
13 | | pssdifn0 3898 |
. . . . . . . . . . . . 13
⊢ (({𝑍} ⊆ 𝑖 ∧ {𝑍} ≠ 𝑖) → (𝑖 ∖ {𝑍}) ≠ ∅) |
14 | | n0 3890 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∖ {𝑍}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍})) |
15 | 13, 14 | sylib 207 |
. . . . . . . . . . . 12
⊢ (({𝑍} ⊆ 𝑖 ∧ {𝑍} ≠ 𝑖) → ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍})) |
16 | 11, 12, 15 | syl2anb 495 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ 𝑖 ∧ 𝑖 ≠ {𝑍}) → ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍})) |
17 | 1, 4 | idlss 32985 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ 𝑋) |
18 | | ssdif 3707 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ⊆ 𝑋 → (𝑖 ∖ {𝑍}) ⊆ (𝑋 ∖ {𝑍})) |
19 | 18 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ⊆ 𝑋 ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑧 ∈ (𝑋 ∖ {𝑍})) |
20 | 17, 19 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑧 ∈ (𝑋 ∖ {𝑍})) |
21 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝑦𝐻𝑥) = (𝑦𝐻𝑧)) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((𝑦𝐻𝑥) = (GId‘𝐻) ↔ (𝑦𝐻𝑧) = (GId‘𝐻))) |
23 | 22 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻) ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻))) |
24 | 23 | rspcva 3280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻)) |
25 | 20, 24 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻)) |
26 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑧 ∈ 𝑖) |
27 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑋 ∖ {𝑍}) → 𝑦 ∈ 𝑋) |
28 | 26, 27 | anim12i 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (𝑖 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋)) |
29 | 1, 2, 4 | idllmulcl 32989 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝑧) ∈ 𝑖) |
30 | 1, 2, 4, 5 | 1idl 32995 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((GId‘𝐻) ∈ 𝑖 ↔ 𝑖 = 𝑋)) |
31 | 30 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((GId‘𝐻) ∈ 𝑖 → 𝑖 = 𝑋)) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋)) → ((GId‘𝐻) ∈ 𝑖 → 𝑖 = 𝑋)) |
33 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦𝐻𝑧) = (GId‘𝐻) → ((𝑦𝐻𝑧) ∈ 𝑖 ↔ (GId‘𝐻) ∈ 𝑖)) |
34 | 33 | imbi1d 330 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦𝐻𝑧) = (GId‘𝐻) → (((𝑦𝐻𝑧) ∈ 𝑖 → 𝑖 = 𝑋) ↔ ((GId‘𝐻) ∈ 𝑖 → 𝑖 = 𝑋))) |
35 | 32, 34 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋)) → ((𝑦𝐻𝑧) = (GId‘𝐻) → ((𝑦𝐻𝑧) ∈ 𝑖 → 𝑖 = 𝑋))) |
36 | 29, 35 | mpid 43 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋)) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋)) |
37 | 28, 36 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ (𝑖 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍}))) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋)) |
38 | 37 | anassrs 678 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋)) |
39 | 38 | rexlimdva 3013 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋)) |
40 | 39 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻)) → 𝑖 = 𝑋) |
41 | 25, 40 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → 𝑖 = 𝑋) |
42 | 41 | an32s 842 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑖 = 𝑋) |
43 | 42 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑖 = 𝑋)) |
44 | 43 | exlimdv 1848 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑖 = 𝑋)) |
45 | 16, 44 | syl5 33 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ((𝑍 ∈ 𝑖 ∧ 𝑖 ≠ {𝑍}) → 𝑖 = 𝑋)) |
46 | 8, 45 | mpand 707 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ≠ {𝑍} → 𝑖 = 𝑋)) |
47 | 46 | an32s 842 |
. . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑖 ≠ {𝑍} → 𝑖 = 𝑋)) |
48 | | neor 2873 |
. . . . . . . 8
⊢ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ↔ (𝑖 ≠ {𝑍} → 𝑖 = 𝑋)) |
49 | 47, 48 | sylibr 223 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) |
50 | 49 | ex 449 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) → (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))) |
51 | 1, 3 | 0idl 32994 |
. . . . . . . . 9
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) |
52 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑖 = {𝑍} → (𝑖 ∈ (Idl‘𝑅) ↔ {𝑍} ∈ (Idl‘𝑅))) |
53 | 51, 52 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝑅 ∈ RingOps → (𝑖 = {𝑍} → 𝑖 ∈ (Idl‘𝑅))) |
54 | 1, 4 | rngoidl 32993 |
. . . . . . . . 9
⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅)) |
55 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑖 = 𝑋 → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑋 ∈ (Idl‘𝑅))) |
56 | 54, 55 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝑅 ∈ RingOps → (𝑖 = 𝑋 → 𝑖 ∈ (Idl‘𝑅))) |
57 | 53, 56 | jaod 394 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) → 𝑖 ∈ (Idl‘𝑅))) |
58 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) → 𝑖 ∈ (Idl‘𝑅))) |
59 | 50, 58 | impbid 201 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))) |
60 | | vex 3176 |
. . . . . 6
⊢ 𝑖 ∈ V |
61 | 60 | elpr 4146 |
. . . . 5
⊢ (𝑖 ∈ {{𝑍}, 𝑋} ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) |
62 | 59, 61 | syl6bbr 277 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ {{𝑍}, 𝑋})) |
63 | 62 | eqrdv 2608 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧
∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (Idl‘𝑅) = {{𝑍}, 𝑋}) |
64 | 63 | adantrl 748 |
. 2
⊢ ((𝑅 ∈ RingOps ∧
((GId‘𝐻) ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻))) → (Idl‘𝑅) = {{𝑍}, 𝑋}) |
65 | 6, 64 | sylbi 206 |
1
⊢ (𝑅 ∈ DivRingOps →
(Idl‘𝑅) = {{𝑍}, 𝑋}) |