Theorem domnnzr 20622

Description: A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)

Assertion

Ref	Expression
domnnzr	⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)

Proof of Theorem domnnzr

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2731	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
3		eqid 2731	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4	1, 2, 3	isdomn 20621	. 2 ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)))))
5	4	simplbi 497	1 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  ._rcmulr 17162  0_gc0g 17343  NzRingcnzr 20428  Domncdomn 20608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-domn 20611

This theorem is referenced by:  domnring  20623  isdomn4  20632  fidomndrng  20689  abvn0b  20752  domnchr  21470  znidomb  21499  nrgdomn  24587  ply1domn  26057  fta1glem1  26101  fta1glem2  26102  fta1b  26105  idomrootle  26106  lgsqrlem4  27288  domnprodn0  33240  subrdom  33249  fracfld  33272  qsidomlem1  33415  1arithufdlem1  33507  ply1dg1rt  33541  assafld  33648  idomnnzpownz  42171  idomnnzgmulnz  42172  deg1gprod  42179  deg1pow  42180  domnexpgn0cl  42562  fiabv  42575  deg1mhm  43239