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 Fld K DivRingOps

Proof

Step Hyp Ref Expression
1 df-fld Fld = DivRingOps Com2
2 inss1 DivRingOps Com2 DivRingOps
3 1 2 eqsstri Fld DivRingOps
4 3 sseli K Fld K DivRingOps