Theorem lidlnz

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

	Ref	Expression
Hypotheses	lidlnz.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
	lidlnz.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	lidlnz	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\wedge I\ne \left\{\underset{\dot{}}{0}\right\}\right)\to \exists x\in Ix\ne \underset{\dot{}}{0}$$

Proof

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