Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > isfld | Structured version Visualization version Unicode version |
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
Ref | Expression |
---|---|
isfld | Field |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-field 18750 | . 2 Field | |
2 | 1 | elin2 3801 | 1 Field |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wcel 1990 ccrg 18548 cdr 18747 Fieldcfield 18748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-field 18750 |
This theorem is referenced by: fldpropd 18775 rng1nfld 19278 fldidom 19305 fiidomfld 19308 refld 19965 recrng 19967 frlmphllem 20119 frlmphl 20120 rrxcph 23180 ply1pid 23939 lgseisenlem3 25102 lgseisenlem4 25103 ofldlt1 29813 ofldchr 29814 subofld 29816 isarchiofld 29817 reofld 29840 rearchi 29842 qqhrhm 30033 matunitlindflem1 33405 matunitlindflem2 33406 matunitlindf 33407 fldcat 42082 fldcatALTV 42100 |
Copyright terms: Public domain | W3C validator |