Theorem domnnzr 20706

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  ._rcmulr 17298  0_gc0g 17484  NzRingcnzr 20512  Domncdomn 20692

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  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-domn 20695

This theorem is referenced by:  domnring  20707  isdomn4  20716  fidomndrng  20774  abvn0b  20837  domnchr  21547  znidomb  21580  nrgdomn  24692  ply1domn  26163  fta1glem1  26207  fta1glem2  26208  fta1b  26211  idomrootle  26212  lgsqrlem4  27393  domnprodn0  33279  subrdom  33288  fracfld  33310  qsidomlem1  33480  1arithufdlem1  33572  ply1dg1rt  33604  assafld  33688  idomnnzpownz  42133  idomnnzgmulnz  42134  deg1gprod  42141  deg1pow  42142  domnexpgn0cl  42533  fiabv  42546  deg1mhm  43212