Theorem ringelnzr

Description: A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 13-Jun-2015)

	Ref	Expression
Hypotheses	ringelnzr.z	⊢ 0 = ( 0g ‘ 𝑅 )
	ringelnzr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	ringelnzr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		ringelnzr.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		ringelnzr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
4		eldifsni	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ≠ 0 )
5	4	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑋 ≠ 0 )
6		eldifi	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ∈ 𝐵 )
7	6	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑋 ∈ 𝐵 )
8	2 1	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
9	8	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 0 ∈ 𝐵 )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	2 10 1	ring1eq0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) = 0 → 𝑋 = 0 ) )
12	3 7 9 11	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 1r ‘ 𝑅 ) = 0 → 𝑋 = 0 ) )
13	12	necon3d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 ≠ 0 → ( 1r ‘ 𝑅 ) ≠ 0 ) )
14	5 13	mpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1r ‘ 𝑅 ) ≠ 0 )
15	10 1	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) )
16	3 14 15	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ NzRing )