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 ) |