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	|- .0. = ( 0g ` R )
Assertion	lidlnz	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> E. x e. I x =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		lidlnz.u	|- U = ( LIdeal ` R )
2		lidlnz.z	|- .0. = ( 0g ` R )
3	1 2	lidl0cl	|- ( ( R e. Ring /\ I e. U ) -> .0. e. I )
4	3	snssd	|- ( ( R e. Ring /\ I e. U ) -> { .0. } C_ I )
5	4	3adant3	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> { .0. } C_ I )
6		simp3	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> I =/= { .0. } )
7	6	necomd	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> { .0. } =/= I )
8		df-pss	|- ( { .0. } C. I <-> ( { .0. } C_ I /\ { .0. } =/= I ) )
9	5 7 8	sylanbrc	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> { .0. } C. I )
10		pssnel	|- ( { .0. } C. I -> E. x ( x e. I /\ -. x e. { .0. } ) )
11	9 10	syl	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> E. x ( x e. I /\ -. x e. { .0. } ) )
12		velsn	|- ( x e. { .0. } <-> x = .0. )
13	12	necon3bbii	|- ( -. x e. { .0. } <-> x =/= .0. )
14	13	anbi2i	|- ( ( x e. I /\ -. x e. { .0. } ) <-> ( x e. I /\ x =/= .0. ) )
15	14	exbii	|- ( E. x ( x e. I /\ -. x e. { .0. } ) <-> E. x ( x e. I /\ x =/= .0. ) )
16		df-rex	|- ( E. x e. I x =/= .0. <-> E. x ( x e. I /\ x =/= .0. ) )
17	15 16	bitr4i	|- ( E. x ( x e. I /\ -. x e. { .0. } ) <-> E. x e. I x =/= .0. )
18	11 17	sylib	|- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> E. x e. I x =/= .0. )