| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > domnnzr | Structured version Visualization version GIF version | ||
| Description: A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
| Ref | Expression |
|---|---|
| domnnzr | ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2765 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 2 | eqid 2765 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
| 3 | eqid 2765 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
| 4 | 1, 2, 3 | isdomn 20781 | . 2 ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))))) |
| 5 | 4 | simplbi 501 | 1 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 860 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ‘cfv 6525 (class class class)co 7400 Basecbs 17259 .rcmulr 17301 0gc0g 17482 NzRingcnzr 20586 Domncdomn 20768 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-nul 5261 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-iota 6481 df-fv 6533 df-ov 7403 df-domn 20771 |
| This theorem is referenced by: domnring 20783 isdomn4 20791 fidomndrng 20846 abvn0b 20908 qsidomlem1 21440 domnchr 21642 znidomb 21671 nrgdomn 24789 ply1domn 26242 fta1glem1 26286 fta1glem2 26287 fta1b 26290 idomrootle 26291 lgsqrlem4 27471 domnprodn0 33511 domnprodeq0 33512 subrdom 33518 ricdomn1 33522 fracfld 33544 1arithufdlem1 33751 ply1dg1rt 33787 deg1prod 33790 mplidomlem 33834 vietadeg1 33885 assafld 33944 idomnnzpownz 42761 idomnnzgmulnz 42762 deg1gprod 42769 deg1pow 42770 domnexpgn0cl 43153 fiabv 43166 deg1mhm 43789 |
| Copyright terms: Public domain | W3C validator |