Metamath Proof Explorer

Theorem isfldidl2

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses isfldidl2.1 ⊢ G = 1 st ⁡ K
isfldidl2.2 ⊢ H = 2 nd ⁡ K
isfldidl2.3 ⊢ X = ran ⁡ G
isfldidl2.4 ⊢ Z = GId ⁡ G
Assertion isfldidl2 ⊢ K ∈ Fld ↔ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X

Proof

Step Hyp Ref Expression
1 isfldidl2.1 ⊢ G = 1 st ⁡ K
2 isfldidl2.2 ⊢ H = 2 nd ⁡ K
3 isfldidl2.3 ⊢ X = ran ⁡ G
4 isfldidl2.4 ⊢ Z = GId ⁡ G
5 eqid ⊢ GId ⁡ H = GId ⁡ H
6 1 2 3 4 5 isfldidl ⊢ K ∈ Fld ↔ K ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X
7 crngorngo ⊢ K ∈ CRingOps → K ∈ RingOps
8 eqcom ⊢ GId ⁡ H = Z ↔ Z = GId ⁡ H
9 1 2 3 4 5 0rngo ⊢ K ∈ RingOps → Z = GId ⁡ H ↔ X = Z
10 8 9 bitrid ⊢ K ∈ RingOps → GId ⁡ H = Z ↔ X = Z
11 7 10 syl ⊢ K ∈ CRingOps → GId ⁡ H = Z ↔ X = Z
12 11 necon3bid ⊢ K ∈ CRingOps → GId ⁡ H ≠ Z ↔ X ≠ Z
13 12 anbi1d ⊢ K ∈ CRingOps → GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X ↔ X ≠ Z ∧ Idl ⁡ K = Z X
14 13 pm5.32i ⊢ K ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X ↔ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X
15 3anass ⊢ K ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X ↔ K ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X
16 3anass ⊢ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X ↔ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X
17 14 15 16 3bitr4i ⊢ K ∈ CRingOps ∧ GId ⁡ H ≠ Z ∧ Idl ⁡ K = Z X ↔ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X
18 6 17 bitri ⊢ K ∈ Fld ↔ K ∈ CRingOps ∧ X ≠ Z ∧ Idl ⁡ K = Z X