![]() |
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 19113 | . 2 ⊢ Field = (DivRing ∩ CRing) | |
2 | 1 | elin2 4030 | 1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∈ wcel 2164 CRingccrg 18909 DivRingcdr 19110 Fieldcfield 19111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-in 3805 df-field 19113 |
This theorem is referenced by: fldpropd 19138 rng1nfld 19646 fldidom 19673 fiidomfld 19676 refld 20333 recrng 20335 frlmphllem 20493 frlmphl 20494 rrxcph 23567 rrx0 23572 ply1pid 24345 lgseisenlem3 25522 lgseisenlem4 25523 ofldlt1 30354 ofldchr 30355 subofld 30357 isarchiofld 30358 reofld 30381 rearchi 30383 qqhrhm 30574 matunitlindflem1 33944 matunitlindflem2 33945 matunitlindf 33946 fldcat 42943 fldcatALTV 42961 |
Copyright terms: Public domain | W3C validator |