isfldidl

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

	Ref	Expression
Hypotheses	isfldidl.1	$⊢ G = 1^{st} (K)$
	isfldidl.2	$⊢ H = 2^{nd} (K)$
	isfldidl.3	$⊢ X = ran G$
	isfldidl.4	$⊢ Z = GId (G)$
	isfldidl.5	$⊢ U = GId (H)$
Assertion	isfldidl	$⊢ K \in Fld \leftrightarrow (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\})$

Proof

Step	Hyp	Ref	Expression
1		isfldidl.1	$⊢ G = 1^{st} (K)$
2		isfldidl.2	$⊢ H = 2^{nd} (K)$
3		isfldidl.3	$⊢ X = ran G$
4		isfldidl.4	$⊢ Z = GId (G)$
5		isfldidl.5	$⊢ U = GId (H)$
6		fldcrngo	$⊢ K \in Fld \to K \in CRingOps$
7		flddivrng	$⊢ K \in Fld \to K \in DivRingOps$
8	1 2 3 4 5	dvrunz	$⊢ K \in DivRingOps \to U \neq Z$
9	7 8	syl	$⊢ K \in Fld \to U \neq Z$
10	1 2 3 4	divrngidl	$⊢ K \in DivRingOps \to Idl (K) = \{\{Z\}, X\}$
11	7 10	syl	$⊢ K \in Fld \to Idl (K) = \{\{Z\}, X\}$
12	6 9 11	3jca	$⊢ K \in Fld \to (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\})$
13		crngorngo	$⊢ K \in CRingOps \to K \in RingOps$
14	13	3ad2ant1	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to K \in RingOps$
15		simp2	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to U \neq Z$
16	1	rneqi	$⊢ ran G = ran 1^{st} (K)$
17	3 16	eqtri	$⊢ X = ran 1^{st} (K)$
18	17 2 5	rngo1cl	$⊢ K \in RingOps \to U \in X$
19	13 18	syl	$⊢ K \in CRingOps \to U \in X$
20	19	ad2antrr	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to U \in X$
21		eldif	$⊢ x \in (X ∖ \{Z\}) \leftrightarrow (x \in X \land \neg x \in \{Z\})$
22		snssi	$⊢ x \in X \to \{x\} \subseteq X$
23	1 3	igenss	$⊢ (K \in RingOps \land \{x\} \subseteq X) \to \{x\} \subseteq K IdlGen \{x\}$
24	22 23	sylan2	$⊢ (K \in RingOps \land x \in X) \to \{x\} \subseteq K IdlGen \{x\}$
25		vex	$⊢ x \in V$
26	25	snss	$⊢ x \in (K IdlGen \{x\}) \leftrightarrow \{x\} \subseteq K IdlGen \{x\}$
27	26	biimpri	$⊢ \{x\} \subseteq K IdlGen \{x\} \to x \in (K IdlGen \{x\})$
28		eleq2	$⊢ K IdlGen \{x\} = \{Z\} \to (x \in (K IdlGen \{x\}) \leftrightarrow x \in \{Z\})$
29	27 28	syl5ibcom	$⊢ \{x\} \subseteq K IdlGen \{x\} \to (K IdlGen \{x\} = \{Z\} \to x \in \{Z\})$
30	29	con3dimp	$⊢ (\{x\} \subseteq K IdlGen \{x\} \land \neg x \in \{Z\}) \to \neg K IdlGen \{x\} = \{Z\}$
31	24 30	sylan	$⊢ ((K \in RingOps \land x \in X) \land \neg x \in \{Z\}) \to \neg K IdlGen \{x\} = \{Z\}$
32	31	anasss	$⊢ (K \in RingOps \land (x \in X \land \neg x \in \{Z\})) \to \neg K IdlGen \{x\} = \{Z\}$
33	21 32	sylan2b	$⊢ (K \in RingOps \land x \in (X ∖ \{Z\})) \to \neg K IdlGen \{x\} = \{Z\}$
34	33	adantlr	$⊢ ((K \in RingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to \neg K IdlGen \{x\} = \{Z\}$
35		eldifi	$⊢ x \in (X ∖ \{Z\}) \to x \in X$
36	35	snssd	$⊢ x \in (X ∖ \{Z\}) \to \{x\} \subseteq X$
37	1 3	igenidl	$⊢ (K \in RingOps \land \{x\} \subseteq X) \to K IdlGen \{x\} \in Idl (K)$
38	36 37	sylan2	$⊢ (K \in RingOps \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} \in Idl (K)$
39		eleq2	$⊢ Idl (K) = \{\{Z\}, X\} \to (K IdlGen \{x\} \in Idl (K) \leftrightarrow K IdlGen \{x\} \in \{\{Z\}, X\})$
40	38 39	syl5ibcom	$⊢ (K \in RingOps \land x \in (X ∖ \{Z\})) \to (Idl (K) = \{\{Z\}, X\} \to K IdlGen \{x\} \in \{\{Z\}, X\})$
41	40	imp	$⊢ ((K \in RingOps \land x \in (X ∖ \{Z\})) \land Idl (K) = \{\{Z\}, X\}) \to K IdlGen \{x\} \in \{\{Z\}, X\}$
42	41	an32s	$⊢ ((K \in RingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} \in \{\{Z\}, X\}$
43		ovex	$⊢ K IdlGen \{x\} \in V$
44	43	elpr	$⊢ K IdlGen \{x\} \in \{\{Z\}, X\} \leftrightarrow (K IdlGen \{x\} = \{Z\} \lor K IdlGen \{x\} = X)$
45	42 44	sylib	$⊢ ((K \in RingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to (K IdlGen \{x\} = \{Z\} \lor K IdlGen \{x\} = X)$
46	45	ord	$⊢ ((K \in RingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to (\neg K IdlGen \{x\} = \{Z\} \to K IdlGen \{x\} = X)$
47	34 46	mpd	$⊢ ((K \in RingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} = X$
48	13 47	sylanl1	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} = X$
49	1 2 3	prnc	$⊢ (K \in CRingOps \land x \in X) \to K IdlGen \{x\} = \{z \in X \| \exists y \in X z = y H x\}$
50	35 49	sylan2	$⊢ (K \in CRingOps \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} = \{z \in X \| \exists y \in X z = y H x\}$
51	50	adantlr	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to K IdlGen \{x\} = \{z \in X \| \exists y \in X z = y H x\}$
52	48 51	eqtr3d	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to X = \{z \in X \| \exists y \in X z = y H x\}$
53	20 52	eleqtrd	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to U \in \{z \in X \| \exists y \in X z = y H x\}$
54		eqeq1	$⊢ z = U \to (z = y H x \leftrightarrow U = y H x)$
55	54	rexbidv	$⊢ z = U \to (\exists y \in X z = y H x \leftrightarrow \exists y \in X U = y H x)$
56	55	elrab	$⊢ U \in \{z \in X \| \exists y \in X z = y H x\} \leftrightarrow (U \in X \land \exists y \in X U = y H x)$
57	53 56	sylib	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to (U \in X \land \exists y \in X U = y H x)$
58	57	simprd	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to \exists y \in X U = y H x$
59		eqcom	$⊢ y H x = U \leftrightarrow U = y H x$
60	59	rexbii	$⊢ \exists y \in X y H x = U \leftrightarrow \exists y \in X U = y H x$
61	58 60	sylibr	$⊢ ((K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \land x \in (X ∖ \{Z\})) \to \exists y \in X y H x = U$
62	61	ralrimiva	$⊢ (K \in CRingOps \land Idl (K) = \{\{Z\}, X\}) \to \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U$
63	62	3adant2	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U$
64	14 15 63	jca32	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to (K \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$
65	1 2 4 3 5	isdrngo3	$⊢ K \in DivRingOps \leftrightarrow (K \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$
66	64 65	sylibr	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to K \in DivRingOps$
67		simp1	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to K \in CRingOps$
68		isfld2	$⊢ K \in Fld \leftrightarrow (K \in DivRingOps \land K \in CRingOps)$
69	66 67 68	sylanbrc	$⊢ (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\}) \to K \in Fld$
70	12 69	impbii	$⊢ K \in Fld \leftrightarrow (K \in CRingOps \land U \neq Z \land Idl (K) = \{\{Z\}, X\})$

Metamath Proof Explorer

Theorem isfldidl

Proof