Theorem domnnzr 20685

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

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  ._rcmulr 17219  0_gc0g 17400  NzRingcnzr 20491  Domncdomn 20671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-domn 20674

This theorem is referenced by:  domnring  20686  isdomn4  20695  fidomndrng  20752  abvn0b  20815  domnchr  21514  znidomb  21543  nrgdomn  24661  ply1domn  26114  fta1glem1  26158  fta1glem2  26159  fta1b  26162  idomrootle  26163  lgsqrlem4  27337  domnprodn0  33363  domnprodeq0  33364  subrdom  33373  ricdomn1  33377  fracfld  33399  qsidomlem1  33542  1arithufdlem1  33634  ply1dg1rt  33670  deg1prod  33673  mplidomlem  33718  vietadeg1  33769  assafld  33828  idomnnzpownz  42624  idomnnzgmulnz  42625  deg1gprod  42632  deg1pow  42633  domnexpgn0cl  43016  fiabv  43029  deg1mhm  43652