This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )