Step |
Hyp |
Ref |
Expression |
1 |
|
mxidlval.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
1
|
mxidlidl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) |
3 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
4 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
5 |
3 4
|
lidl0cl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑀 ) |
6 |
2 5
|
syldan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑀 ) |
7 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
8 |
1 7
|
mxidln1 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑀 ) |
9 |
|
nelne2 |
⊢ ( ( ( 0g ‘ 𝑅 ) ∈ 𝑀 ∧ ¬ ( 1r ‘ 𝑅 ) ∈ 𝑀 ) → ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) ) |
10 |
6 8 9
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) ) |
11 |
10
|
necomd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) |
12 |
7 4
|
isnzr |
⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ) |
13 |
12
|
biimpri |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ NzRing ) |
14 |
11 13
|
syldan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing ) |