Theorem isnzr 20757

Description: Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)

Hypotheses

Ref	Expression
isnzr.o	⊢ 1 = (1r‘𝑅)
isnzr.z	⊢ 0 = (0g‘𝑅)

Assertion

Ref	Expression
isnzr	⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))

Proof of Theorem isnzr

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6883	. . . 4 ⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅))
2		isnzr.o	. . . 4 ⊢ 1 = (1r‘𝑅)
3	1, 2	eqtr4di 2814	. . 3 ⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 )
4		fveq2 6883	. . . 4 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
5		isnzr.z	. . . 4 ⊢ 0 = (0g‘𝑅)
6	4, 5	eqtr4di 2814	. . 3 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 )
7	3, 6	neeq12d 3017	. 2 ⊢ (𝑟 = 𝑅 → ((1r‘𝑟) ≠ (0g‘𝑟) ↔ 1 ≠ 0 ))
8		df-nzr 20756	. 2 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
9	7, 8	elrab2 3649	1 ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ‘cfv 6537  0_gc0g 17603  1_rcur 20400  Ringcrg 20452  NzRingcnzr 20755

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-nzr 20756

This theorem is used by:  nzrnz  20758  nzrringOLD  20760  isnzr2  20761  isnzr2hash  20763  nzrpropd  20764  opprnzrb  20765  ringelnzr  20767  subrgnzr  20839  isdomn3  20959  drngnzr  20995  isfieldidl  21533  qsnzr  21632  zringnzr  21759  chrnzr  21829  nrginvrcn  25004  ply1nzb  26434  ricnzr1  33842  drngidlhash  33976  mxidlnzr  33985  psrnzr  34137  zrhnm  34592