Theorem isnzr

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

	Ref	Expression
Hypotheses	isnzr.o	⊢ 1 = ( 1r ‘ 𝑅 )
	isnzr.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) )

Proof

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