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 
|- .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. )