This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lidlnz

Description: A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015)

		Ref	Expression
	Hypotheses	lidlnz.u	$⊢ U = LIdeal (R)$
		lidlnz.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	lidlnz	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists x \in I x \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lidlnz.u	$⊢ U = LIdeal (R)$
2		lidlnz.z	$⊢ \underset{˙}{0} = 0_{R}$
3	1 2	lidl0cl	$⊢ (R \in Ring \land I \in U) \to \underset{˙}{0} \in I$
4	3	snssd	$⊢ (R \in Ring \land I \in U) \to \{\underset{˙}{0}\} \subseteq I$
5	4	3adant3	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \subseteq I$
6		simp3	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \neq \{\underset{˙}{0}\}$
7	6	necomd	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \neq I$
8		df-pss	$⊢ \{\underset{˙}{0}\} \subset I \leftrightarrow (\{\underset{˙}{0}\} \subseteq I \land \{\underset{˙}{0}\} \neq I)$
9	5 7 8	sylanbrc	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \subset I$
10		pssnel	$⊢ \{\underset{˙}{0}\} \subset I \to \exists x (x \in I \land \neg x \in \{\underset{˙}{0}\})$
11	9 10	syl	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists x (x \in I \land \neg x \in \{\underset{˙}{0}\})$
12		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
13	12	necon3bbii	$⊢ \neg x \in \{\underset{˙}{0}\} \leftrightarrow x \neq \underset{˙}{0}$
14	13	anbi2i	$⊢ (x \in I \land \neg x \in \{\underset{˙}{0}\}) \leftrightarrow (x \in I \land x \neq \underset{˙}{0})$
15	14	exbii	$⊢ \exists x (x \in I \land \neg x \in \{\underset{˙}{0}\}) \leftrightarrow \exists x (x \in I \land x \neq \underset{˙}{0})$
16		df-rex	$⊢ \exists x \in I x \neq \underset{˙}{0} \leftrightarrow \exists x (x \in I \land x \neq \underset{˙}{0})$
17	15 16	bitr4i	$⊢ \exists x (x \in I \land \neg x \in \{\underset{˙}{0}\}) \leftrightarrow \exists x \in I x \neq \underset{˙}{0}$
18	11 17	sylib	$⊢ (R \in Ring \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists x \in I x \neq \underset{˙}{0}$