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	bitrid	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → ( 𝐼 ∉ Ring ↔ ¬ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )
14	8 13	mpbird	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵 ) ) → 𝐼 ∉ Ring )