Metamath Proof Explorer


Theorem flddivrng

Description: A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion flddivrng
|- ( K e. Fld -> K e. DivRingOps )

Proof

Step Hyp Ref Expression
1 df-fld
 |-  Fld = ( DivRingOps i^i Com2 )
2 inss1
 |-  ( DivRingOps i^i Com2 ) C_ DivRingOps
3 1 2 eqsstri
 |-  Fld C_ DivRingOps
4 3 sseli
 |-  ( K e. Fld -> K e. DivRingOps )