isfldidl - Mathbox for Jeff Madsen

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

Theorem isfldidl 38389

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

**Hypotheses**
Ref	Expression
isfldidl.1	⊢ 𝐺 = (1^st ‘𝐾)
isfldidl.2	⊢ 𝐻 = (2^nd ‘𝐾)
isfldidl.3	⊢ 𝑋 = ran 𝐺
isfldidl.4	⊢ 𝑍 = (GId‘𝐺)
isfldidl.5	⊢ 𝑈 = (GId‘𝐻)

**Assertion**
Ref	Expression
isfldidl	⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))

Proof of Theorem isfldidl Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldcrngo 38325	. . 3 ⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps)
2		flddivrng 38320	. . . 4 ⊢ (𝐾 ∈ Fld → 𝐾 ∈ DivRingOps)
3		isfldidl.1	. . . . 5 ⊢ 𝐺 = (1^st ‘𝐾)
4		isfldidl.2	. . . . 5 ⊢ 𝐻 = (2^nd ‘𝐾)
5		isfldidl.3	. . . . 5 ⊢ 𝑋 = ran 𝐺
6		isfldidl.4	. . . . 5 ⊢ 𝑍 = (GId‘𝐺)
7		isfldidl.5	. . . . 5 ⊢ 𝑈 = (GId‘𝐻)
8	3, 4, 5, 6, 7	dvrunz 38275	. . . 4 ⊢ (𝐾 ∈ DivRingOps → 𝑈 ≠ 𝑍)
9	2, 8	syl 17	. . 3 ⊢ (𝐾 ∈ Fld → 𝑈 ≠ 𝑍)
10	3, 4, 5, 6	divrngidl 38349	. . . 4 ⊢ (𝐾 ∈ DivRingOps → (Idl‘𝐾) = {{𝑍}, 𝑋})
11	2, 10	syl 17	. . 3 ⊢ (𝐾 ∈ Fld → (Idl‘𝐾) = {{𝑍}, 𝑋})
12	1, 9, 11	3jca 1129	. 2 ⊢ (𝐾 ∈ Fld → (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
13		crngorngo 38321	. . . . . 6 ⊢ (𝐾 ∈ CRingOps → 𝐾 ∈ RingOps)
14	13	3ad2ant1 1134	. . . . 5 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ RingOps)
15		simp2 1138	. . . . 5 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝑈 ≠ 𝑍)
16	3	rneqi 5893	. . . . . . . . . . . . . . 15 ⊢ ran 𝐺 = ran (1^st ‘𝐾)
17	5, 16	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ran (1^st ‘𝐾)
18	17, 4, 7	rngo1cl 38260	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ RingOps → 𝑈 ∈ 𝑋)
19	13, 18	syl 17	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ CRingOps → 𝑈 ∈ 𝑋)
20	19	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈 ∈ 𝑋)
21		eldif 3900	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ {𝑍}))
22		snssi 4730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑋 → {𝑥} ⊆ 𝑋)
23	3, 5	igenss 38383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
24	22, 23	sylan2 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
25		vex 3434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑥 ∈ V
26	25	snss 4729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
27	26	biimpri 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → 𝑥 ∈ (𝐾 IdlGen {𝑥}))
28		eleq2 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 IdlGen {𝑥}) = {𝑍} → (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ 𝑥 ∈ {𝑍}))
29	27, 28	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → ((𝐾 IdlGen {𝑥}) = {𝑍} → 𝑥 ∈ {𝑍}))
30	29	con3dimp 408	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑥} ⊆ (𝐾 IdlGen {𝑥}) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
31	24, 30	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
32	31	anasss 466	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ RingOps ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
33	21, 32	sylan2b 595	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
34	33	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
35		eldifi 4072	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → 𝑥 ∈ 𝑋)
36	35	snssd 4731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → {𝑥} ⊆ 𝑋)
37	3, 5	igenidl 38384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾))
38	36, 37	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾))
39		eleq2 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Idl‘𝐾) = {{𝑍}, 𝑋} → ((𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾) ↔ (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}))
40	38, 39	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((Idl‘𝐾) = {{𝑍}, 𝑋} → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}))
41	40	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})
42	41	an32s 653	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})
43		ovex 7400	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 IdlGen {𝑥}) ∈ V
44	43	elpr 4593	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋} ↔ ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋))
45	42, 44	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋))
46	45	ord 865	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (¬ (𝐾 IdlGen {𝑥}) = {𝑍} → (𝐾 IdlGen {𝑥}) = 𝑋))
47	34, 46	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋)
48	13, 47	sylanl1 681	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋)
49	3, 4, 5	prnc 38388	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑥 ∈ 𝑋) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)})
50	35, 49	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)})
51	50	adantlr 716	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)})
52	48, 51	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)})
53	20, 52	eleqtrd 2839	. . . . . . . . . 10 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈 ∈ {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)})
54		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑈 → (𝑧 = (𝑦𝐻𝑥) ↔ 𝑈 = (𝑦𝐻𝑥)))
55	54	rexbidv 3162	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → (∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥) ↔ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥)))
56	55	elrab 3635	. . . . . . . . . 10 ⊢ (𝑈 ∈ {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)} ↔ (𝑈 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥)))
57	53, 56	sylib 218	. . . . . . . . 9 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑈 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥)))
58	57	simprd 495	. . . . . . . 8 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥))
59		eqcom 2744	. . . . . . . . 9 ⊢ ((𝑦𝐻𝑥) = 𝑈 ↔ 𝑈 = (𝑦𝐻𝑥))
60	59	rexbii 3085	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥))
61	58, 60	sylibr 234	. . . . . . 7 ⊢ (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)
62	61	ralrimiva 3130	. . . . . 6 ⊢ ((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)
63	62	3adant2 1132	. . . . 5 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)
64	14, 15, 63	jca32 515	. . . 4 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
65	3, 4, 6, 5, 7	isdrngo3 38280	. . . 4 ⊢ (𝐾 ∈ DivRingOps ↔ (𝐾 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
66	64, 65	sylibr 234	. . 3 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ DivRingOps)
67		simp1 1137	. . 3 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ CRingOps)
68		isfld2 38326	. . 3 ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps))
69	66, 67, 68	sylanbrc 584	. 2 ⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ Fld)
70	12, 69	impbii 209	1 ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 ∖ cdif 3887 ⊆ wss 3890 {csn 4568 {cpr 4570 ran crn 5632 ‘cfv 6499 (class class class)co 7367 1^st c1st 7940 2^nd c2nd 7941 GIdcgi 30561 RingOpscrngo 38215 DivRingOpscdrng 38269 Fldcfld 38312 CRingOpsccring 38314 Idlcidl 38328 IdlGen cigen 38380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-1o 8405 df-en 8894 df-grpo 30564 df-gid 30565 df-ginv 30566 df-ablo 30616 df-ass 38164 df-exid 38166 df-mgmOLD 38170 df-sgrOLD 38182 df-mndo 38188 df-rngo 38216 df-drngo 38270 df-com2 38311 df-fld 38313 df-crngo 38315 df-idl 38331 df-igen 38381

This theorem is referenced by: isfldidl2 38390

W3C validator