Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > isfld | Structured version Visualization version GIF version |
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
Ref | Expression |
---|---|
isfld | ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-field 19434 | . 2 ⊢ Field = (DivRing ∩ CRing) | |
2 | 1 | elin2 4171 | 1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∈ wcel 2105 CRingccrg 19227 DivRingcdr 19431 Fieldcfield 19432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-field 19434 |
This theorem is referenced by: fldpropd 19459 primefld 19513 rng1nfld 19979 fldidom 20006 fiidomfld 20009 refld 20691 recrng 20693 frlmphllem 20852 frlmphl 20853 rrxcph 23922 rrx0 23927 ply1pid 24700 lgseisenlem3 25880 lgseisenlem4 25881 ofldlt1 30813 ofldchr 30814 subofld 30816 isarchiofld 30817 reofld 30840 rearchi 30842 srafldlvec 30890 rgmoddim 30907 ccfldextrr 30937 fldextsralvec 30944 extdgcl 30945 extdggt0 30946 fldextid 30948 extdgmul 30950 extdg1id 30952 ccfldsrarelvec 30955 qqhrhm 31129 matunitlindflem1 34769 matunitlindflem2 34770 matunitlindf 34771 fldcat 44281 fldcatALTV 44299 |
Copyright terms: Public domain | W3C validator |