Metamath Proof Explorer

Theorem isfld2

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

Ref Expression
Assertion isfld2 
|- ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )

Proof

Step Hyp Ref Expression
1 flddivrng 
 |-  ( K e. Fld -> K e. DivRingOps )
2 fldcrngo 
 |-  ( K e. Fld -> K e. CRingOps )
3 1 2 jca 
 |-  ( K e. Fld -> ( K e. DivRingOps /\ K e. CRingOps ) )
4 iscrngo 
 |-  ( K e. CRingOps <-> ( K e. RingOps /\ K e. Com2 ) )
5 4 simprbi 
 |-  ( K e. CRingOps -> K e. Com2 )
6 elin 
 |-  ( K e. ( DivRingOps i^i Com2 ) <-> ( K e. DivRingOps /\ K e. Com2 ) )
7 6 biimpri 
 |-  ( ( K e. DivRingOps /\ K e. Com2 ) -> K e. ( DivRingOps i^i Com2 ) )
8 df-fld 
 |-  Fld = ( DivRingOps i^i Com2 )
9 7 8 eleqtrrdi 
 |-  ( ( K e. DivRingOps /\ K e. Com2 ) -> K e. Fld )
10 5 9 sylan2 
 |-  ( ( K e. DivRingOps /\ K e. CRingOps ) -> K e. Fld )
11 3 10 impbii 
 |-  ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )