Metamath Proof Explorer


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 )