![]() |
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 20043 | . 2 ⊢ Field = (DivRing ∩ CRing) | |
2 | 1 | elin2 4137 | 1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∈ wcel 2104 CRingccrg 19833 DivRingcdr 20040 Fieldcfield 20041 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3439 df-in 3899 df-field 20043 |
This theorem is referenced by: fldpropd 20068 primefld 20122 rng1nfld 20598 fldidom 20625 fldidomOLD 20626 fiidomfld 20629 refld 20873 recrng 20875 frlmphllem 21036 frlmphl 21037 recvs 24358 rrxcph 24605 rrx0 24610 ply1pid 25393 lgseisenlem3 26574 lgseisenlem4 26575 ofldlt1 31561 ofldchr 31562 subofld 31564 isarchiofld 31565 reofld 31593 rearchi 31595 srafldlvec 31725 rgmoddim 31742 ccfldextrr 31772 fldextsralvec 31779 extdgcl 31780 extdggt0 31781 fldextid 31783 extdgmul 31785 extdg1id 31787 ccfldsrarelvec 31790 qqhrhm 31988 matunitlindflem1 35821 matunitlindflem2 35822 matunitlindf 35823 fldcrngd 40450 prjcrv0 40665 fldcat 45884 fldcatALTV 45902 |
Copyright terms: Public domain | W3C validator |