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	|- L = ( LIdeal ` R )
	lidlabl.i	|- I = ( R |`s U )
	zlidlring.b	|- B = ( Base ` R )
	zlidlring.0	|- .0. = ( 0g ` R )
Assertion	lidldomnnring	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> I e/ Ring )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	|- L = ( LIdeal ` R )
2		lidlabl.i	|- I = ( R |`s U )
3		zlidlring.b	|- B = ( Base ` R )
4		zlidlring.0	|- .0. = ( 0g ` R )
5		neanior	|- ( ( U =/= { .0. } /\ U =/= B ) <-> -. ( U = { .0. } \/ U = B ) )
6	5	biimpi	|- ( ( U =/= { .0. } /\ U =/= B ) -> -. ( U = { .0. } \/ U = B ) )
7	6	3adant1	|- ( ( U e. L /\ U =/= { .0. } /\ U =/= B ) -> -. ( U = { .0. } \/ U = B ) )
8	7	adantl	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> -. ( U = { .0. } \/ U = B ) )
9		df-nel	|- ( I e/ Ring <-> -. I e. Ring )
10	1 2 3 4	uzlidlring	|- ( ( R e. Domn /\ U e. L ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )
11	10	3ad2antr1	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )
12	11	notbid	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> ( -. I e. Ring <-> -. ( U = { .0. } \/ U = B ) ) )
13	9 12	syl5bb	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> ( I e/ Ring <-> -. ( U = { .0. } \/ U = B ) ) )
14	8 13	mpbird	|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> I e/ Ring )