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 ) |
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 ) |