![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > qsfld | Structured version Visualization version GIF version |
Description: An ideal π in the commutative ring π is maximal if and only if the factor ring π is a field. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
Ref | Expression |
---|---|
qsfld.1 | β’ π = (π /s (π ~QG π)) |
qsfld.2 | β’ (π β π β CRing) |
qsfld.3 | β’ (π β π β NzRing) |
qsfld.4 | β’ (π β π β (LIdealβπ )) |
Ref | Expression |
---|---|
qsfld | β’ (π β (π β Field β π β (MaxIdealβπ ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2740 | . . 3 β’ (opprβπ ) = (opprβπ ) | |
2 | qsfld.1 | . . 3 β’ π = (π /s (π ~QG π)) | |
3 | qsfld.3 | . . 3 β’ (π β π β NzRing) | |
4 | qsfld.4 | . . . 4 β’ (π β π β (LIdealβπ )) | |
5 | qsfld.2 | . . . . 5 β’ (π β π β CRing) | |
6 | eqid 2740 | . . . . . 6 β’ (LIdealβπ ) = (LIdealβπ ) | |
7 | 6 | crng2idl 21334 | . . . . 5 β’ (π β CRing β (LIdealβπ ) = (2Idealβπ )) |
8 | 5, 7 | syl 17 | . . . 4 β’ (π β (LIdealβπ ) = (2Idealβπ )) |
9 | 4, 8 | eleqtrd 2846 | . . 3 β’ (π β π β (2Idealβπ )) |
10 | 1, 2, 3, 9 | qsdrng 33510 | . 2 β’ (π β (π β DivRing β (π β (MaxIdealβπ ) β§ π β (MaxIdealβ(opprβπ ))))) |
11 | isfld 20782 | . . 3 β’ (π β Field β (π β DivRing β§ π β CRing)) | |
12 | 2, 6 | quscrng 21336 | . . . . 5 β’ ((π β CRing β§ π β (LIdealβπ )) β π β CRing) |
13 | 5, 4, 12 | syl2anc 583 | . . . 4 β’ (π β π β CRing) |
14 | 13 | biantrud 531 | . . 3 β’ (π β (π β DivRing β (π β DivRing β§ π β CRing))) |
15 | 11, 14 | bitr4id 290 | . 2 β’ (π β (π β Field β π β DivRing)) |
16 | eqid 2740 | . . . . . . 7 β’ (MaxIdealβπ ) = (MaxIdealβπ ) | |
17 | 16, 1 | crngmxidl 33482 | . . . . . 6 β’ (π β CRing β (MaxIdealβπ ) = (MaxIdealβ(opprβπ ))) |
18 | 5, 17 | syl 17 | . . . . 5 β’ (π β (MaxIdealβπ ) = (MaxIdealβ(opprβπ ))) |
19 | 18 | eleq2d 2830 | . . . 4 β’ (π β (π β (MaxIdealβπ ) β π β (MaxIdealβ(opprβπ )))) |
20 | 19 | biimpd 229 | . . 3 β’ (π β (π β (MaxIdealβπ ) β π β (MaxIdealβ(opprβπ )))) |
21 | 20 | pm4.71d 561 | . 2 β’ (π β (π β (MaxIdealβπ ) β (π β (MaxIdealβπ ) β§ π β (MaxIdealβ(opprβπ ))))) |
22 | 10, 15, 21 | 3bitr4d 311 | 1 β’ (π β (π β Field β π β (MaxIdealβπ ))) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 206 β§ wa 395 = wceq 1537 β wcel 2108 βcfv 6576 (class class class)co 7451 /s cqus 17585 ~QG cqg 19182 CRingccrg 20281 opprcoppr 20379 NzRingcnzr 20558 DivRingcdr 20771 Fieldcfield 20772 LIdealclidl 21259 2Idealc2idl 21302 MaxIdealcmxidl 33472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5304 ax-sep 5318 ax-nul 5325 ax-pow 5384 ax-pr 5448 ax-un 7773 ax-cnex 11243 ax-resscn 11244 ax-1cn 11245 ax-icn 11246 ax-addcl 11247 ax-addrcl 11248 ax-mulcl 11249 ax-mulrcl 11250 ax-mulcom 11251 ax-addass 11252 ax-mulass 11253 ax-distr 11254 ax-i2m1 11255 ax-1ne0 11256 ax-1rid 11257 ax-rnegex 11258 ax-rrecex 11259 ax-cnre 11260 ax-pre-lttri 11261 ax-pre-lttrn 11262 ax-pre-ltadd 11263 ax-pre-mulgt0 11264 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4933 df-int 4972 df-iun 5018 df-iin 5019 df-br 5168 df-opab 5230 df-mpt 5251 df-tr 5285 df-id 5594 df-eprel 5600 df-po 5608 df-so 5609 df-fr 5653 df-se 5654 df-we 5655 df-xp 5707 df-rel 5708 df-cnv 5709 df-co 5710 df-dm 5711 df-rn 5712 df-res 5713 df-ima 5714 df-pred 6335 df-ord 6401 df-on 6402 df-lim 6403 df-suc 6404 df-iota 6528 df-fun 6578 df-fn 6579 df-f 6580 df-f1 6581 df-fo 6582 df-f1o 6583 df-fv 6584 df-isom 6585 df-riota 7407 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7717 df-om 7907 df-1st 8033 df-2nd 8034 df-supp 8205 df-tpos 8270 df-frecs 8325 df-wrecs 8356 df-recs 8430 df-rdg 8469 df-1o 8525 df-2o 8526 df-oadd 8529 df-er 8766 df-ec 8768 df-qs 8772 df-map 8889 df-ixp 8959 df-en 9007 df-dom 9008 df-sdom 9009 df-fin 9010 df-fsupp 9435 df-sup 9514 df-inf 9515 df-oi 9582 df-dju 9973 df-card 10011 df-pnf 11329 df-mnf 11330 df-xr 11331 df-ltxr 11332 df-le 11333 df-sub 11526 df-neg 11527 df-nn 12299 df-2 12361 df-3 12362 df-4 12363 df-5 12364 df-6 12365 df-7 12366 df-8 12367 df-9 12368 df-n0 12559 df-xnn0 12632 df-z 12646 df-dec 12766 df-uz 12911 df-fz 13579 df-fzo 13723 df-seq 14070 df-hash 14397 df-struct 17214 df-sets 17231 df-slot 17249 df-ndx 17261 df-base 17279 df-ress 17308 df-plusg 17344 df-mulr 17345 df-sca 17347 df-vsca 17348 df-ip 17349 df-tset 17350 df-ple 17351 df-ds 17353 df-hom 17355 df-cco 17356 df-0g 17521 df-gsum 17522 df-prds 17527 df-pws 17529 df-imas 17588 df-qus 17589 df-mre 17664 df-mrc 17665 df-acs 17667 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-mhm 18838 df-submnd 18839 df-grp 18996 df-minusg 18997 df-sbg 18998 df-mulg 19128 df-subg 19183 df-nsg 19184 df-eqg 19185 df-ghm 19273 df-cntz 19377 df-oppg 19406 df-lsm 19698 df-cmn 19844 df-abl 19845 df-mgp 20182 df-rng 20200 df-ur 20229 df-ring 20282 df-cring 20283 df-oppr 20380 df-dvdsr 20403 df-unit 20404 df-invr 20434 df-nzr 20559 df-subrg 20617 df-drng 20773 df-field 20774 df-lmod 20902 df-lss 20973 df-lsp 21013 df-lmhm 21064 df-lbs 21117 df-sra 21215 df-rgmod 21216 df-lidl 21261 df-rsp 21262 df-2idl 21303 df-dsmm 21795 df-frlm 21810 df-uvc 21846 df-mxidl 33473 |
This theorem is referenced by: mxidlprmALT 33512 |
Copyright terms: Public domain | W3C validator |