Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  divrngidl Structured version   Visualization version   GIF version

Theorem divrngidl 34784
Description: The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypotheses
Ref Expression
divrngidl.1 𝐺 = (1st𝑅)
divrngidl.2 𝐻 = (2nd𝑅)
divrngidl.3 𝑋 = ran 𝐺
divrngidl.4 𝑍 = (GId‘𝐺)
Assertion
Ref Expression
divrngidl (𝑅 ∈ DivRingOps → (Idl‘𝑅) = {{𝑍}, 𝑋})

Proof of Theorem divrngidl
Dummy variables 𝑖 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 divrngidl.1 . . 3 𝐺 = (1st𝑅)
2 divrngidl.2 . . 3 𝐻 = (2nd𝑅)
3 divrngidl.4 . . 3 𝑍 = (GId‘𝐺)
4 divrngidl.3 . . 3 𝑋 = ran 𝐺
5 eqid 2793 . . 3 (GId‘𝐻) = (GId‘𝐻)
61, 2, 3, 4, 5isdrngo2 34714 . 2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ ((GId‘𝐻) ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻))))
71, 3idl0cl 34774 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑍𝑖)
87adantr 481 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → 𝑍𝑖)
93fvexi 6544 . . . . . . . . . . . . 13 𝑍 ∈ V
109snss 4619 . . . . . . . . . . . 12 (𝑍𝑖 ↔ {𝑍} ⊆ 𝑖)
11 necom 3035 . . . . . . . . . . . 12 (𝑖 ≠ {𝑍} ↔ {𝑍} ≠ 𝑖)
12 pssdifn0 4239 . . . . . . . . . . . . 13 (({𝑍} ⊆ 𝑖 ∧ {𝑍} ≠ 𝑖) → (𝑖 ∖ {𝑍}) ≠ ∅)
13 n0 4224 . . . . . . . . . . . . 13 ((𝑖 ∖ {𝑍}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍}))
1412, 13sylib 219 . . . . . . . . . . . 12 (({𝑍} ⊆ 𝑖 ∧ {𝑍} ≠ 𝑖) → ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍}))
1510, 11, 14syl2anb 597 . . . . . . . . . . 11 ((𝑍𝑖𝑖 ≠ {𝑍}) → ∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍}))
161, 4idlss 34772 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖𝑋)
17 ssdif 4032 . . . . . . . . . . . . . . . . . 18 (𝑖𝑋 → (𝑖 ∖ {𝑍}) ⊆ (𝑋 ∖ {𝑍}))
1817sselda 3884 . . . . . . . . . . . . . . . . 17 ((𝑖𝑋𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑧 ∈ (𝑋 ∖ {𝑍}))
1916, 18sylan 580 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑧 ∈ (𝑋 ∖ {𝑍}))
20 oveq2 7015 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑦𝐻𝑥) = (𝑦𝐻𝑧))
2120eqeq1d 2795 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑦𝐻𝑥) = (GId‘𝐻) ↔ (𝑦𝐻𝑧) = (GId‘𝐻)))
2221rexbidv 3257 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻) ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻)))
2322rspcva 3552 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻))
2419, 23sylan 580 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻))
25 eldifi 4019 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑧𝑖)
26 eldifi 4019 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑋 ∖ {𝑍}) → 𝑦𝑋)
2725, 26anim12i 612 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑖 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑧𝑖𝑦𝑋))
281, 2, 4idllmulcl 34776 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧𝑖𝑦𝑋)) → (𝑦𝐻𝑧) ∈ 𝑖)
291, 2, 4, 51idl 34782 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((GId‘𝐻) ∈ 𝑖𝑖 = 𝑋))
3029biimpd 230 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((GId‘𝐻) ∈ 𝑖𝑖 = 𝑋))
3130adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧𝑖𝑦𝑋)) → ((GId‘𝐻) ∈ 𝑖𝑖 = 𝑋))
32 eleq1 2868 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐻𝑧) = (GId‘𝐻) → ((𝑦𝐻𝑧) ∈ 𝑖 ↔ (GId‘𝐻) ∈ 𝑖))
3332imbi1d 343 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐻𝑧) = (GId‘𝐻) → (((𝑦𝐻𝑧) ∈ 𝑖𝑖 = 𝑋) ↔ ((GId‘𝐻) ∈ 𝑖𝑖 = 𝑋)))
3431, 33syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧𝑖𝑦𝑋)) → ((𝑦𝐻𝑧) = (GId‘𝐻) → ((𝑦𝐻𝑧) ∈ 𝑖𝑖 = 𝑋)))
3528, 34mpid 44 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧𝑖𝑦𝑋)) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋))
3627, 35sylan2 592 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑧 ∈ (𝑖 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍}))) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋))
3736anassrs 468 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋))
3837rexlimdva 3244 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻) → 𝑖 = 𝑋))
3938imp 407 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑧) = (GId‘𝐻)) → 𝑖 = 𝑋)
4024, 39syldan 591 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → 𝑖 = 𝑋)
4140an32s 648 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑧 ∈ (𝑖 ∖ {𝑍})) → 𝑖 = 𝑋)
4241ex 413 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑖 = 𝑋))
4342exlimdv 1909 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (∃𝑧 𝑧 ∈ (𝑖 ∖ {𝑍}) → 𝑖 = 𝑋))
4415, 43syl5 34 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ((𝑍𝑖𝑖 ≠ {𝑍}) → 𝑖 = 𝑋))
458, 44mpand 691 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ≠ {𝑍} → 𝑖 = 𝑋))
4645an32s 648 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑖 ≠ {𝑍} → 𝑖 = 𝑋))
47 neor 3074 . . . . . . . 8 ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ↔ (𝑖 ≠ {𝑍} → 𝑖 = 𝑋))
4846, 47sylibr 235 . . . . . . 7 (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
4948ex 413 . . . . . 6 ((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) → (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)))
501, 30idl 34781 . . . . . . . . 9 (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
51 eleq1 2868 . . . . . . . . 9 (𝑖 = {𝑍} → (𝑖 ∈ (Idl‘𝑅) ↔ {𝑍} ∈ (Idl‘𝑅)))
5250, 51syl5ibrcom 248 . . . . . . . 8 (𝑅 ∈ RingOps → (𝑖 = {𝑍} → 𝑖 ∈ (Idl‘𝑅)))
531, 4rngoidl 34780 . . . . . . . . 9 (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅))
54 eleq1 2868 . . . . . . . . 9 (𝑖 = 𝑋 → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑋 ∈ (Idl‘𝑅)))
5553, 54syl5ibrcom 248 . . . . . . . 8 (𝑅 ∈ RingOps → (𝑖 = 𝑋𝑖 ∈ (Idl‘𝑅)))
5652, 55jaod 854 . . . . . . 7 (𝑅 ∈ RingOps → ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) → 𝑖 ∈ (Idl‘𝑅)))
5756adantr 481 . . . . . 6 ((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) → 𝑖 ∈ (Idl‘𝑅)))
5849, 57impbid 213 . . . . 5 ((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)))
59 vex 3435 . . . . . 6 𝑖 ∈ V
6059elpr 4489 . . . . 5 (𝑖 ∈ {{𝑍}, 𝑋} ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
6158, 60syl6bbr 290 . . . 4 ((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ {{𝑍}, 𝑋}))
6261eqrdv 2791 . . 3 ((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻)) → (Idl‘𝑅) = {{𝑍}, 𝑋})
6362adantrl 712 . 2 ((𝑅 ∈ RingOps ∧ ((GId‘𝐻) ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = (GId‘𝐻))) → (Idl‘𝑅) = {{𝑍}, 𝑋})
646, 63sylbi 218 1 (𝑅 ∈ DivRingOps → (Idl‘𝑅) = {{𝑍}, 𝑋})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 842   = wceq 1520  wex 1759  wcel 2079  wne 2982  wral 3103  wrex 3104  cdif 3851  wss 3854  c0 4206  {csn 4466  {cpr 4468  ran crn 5436  cfv 6217  (class class class)co 7007  1st c1st 7534  2nd c2nd 7535  GIdcgi 27946  RingOpscrngo 34650  DivRingOpscdrng 34704  Idlcidl 34763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-om 7428  df-1st 7536  df-2nd 7537  df-1o 7944  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-fin 8351  df-grpo 27949  df-gid 27950  df-ginv 27951  df-ablo 28001  df-ass 34599  df-exid 34601  df-mgmOLD 34605  df-sgrOLD 34617  df-mndo 34623  df-rngo 34651  df-drngo 34705  df-idl 34766
This theorem is referenced by:  divrngpr  34809  isfldidl  34824
  Copyright terms: Public domain W3C validator