Metamath Proof Explorer

Theorem fldcrng

Description: A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Assertion fldcrng 
|- ( K e. Fld -> K e. CRingOps )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` K ) = ( 1st ` K )
2 eqid 
 |-  ( 2nd ` K ) = ( 2nd ` K )
3 eqid 
 |-  ran ( 1st ` K ) = ran ( 1st ` K )
4 eqid 
 |-  ( GId ` ( 1st ` K ) ) = ( GId ` ( 1st ` K ) )
5 1 2 3 4 drngoi 
 |-  ( K e. DivRingOps -> ( K e. RingOps /\ ( ( 2nd ` K ) |` ( ( ran ( 1st ` K ) \ { ( GId ` ( 1st ` K ) ) } ) X. ( ran ( 1st ` K ) \ { ( GId ` ( 1st ` K ) ) } ) ) ) e. GrpOp ) )
6 5 simpld 
 |-  ( K e. DivRingOps -> K e. RingOps )
7 6 anim1i 
 |-  ( ( K e. DivRingOps /\ K e. Com2 ) -> ( K e. RingOps /\ K e. Com2 ) )
8 df-fld 
 |-  Fld = ( DivRingOps i^i Com2 )
9 8 elin2 
 |-  ( K e. Fld <-> ( K e. DivRingOps /\ K e. Com2 ) )
10 iscrngo 
 |-  ( K e. CRingOps <-> ( K e. RingOps /\ K e. Com2 ) )
11 7 9 10 3imtr4i 
 |-  ( K e. Fld -> K e. CRingOps )