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 ↾_{𝑠} U$
	zlidlring.b	$⊢ B = {Base}_{R}$
	zlidlring.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lidldomnnring	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to I \notin Ring$

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		zlidlring.b	$⊢ B = {Base}_{R}$
4		zlidlring.0	$⊢ \underset{˙}{0} = 0_{R}$
5		neanior	$⊢ (U \neq \{\underset{˙}{0}\} \land U \neq B) \leftrightarrow \neg (U = \{\underset{˙}{0}\} \lor U = B)$
6	5	biimpi	$⊢ (U \neq \{\underset{˙}{0}\} \land U \neq B) \to \neg (U = \{\underset{˙}{0}\} \lor U = B)$
7	6	3adant1	$⊢ (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B) \to \neg (U = \{\underset{˙}{0}\} \lor U = B)$
8	7	adantl	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to \neg (U = \{\underset{˙}{0}\} \lor U = B)$
9		df-nel	$⊢ I \notin Ring \leftrightarrow \neg I \in Ring$
10	1 2 3 4	uzlidlring	$⊢ (R \in Domn \land U \in L) \to (I \in Ring \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$
11	10	3ad2antr1	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to (I \in Ring \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$
12	11	notbid	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to (\neg I \in Ring \leftrightarrow \neg (U = \{\underset{˙}{0}\} \lor U = B))$
13	9 12	syl5bb	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to (I \notin Ring \leftrightarrow \neg (U = \{\underset{˙}{0}\} \lor U = B))$
14	8 13	mpbird	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\} \land U \neq B)) \to I \notin Ring$

Metamath Proof Explorer