Theorem domnnzr 20681

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 2741	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2741	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
3		eqid 2741	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4	1, 2, 3	isdomn 20680	. 2 ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)))))
5	4	simplbi 498	1 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)

Syntax hints:   → wi 4   ∨ wo 854   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ‘cfv 6488  (class class class)co 7359  Basecbs 17174  ._rcmulr 17216  0_gc0g 17397  NzRingcnzr 20487  Domncdomn 20667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5230

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rab 3394  df-v 3435  df-sbc 3725  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362  df-domn 20670

This theorem is referenced by:  domnring  20682  isdomn4  20691  fidomndrng  20748  abvn0b  20811  domnchr  21510  znidomb  21539  nrgdomn  24657  ply1domn  26110  fta1glem1  26154  fta1glem2  26155  fta1b  26158  idomrootle  26159  lgsqrlem4  27333  domnprodn0  33358  domnprodeq0  33359  subrdom  33368  ricdomn1  33372  fracfld  33394  qsidomlem1  33537  1arithufdlem1  33637  ply1dg1rt  33673  deg1prod  33676  mplidomlem  33721  vietadeg1  33772  assafld  33831  idomnnzpownz  42630  idomnnzgmulnz  42631  deg1gprod  42638  deg1pow  42639  domnexpgn0cl  43022  fiabv  43035  deg1mhm  43658