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=1st⁡K
isfldidl2.2 ⊢H=2nd⁡K
isfldidl2.3 ⊢X=ran⁡G
isfldidl2.4 ⊢Z=GId⁡G
Assertion isfldidl2 ⊢K∈Fld↔K∈CRingOps∧X≠Z∧Idl⁡K=ZX

Proof

Step Hyp Ref Expression
1 isfldidl2.1 ⊢G=1st⁡K
2 isfldidl2.2 ⊢H=2nd⁡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=ZX
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=ZX↔X≠Z∧Idl⁡K=ZX
14 13 pm5.32i ⊢K∈CRingOps∧GId⁡H≠Z∧Idl⁡K=ZX↔K∈CRingOps∧X≠Z∧Idl⁡K=ZX
15 3anass ⊢K∈CRingOps∧GId⁡H≠Z∧Idl⁡K=ZX↔K∈CRingOps∧GId⁡H≠Z∧Idl⁡K=ZX
16 3anass ⊢K∈CRingOps∧X≠Z∧Idl⁡K=ZX↔K∈CRingOps∧X≠Z∧Idl⁡K=ZX
17 14 15 16 3bitr4i ⊢K∈CRingOps∧GId⁡H≠Z∧Idl⁡K=ZX↔K∈CRingOps∧X≠Z∧Idl⁡K=ZX
18 6 17 bitri ⊢K∈Fld↔K∈CRingOps∧X≠Z∧Idl⁡K=ZX