Step |
Hyp |
Ref |
Expression |
1 |
|
lidlabl.l |
⊢ 𝐿 = ( LIdeal ‘ 𝑅 ) |
2 |
|
lidlabl.i |
⊢ 𝐼 = ( 𝑅 ↾s 𝑈 ) |
3 |
|
zlidlring.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
4 |
|
zlidlring.0 |
⊢ 0 = ( 0g ‘ 𝑅 ) |
5 |
|
neanior |
⊢ ( ( 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ↔ ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) |
6 |
5
|
biimpi |
⊢ ( ( 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) → ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) |
7 |
6
|
3adant1 |
⊢ ( ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) → ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) |
9 |
|
df-nel |
⊢ ( 𝐼 ∉ Ring ↔ ¬ 𝐼 ∈ Ring ) |
10 |
1 2 3 4
|
uzlidlring |
⊢ ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) → ( 𝐼 ∈ Ring ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) ) |
11 |
10
|
3ad2antr1 |
⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → ( 𝐼 ∈ Ring ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) ) |
12 |
11
|
notbid |
⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → ( ¬ 𝐼 ∈ Ring ↔ ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) ) |
13 |
9 12
|
syl5bb |
⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → ( 𝐼 ∉ Ring ↔ ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) ) |
14 |
8 13
|
mpbird |
⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → 𝐼 ∉ Ring ) |