| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > drngmxidl | Structured version Visualization version GIF version | ||
| Description: The zero ideal is the only ideal of a division ring. (Contributed by Thierry Arnoux, 16-Mar-2025.) |
| Ref | Expression |
|---|---|
| drngmxidl.1 | ⊢ 0 = (0g‘𝑅) |
| Ref | Expression |
|---|---|
| drngmxidl | ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) = {{ 0 }}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | drngring 20605 | . . . . . 6 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | |
| 2 | eqid 2729 | . . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 3 | 2 | mxidlidl 33396 | . . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (MaxIdeal‘𝑅)) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 4 | 3 | ex 412 | . . . . . . 7 ⊢ (𝑅 ∈ Ring → (𝑖 ∈ (MaxIdeal‘𝑅) → 𝑖 ∈ (LIdeal‘𝑅))) |
| 5 | 4 | ssrdv 3937 | . . . . . 6 ⊢ (𝑅 ∈ Ring → (MaxIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) |
| 6 | 1, 5 | syl 17 | . . . . 5 ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) |
| 7 | drngmxidl.1 | . . . . . 6 ⊢ 0 = (0g‘𝑅) | |
| 8 | eqid 2729 | . . . . . 6 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅) | |
| 9 | 2, 7, 8 | drngnidl 21134 | . . . . 5 ⊢ (𝑅 ∈ DivRing → (LIdeal‘𝑅) = {{ 0 }, (Base‘𝑅)}) |
| 10 | 6, 9 | sseqtrd 3968 | . . . 4 ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) ⊆ {{ 0 }, (Base‘𝑅)}) |
| 11 | 2 | mxidlnr 33397 | . . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (MaxIdeal‘𝑅)) → 𝑖 ≠ (Base‘𝑅)) |
| 12 | 1, 11 | sylan 580 | . . . . 5 ⊢ ((𝑅 ∈ DivRing ∧ 𝑖 ∈ (MaxIdeal‘𝑅)) → 𝑖 ≠ (Base‘𝑅)) |
| 13 | 12 | nelrdva 3661 | . . . 4 ⊢ (𝑅 ∈ DivRing → ¬ (Base‘𝑅) ∈ (MaxIdeal‘𝑅)) |
| 14 | ssdifsn 4737 | . . . 4 ⊢ ((MaxIdeal‘𝑅) ⊆ ({{ 0 }, (Base‘𝑅)} ∖ {(Base‘𝑅)}) ↔ ((MaxIdeal‘𝑅) ⊆ {{ 0 }, (Base‘𝑅)} ∧ ¬ (Base‘𝑅) ∈ (MaxIdeal‘𝑅))) | |
| 15 | 10, 13, 14 | sylanbrc 583 | . . 3 ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) ⊆ ({{ 0 }, (Base‘𝑅)} ∖ {(Base‘𝑅)})) |
| 16 | drngnzr 20617 | . . . 4 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | |
| 17 | 7, 2 | drnglidl1ne0 33408 | . . . . 5 ⊢ (𝑅 ∈ NzRing → (Base‘𝑅) ≠ { 0 }) |
| 18 | 17 | necomd 2980 | . . . 4 ⊢ (𝑅 ∈ NzRing → { 0 } ≠ (Base‘𝑅)) |
| 19 | difprsn2 4750 | . . . 4 ⊢ ({ 0 } ≠ (Base‘𝑅) → ({{ 0 }, (Base‘𝑅)} ∖ {(Base‘𝑅)}) = {{ 0 }}) | |
| 20 | 16, 18, 19 | 3syl 18 | . . 3 ⊢ (𝑅 ∈ DivRing → ({{ 0 }, (Base‘𝑅)} ∖ {(Base‘𝑅)}) = {{ 0 }}) |
| 21 | 15, 20 | sseqtrd 3968 | . 2 ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) ⊆ {{ 0 }}) |
| 22 | 7 | drng0mxidl 33409 | . . 3 ⊢ (𝑅 ∈ DivRing → { 0 } ∈ (MaxIdeal‘𝑅)) |
| 23 | 22 | snssd 4758 | . 2 ⊢ (𝑅 ∈ DivRing → {{ 0 }} ⊆ (MaxIdeal‘𝑅)) |
| 24 | 21, 23 | eqssd 3949 | 1 ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) = {{ 0 }}) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3896 ⊆ wss 3899 {csn 4573 {cpr 4575 ‘cfv 6476 Basecbs 17107 0gc0g 17330 Ringcrg 20105 NzRingcnzr 20381 DivRingcdr 20598 LIdealclidl 21097 MaxIdealcmxidl 33392 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5214 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5367 ax-un 7662 ax-cnex 11053 ax-resscn 11054 ax-1cn 11055 ax-icn 11056 ax-addcl 11057 ax-addrcl 11058 ax-mulcl 11059 ax-mulrcl 11060 ax-mulcom 11061 ax-addass 11062 ax-mulass 11063 ax-distr 11064 ax-i2m1 11065 ax-1ne0 11066 ax-1rid 11067 ax-rnegex 11068 ax-rrecex 11069 ax-cnre 11070 ax-pre-lttri 11071 ax-pre-lttrn 11072 ax-pre-ltadd 11073 ax-pre-mulgt0 11074 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3393 df-v 3435 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4940 df-br 5089 df-opab 5151 df-mpt 5170 df-tr 5196 df-id 5508 df-eprel 5513 df-po 5521 df-so 5522 df-fr 5566 df-we 5568 df-xp 5619 df-rel 5620 df-cnv 5621 df-co 5622 df-dm 5623 df-rn 5624 df-res 5625 df-ima 5626 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7297 df-ov 7343 df-oprab 7344 df-mpo 7345 df-om 7791 df-1st 7915 df-2nd 7916 df-tpos 8150 df-frecs 8205 df-wrecs 8236 df-recs 8285 df-rdg 8323 df-er 8616 df-en 8864 df-dom 8865 df-sdom 8866 df-pnf 11139 df-mnf 11140 df-xr 11141 df-ltxr 11142 df-le 11143 df-sub 11337 df-neg 11338 df-nn 12117 df-2 12179 df-3 12180 df-4 12181 df-5 12182 df-6 12183 df-7 12184 df-8 12185 df-sets 17062 df-slot 17080 df-ndx 17092 df-base 17108 df-ress 17129 df-plusg 17161 df-mulr 17162 df-sca 17164 df-vsca 17165 df-ip 17166 df-0g 17332 df-mgm 18501 df-sgrp 18580 df-mnd 18596 df-grp 18802 df-minusg 18803 df-sbg 18804 df-subg 18989 df-cmn 19648 df-abl 19649 df-mgp 20013 df-rng 20025 df-ur 20054 df-ring 20107 df-oppr 20209 df-dvdsr 20229 df-unit 20230 df-invr 20260 df-nzr 20382 df-subrg 20439 df-drng 20600 df-lmod 20749 df-lss 20819 df-sra 21061 df-rgmod 21062 df-lidl 21099 df-mxidl 33393 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |