Metamath Proof Explorer

Theorem 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 ∈ Fld ↔ K ∈ CRingOps ∧ U ≠ Z ∧ 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 fldcrng ⊢ K ∈ Fld → K ∈ CRingOps
7 flddivrng ⊢ K ∈ Fld → K ∈ DivRingOps
8 1 2 3 4 5 dvrunz ⊢ K ∈ DivRingOps → U ≠ Z
9 7 8 syl ⊢ K ∈ Fld → U ≠ Z
10 1 2 3 4 divrngidl ⊢ K ∈ DivRingOps → Idl ⁡ K = Z X
11 7 10 syl ⊢ K ∈ Fld → Idl ⁡ K = Z X
12 6 9 11 3jca ⊢ K ∈ Fld → K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X
13 crngorngo ⊢ K ∈ CRingOps → K ∈ RingOps
14 13 3ad2ant1 ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → K ∈ RingOps
15 simp2 ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → U ≠ 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 ∈ RingOps → U ∈ X
19 13 18 syl ⊢ K ∈ CRingOps → U ∈ X
20 19 ad2antrr ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → U ∈ X
21 eldif ⊢ x ∈ X ∖ Z ↔ x ∈ X ∧ ¬ x ∈ Z
22 snssi ⊢ x ∈ X → x ⊆ X
23 1 3 igenss ⊢ K ∈ RingOps ∧ x ⊆ X → x ⊆ K IdlGen x
24 22 23 sylan2 ⊢ K ∈ RingOps ∧ x ∈ X → x ⊆ K IdlGen x
25 vex ⊢ x ∈ V
26 25 snss ⊢ x ∈ K IdlGen x ↔ x ⊆ K IdlGen x
27 26 biimpri ⊢ x ⊆ K IdlGen x → x ∈ K IdlGen x
28 eleq2 ⊢ K IdlGen x = Z → x ∈ K IdlGen x ↔ x ∈ Z
29 27 28 syl5ibcom ⊢ x ⊆ K IdlGen x → K IdlGen x = Z → x ∈ Z
30 29 con3dimp ⊢ x ⊆ K IdlGen x ∧ ¬ x ∈ Z → ¬ K IdlGen x = Z
31 24 30 sylan ⊢ K ∈ RingOps ∧ x ∈ X ∧ ¬ x ∈ Z → ¬ K IdlGen x = Z
32 31 anasss ⊢ K ∈ RingOps ∧ x ∈ X ∧ ¬ x ∈ Z → ¬ K IdlGen x = Z
33 21 32 sylan2b ⊢ K ∈ RingOps ∧ x ∈ X ∖ Z → ¬ K IdlGen x = Z
34 33 adantlr ⊢ K ∈ RingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → ¬ K IdlGen x = Z
35 eldifi ⊢ x ∈ X ∖ Z → x ∈ X
36 35 snssd ⊢ x ∈ X ∖ Z → x ⊆ X
37 1 3 igenidl ⊢ K ∈ RingOps ∧ x ⊆ X → K IdlGen x ∈ Idl ⁡ K
38 36 37 sylan2 ⊢ K ∈ RingOps ∧ x ∈ X ∖ Z → K IdlGen x ∈ Idl ⁡ K
39 eleq2 ⊢ Idl ⁡ K = Z X → K IdlGen x ∈ Idl ⁡ K ↔ K IdlGen x ∈ Z X
40 38 39 syl5ibcom ⊢ K ∈ RingOps ∧ x ∈ X ∖ Z → Idl ⁡ K = Z X → K IdlGen x ∈ Z X
41 40 imp ⊢ K ∈ RingOps ∧ x ∈ X ∖ Z ∧ Idl ⁡ K = Z X → K IdlGen x ∈ Z X
42 41 an32s ⊢ K ∈ RingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → K IdlGen x ∈ Z X
43 ovex ⊢ K IdlGen x ∈ V
44 43 elpr ⊢ K IdlGen x ∈ Z X ↔ K IdlGen x = Z ∨ K IdlGen x = X
45 42 44 sylib ⊢ K ∈ RingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → K IdlGen x = Z ∨ K IdlGen x = X
46 45 ord ⊢ K ∈ RingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → ¬ K IdlGen x = Z → K IdlGen x = X
47 34 46 mpd ⊢ K ∈ RingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → K IdlGen x = X
48 13 47 sylanl1 ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → K IdlGen x = X
49 1 2 3 prnc ⊢ K ∈ CRingOps ∧ x ∈ X → K IdlGen x = z ∈ X | ∃ y ∈ X z = y H x
50 35 49 sylan2 ⊢ K ∈ CRingOps ∧ x ∈ X ∖ Z → K IdlGen x = z ∈ X | ∃ y ∈ X z = y H x
51 50 adantlr ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → K IdlGen x = z ∈ X | ∃ y ∈ X z = y H x
52 48 51 eqtr3d ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → X = z ∈ X | ∃ y ∈ X z = y H x
53 20 52 eleqtrd ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → U ∈ z ∈ X | ∃ y ∈ X z = y H x
54 eqeq1 ⊢ z = U → z = y H x ↔ U = y H x
55 54 rexbidv ⊢ z = U → ∃ y ∈ X z = y H x ↔ ∃ y ∈ X U = y H x
56 55 elrab ⊢ U ∈ z ∈ X | ∃ y ∈ X z = y H x ↔ U ∈ X ∧ ∃ y ∈ X U = y H x
57 53 56 sylib ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → U ∈ X ∧ ∃ y ∈ X U = y H x
58 57 simprd ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → ∃ y ∈ X U = y H x
59 eqcom ⊢ y H x = U ↔ U = y H x
60 59 rexbii ⊢ ∃ y ∈ X y H x = U ↔ ∃ y ∈ X U = y H x
61 58 60 sylibr ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X ∧ x ∈ X ∖ Z → ∃ y ∈ X y H x = U
62 61 ralrimiva ⊢ K ∈ CRingOps ∧ Idl ⁡ K = Z X → ∀ x ∈ X ∖ Z ∃ y ∈ X y H x = U
63 62 3adant2 ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → ∀ x ∈ X ∖ Z ∃ y ∈ X y H x = U
64 14 15 63 jca32 ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → K ∈ RingOps ∧ U ≠ Z ∧ ∀ x ∈ X ∖ Z ∃ y ∈ X y H x = U
65 1 2 4 3 5 isdrngo3 ⊢ K ∈ DivRingOps ↔ K ∈ RingOps ∧ U ≠ Z ∧ ∀ x ∈ X ∖ Z ∃ y ∈ X y H x = U
66 64 65 sylibr ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → K ∈ DivRingOps
67 simp1 ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → K ∈ CRingOps
68 isfld2 ⊢ K ∈ Fld ↔ K ∈ DivRingOps ∧ K ∈ CRingOps
69 66 67 68 sylanbrc ⊢ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X → K ∈ Fld
70 12 69 impbii ⊢ K ∈ Fld ↔ K ∈ CRingOps ∧ U ≠ Z ∧ Idl ⁡ K = Z X