Metamath Proof Explorer

Theorem isfld2

Description: The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion isfld2 ⊢ K ∈ Fld ↔ K ∈ DivRingOps ∧ K ∈ CRingOps

Proof

Step Hyp Ref Expression
1 flddivrng ⊢ K ∈ Fld → K ∈ DivRingOps
2 fldcrng ⊢ K ∈ Fld → K ∈ CRingOps
3 1 2 jca ⊢ K ∈ Fld → K ∈ DivRingOps ∧ K ∈ CRingOps
4 iscrngo ⊢ K ∈ CRingOps ↔ K ∈ RingOps ∧ K ∈ Com2
5 4 simprbi ⊢ K ∈ CRingOps → K ∈ Com2
6 elin ⊢ K ∈ DivRingOps ∩ Com2 ↔ K ∈ DivRingOps ∧ K ∈ Com2
7 6 biimpri ⊢ K ∈ DivRingOps ∧ K ∈ Com2 → K ∈ DivRingOps ∩ Com2
8 df-fld ⊢ Fld = DivRingOps ∩ Com2
9 7 8 eleqtrrdi ⊢ K ∈ DivRingOps ∧ K ∈ Com2 → K ∈ Fld
10 5 9 sylan2 ⊢ K ∈ DivRingOps ∧ K ∈ CRingOps → K ∈ Fld
11 3 10 impbii ⊢ K ∈ Fld ↔ K ∈ DivRingOps ∧ K ∈ CRingOps