Metamath Proof Explorer


Theorem lidldomnnring

Description: A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020)

Ref Expression
Hypotheses lidlabl.l 𝐿 = ( LIdeal ‘ 𝑅 )
lidlabl.i 𝐼 = ( 𝑅s 𝑈 )
zlidlring.b 𝐵 = ( Base ‘ 𝑅 )
zlidlring.0 0 = ( 0g𝑅 )
Assertion lidldomnnring ( ( 𝑅 ∈ Domn ∧ ( 𝑈𝐿𝑈 ≠ { 0 } ∧ 𝑈𝐵 ) ) → 𝐼 ∉ Ring )

Proof

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 )