Metamath Proof Explorer

Theorem divrngidl

Description: The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses divrngidl.1 ⊢G=1st⁡R
divrngidl.2 ⊢H=2nd⁡R
divrngidl.3 ⊢X=ran⁡G
divrngidl.4 ⊢Z=GId⁡G
Assertion divrngidl ⊢R∈DivRingOps→Idl⁡R=ZX

Proof

Step Hyp Ref Expression
1 divrngidl.1 ⊢G=1st⁡R
2 divrngidl.2 ⊢H=2nd⁡R
3 divrngidl.3 ⊢X=ran⁡G
4 divrngidl.4 ⊢Z=GId⁡G
5 eqid ⊢GId⁡H=GId⁡H
6 1 2 4 3 5 isdrngo2 ⊢R∈DivRingOps↔R∈RingOps∧GId⁡H≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H
7 1 4 idl0cl ⊢R∈RingOps∧i∈Idl⁡R→Z∈i
8 7 adantr ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→Z∈i
9 4 fvexi ⊢Z∈V
10 9 snss ⊢Z∈i↔Z⊆i
11 necom ⊢i≠Z↔Z≠i
12 pssdifn0 ⊢Z⊆i∧Z≠i→i∖Z≠∅
13 n0 ⊢i∖Z≠∅↔∃zz∈i∖Z
14 12 13 sylib ⊢Z⊆i∧Z≠i→∃zz∈i∖Z
15 10 11 14 syl2anb ⊢Z∈i∧i≠Z→∃zz∈i∖Z
16 1 3 idlss ⊢R∈RingOps∧i∈Idl⁡R→i⊆X
17 ssdif ⊢i⊆X→i∖Z⊆X∖Z
18 17 sselda ⊢i⊆X∧z∈i∖Z→z∈X∖Z
19 16 18 sylan ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z→z∈X∖Z
20 oveq2 ⊢x=z→yHx=yHz
21 20 eqeq1d ⊢x=z→yHx=GId⁡H↔yHz=GId⁡H
22 21 rexbidv ⊢x=z→∃y∈X∖ZyHx=GId⁡H↔∃y∈X∖ZyHz=GId⁡H
23 22 rspcva ⊢z∈X∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→∃y∈X∖ZyHz=GId⁡H
24 19 23 sylan ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→∃y∈X∖ZyHz=GId⁡H
25 eldifi ⊢z∈i∖Z→z∈i
26 eldifi ⊢y∈X∖Z→y∈X
27 25 26 anim12i ⊢z∈i∖Z∧y∈X∖Z→z∈i∧y∈X
28 1 2 3 idllmulcl ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∧y∈X→yHz∈i
29 1 2 3 5 1idl ⊢R∈RingOps∧i∈Idl⁡R→GId⁡H∈i↔i=X
30 29 biimpd ⊢R∈RingOps∧i∈Idl⁡R→GId⁡H∈i→i=X
31 30 adantr ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∧y∈X→GId⁡H∈i→i=X
32 eleq1 ⊢yHz=GId⁡H→yHz∈i↔GId⁡H∈i
33 32 imbi1d ⊢yHz=GId⁡H→yHz∈i→i=X↔GId⁡H∈i→i=X
34 31 33 syl5ibrcom ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∧y∈X→yHz=GId⁡H→yHz∈i→i=X
35 28 34 mpid ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∧y∈X→yHz=GId⁡H→i=X
36 27 35 sylan2 ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z∧y∈X∖Z→yHz=GId⁡H→i=X
37 36 anassrs ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z∧y∈X∖Z→yHz=GId⁡H→i=X
38 37 rexlimdva ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z→∃y∈X∖ZyHz=GId⁡H→i=X
39 38 imp ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z∧∃y∈X∖ZyHz=GId⁡H→i=X
40 24 39 syldan ⊢R∈RingOps∧i∈Idl⁡R∧z∈i∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i=X
41 40 an32s ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H∧z∈i∖Z→i=X
42 41 ex ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→z∈i∖Z→i=X
43 42 exlimdv ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→∃zz∈i∖Z→i=X
44 15 43 syl5 ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→Z∈i∧i≠Z→i=X
45 8 44 mpand ⊢R∈RingOps∧i∈Idl⁡R∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i≠Z→i=X
46 45 an32s ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H∧i∈Idl⁡R→i≠Z→i=X
47 neor ⊢i=Z∨i=X↔i≠Z→i=X
48 46 47 sylibr ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H∧i∈Idl⁡R→i=Z∨i=X
49 48 ex ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i∈Idl⁡R→i=Z∨i=X
50 1 4 0idl ⊢R∈RingOps→Z∈Idl⁡R
51 eleq1 ⊢i=Z→i∈Idl⁡R↔Z∈Idl⁡R
52 50 51 syl5ibrcom ⊢R∈RingOps→i=Z→i∈Idl⁡R
53 1 3 rngoidl ⊢R∈RingOps→X∈Idl⁡R
54 eleq1 ⊢i=X→i∈Idl⁡R↔X∈Idl⁡R
55 53 54 syl5ibrcom ⊢R∈RingOps→i=X→i∈Idl⁡R
56 52 55 jaod ⊢R∈RingOps→i=Z∨i=X→i∈Idl⁡R
57 56 adantr ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i=Z∨i=X→i∈Idl⁡R
58 49 57 impbid ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i∈Idl⁡R↔i=Z∨i=X
59 vex ⊢i∈V
60 59 elpr ⊢i∈ZX↔i=Z∨i=X
61 58 60 bitr4di ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→i∈Idl⁡R↔i∈ZX
62 61 eqrdv ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→Idl⁡R=ZX
63 62 adantrl ⊢R∈RingOps∧GId⁡H≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=GId⁡H→Idl⁡R=ZX
64 6 63 sylbi ⊢R∈DivRingOps→Idl⁡R=ZX