Theorem isfldidl 26568

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)

Hypotheses

Ref	Expression
isfldidl.1	|- G = ( 1st ` K )
isfldidl.2	|- H = ( 2nd ` K )
isfldidl.3	|- X = ran G
isfldidl.4	|- Z = (GId ` G )
isfldidl.5	|- U = (GId ` H )

Assertion

Ref	Expression
isfldidl	|- ( K e. Fld <-> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )

Proof of Theorem isfldidl

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldcrng 26504	. . 3 |- ( K e. Fld -> K e. CRingOps )
2		flddivrng 21956	. . . 4 |- ( K e. Fld -> K e. DivRingOps )
3		isfldidl.1	. . . . 5 |- G = ( 1st ` K )
4		isfldidl.2	. . . . 5 |- H = ( 2nd ` K )
5		isfldidl.3	. . . . 5 |- X = ran G
6		isfldidl.4	. . . . 5 |- Z = (GId ` G )
7		isfldidl.5	. . . . 5 |- U = (GId ` H )
8	3, 4, 5, 6, 7	dvrunz 21974	. . . 4 |- ( K e. DivRingOps -> U =/= Z )
9	2, 8	syl 16	. . 3 |- ( K e. Fld -> U =/= Z )
10	3, 4, 5, 6	divrngidl 26528	. . . 4 |- ( K e. DivRingOps -> ( Idl ` K ) = { { Z } , X } )
11	2, 10	syl 16	. . 3 |- ( K e. Fld -> ( Idl ` K ) = { { Z } , X } )
12	1, 9, 11	3jca 1134	. 2 |- ( K e. Fld -> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )
13		crngorngo 26500	. . . . . 6 |- ( K e. CRingOps -> K e. RingOps )
14	13	3ad2ant1 978	. . . . 5 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. RingOps )
15		simp2 958	. . . . 5 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> U =/= Z )
16	3	rneqi 5055	. . . . . . . . . . . . . . 15 |- ran G = ran ( 1st ` K )
17	5, 16	eqtri 2424	. . . . . . . . . . . . . 14 |- X = ran ( 1st ` K )
18	17, 4, 7	rngo1cl 21970	. . . . . . . . . . . . 13 |- ( K e. RingOps -> U e. X )
19	13, 18	syl 16	. . . . . . . . . . . 12 |- ( K e. CRingOps -> U e. X )
20	19	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> U e. X )
21		eldif 3290	. . . . . . . . . . . . . . . 16 |- ( x e. ( X \ { Z } ) <-> ( x e. X /\ -. x e. { Z } ) )
22		snssi 3902	. . . . . . . . . . . . . . . . . . 19 |- ( x e. X -> { x } C_ X )
23	3, 5	igenss 26562	. . . . . . . . . . . . . . . . . . 19 |- ( ( K e. RingOps /\ { x } C_ X ) -> { x } C_ ( K IdlGen { x } ) )
24	22, 23	sylan2 461	. . . . . . . . . . . . . . . . . 18 |- ( ( K e. RingOps /\ x e. X ) -> { x } C_ ( K IdlGen { x } ) )
25		vex 2919	. . . . . . . . . . . . . . . . . . . . . 22 |- x e. _V
26	25	snss 3886	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( K IdlGen { x } ) <-> { x } C_ ( K IdlGen { x } ) )
27	26	biimpri 198	. . . . . . . . . . . . . . . . . . . 20 |- ( { x } C_ ( K IdlGen { x } ) -> x e. ( K IdlGen { x } ) )
28		eleq2 2465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( K IdlGen { x } ) = { Z } -> ( x e. ( K IdlGen { x } ) <-> x e. { Z } ) )
29	27, 28	syl5ibcom 212	. . . . . . . . . . . . . . . . . . 19 |- ( { x } C_ ( K IdlGen { x } ) -> ( ( K IdlGen { x } ) = { Z } -> x e. { Z } ) )
30	29	con3and 429	. . . . . . . . . . . . . . . . . 18 |- ( ( { x } C_ ( K IdlGen { x } ) /\ -. x e. { Z } ) -> -. ( K IdlGen { x } ) = { Z } )
31	24, 30	sylan 458	. . . . . . . . . . . . . . . . 17 |- ( ( ( K e. RingOps /\ x e. X ) /\ -. x e. { Z } ) -> -. ( K IdlGen { x } ) = { Z } )
32	31	anasss 629	. . . . . . . . . . . . . . . 16 |- ( ( K e. RingOps /\ ( x e. X /\ -. x e. { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
33	21, 32	sylan2b 462	. . . . . . . . . . . . . . 15 |- ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
34	33	adantlr 696	. . . . . . . . . . . . . 14 |- ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
35		eldifi 3429	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( X \ { Z } ) -> x e. X )
36	35	snssd 3903	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( X \ { Z } ) -> { x } C_ X )
37	3, 5	igenidl 26563	. . . . . . . . . . . . . . . . . . . 20 |- ( ( K e. RingOps /\ { x } C_ X ) -> ( K IdlGen { x } ) e. ( Idl ` K ) )
38	36, 37	sylan2 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) e. ( Idl ` K ) )
39		eleq2 2465	. . . . . . . . . . . . . . . . . . 19 |- ( ( Idl ` K ) = { { Z } , X } -> ( ( K IdlGen { x } ) e. ( Idl ` K ) <-> ( K IdlGen { x } ) e. { { Z } , X } ) )
40	38, 39	syl5ibcom 212	. . . . . . . . . . . . . . . . . 18 |- ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> ( ( Idl ` K ) = { { Z } , X } -> ( K IdlGen { x } ) e. { { Z } , X } ) )
41	40	imp 419	. . . . . . . . . . . . . . . . 17 |- ( ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) /\ ( Idl ` K ) = { { Z } , X } ) -> ( K IdlGen { x } ) e. { { Z } , X } )
42	41	an32s 780	. . . . . . . . . . . . . . . 16 |- ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) e. { { Z } , X } )
43		ovex 6065	. . . . . . . . . . . . . . . . 17 |- ( K IdlGen { x } ) e. _V
44	43	elpr 3792	. . . . . . . . . . . . . . . 16 |- ( ( K IdlGen { x } ) e. { { Z } , X } <-> ( ( K IdlGen { x } ) = { Z } \/ ( K IdlGen { x } ) = X ) )
45	42, 44	sylib 189	. . . . . . . . . . . . . . 15 |- ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( ( K IdlGen { x } ) = { Z } \/ ( K IdlGen { x } ) = X ) )
46	45	ord 367	. . . . . . . . . . . . . 14 |- ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( -. ( K IdlGen { x } ) = { Z } -> ( K IdlGen { x } ) = X ) )
47	34, 46	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = X )
48	13, 47	sylanl1 632	. . . . . . . . . . . 12 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = X )
49	3, 4, 5	prnc 26567	. . . . . . . . . . . . . 14 |- ( ( K e. CRingOps /\ x e. X ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
50	35, 49	sylan2 461	. . . . . . . . . . . . 13 |- ( ( K e. CRingOps /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
51	50	adantlr 696	. . . . . . . . . . . 12 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
52	48, 51	eqtr3d 2438	. . . . . . . . . . 11 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> X = { z e. X | E. y e. X z = ( y H x ) } )
53	20, 52	eleqtrd 2480	. . . . . . . . . 10 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> U e. { z e. X | E. y e. X z = ( y H x ) } )
54		eqeq1 2410	. . . . . . . . . . . 12 |- ( z = U -> ( z = ( y H x ) <-> U = ( y H x ) ) )
55	54	rexbidv 2687	. . . . . . . . . . 11 |- ( z = U -> ( E. y e. X z = ( y H x ) <-> E. y e. X U = ( y H x ) ) )
56	55	elrab 3052	. . . . . . . . . 10 |- ( U e. { z e. X | E. y e. X z = ( y H x ) } <-> ( U e. X /\ E. y e. X U = ( y H x ) ) )
57	53, 56	sylib 189	. . . . . . . . 9 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( U e. X /\ E. y e. X U = ( y H x ) ) )
58	57	simprd 450	. . . . . . . 8 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> E. y e. X U = ( y H x ) )
59		eqcom 2406	. . . . . . . . 9 |- ( ( y H x ) = U <-> U = ( y H x ) )
60	59	rexbii 2691	. . . . . . . 8 |- ( E. y e. X ( y H x ) = U <-> E. y e. X U = ( y H x ) )
61	58, 60	sylibr 204	. . . . . . 7 |- ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> E. y e. X ( y H x ) = U )
62	61	ralrimiva 2749	. . . . . 6 |- ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) -> A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U )
63	62	3adant2 976	. . . . 5 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U )
64	14, 15, 63	jca32 522	. . . 4 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> ( K e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
65	3, 4, 6, 5, 7	isdrngo3 26465	. . . 4 |- ( K e. DivRingOps <-> ( K e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
66	64, 65	sylibr 204	. . 3 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. DivRingOps )
67		simp1 957	. . 3 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. CRingOps )
68		isfld2 26505	. . 3 |- ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )
69	66, 67, 68	sylanbrc 646	. 2 |- ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. Fld )
70	12, 69	impbii 181	1 |- ( K e. Fld <-> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )

Syntax hints:   -. wn 3   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   \ cdif 3277   C_ wss 3280   {csn 3774   {cpr 3775   ran crn 4838   ` cfv 5413  (class class class)co 6040   1stc1st 6306   2ndc2nd 6307  GIdcgi 21728   RingOpscrngo 21916   DivRingOpscdrng 21946   Fldcfld 21954  CRingOpsccring 26495   Idlcidl 26507   IdlGen cigen 26559

This theorem is referenced by:  isfldidl2  26569

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-1o 6683  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-grpo 21732  df-gid 21733  df-ginv 21734  df-ablo 21823  df-ass 21854  df-exid 21856  df-mgm 21860  df-sgr 21872  df-mndo 21879  df-rngo 21917  df-drngo 21947  df-com2 21952  df-fld 21955  df-crngo 26496  df-idl 26510  df-igen 26560