Theorem domnnzr 20874

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  ._rcmulr 17349  0_gc0g 17530  NzRingcnzr 20678  Domncdomn 20860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-domn 20863

This theorem is used by:  domnring  20875  isdomn4  20883  fidomndrng  20946  abvn0b  21008  qsidomlem1  21549  domnchr  21751  znidomb  21780  nrgdomn  24903  ply1domn  26356  fta1glem1  26400  fta1glem2  26401  fta1b  26404  idomrootle  26405  lgsqrlem4  27593  domnprodn0  33726  domnprodeq0  33727  subrdom  33733  ricdomn1  33737  fracfld  33757  1arithufdlem1  33962  ply1dg1rt  33998  deg1prod  34001  mplidomlem  34045  vietadeg1  34096  assafld  34155  idomnnzpownz  43006  idomnnzgmulnz  43007  deg1gprod  43014  deg1pow  43015  domnexpgn0cl  43413  fiabv  43426  deg1mhm  44049