| 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 20732 | . 2 ⊢ Field = (DivRing ∩ CRing) | |
| 2 | 1 | elin2 4203 | 1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2108 CRingccrg 20231 DivRingcdr 20729 Fieldcfield 20730 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-field 20732 |
| This theorem is referenced by: flddrngd 20741 fldcrngd 20742 fldpropd 20770 fldidom 20771 fldidomOLD 20772 fiidomfld 20775 rng1nfld 20780 fldcat 20784 fldsdrgfld 20799 primefld 20806 refld 21637 frlmphllem 21800 frlmphl 21801 recvs 25179 rrxcph 25426 rrx0 25431 ply1pid 26222 lgseisenlem3 27421 lgseisenlem4 27422 qfld 33300 fracfld 33310 fldgenfld 33322 ofldlt1 33343 ofldchr 33344 subofld 33346 isarchiofld 33347 cnfldfld 33371 reofld 33372 rearchi 33374 qsfld 33526 srafldlvec 33637 rgmoddimOLD 33661 assafld 33688 ccfldextrr 33699 fldextsralvec 33706 extdgcl 33707 extdggt0 33708 fldextid 33710 extdgid 33711 extdgmul 33714 extdg1id 33716 ccfldsrarelvec 33721 2sqr3minply 33791 qqhrhm 33990 matunitlindflem1 37623 matunitlindflem2 37624 matunitlindf 37625 fldhmf1 42091 aks6d1c1p2 42110 aks6d1c2lem4 42128 aks6d1c5lem3 42138 aks6d1c5lem2 42139 aks6d1c6lem1 42171 ricfld 42540 fldcatALTV 48247 |
| Copyright terms: Public domain | W3C validator |