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 ˙ = 0 R
Assertion lidlnz R Ring I U I 0 ˙ x I x 0 ˙

Proof

Step Hyp Ref Expression
1 lidlnz.u U = LIdeal R
2 lidlnz.z 0 ˙ = 0 R
3 1 2 lidl0cl R Ring I U 0 ˙ I
4 3 snssd R Ring I U 0 ˙ I
5 4 3adant3 R Ring I U I 0 ˙ 0 ˙ I
6 simp3 R Ring I U I 0 ˙ I 0 ˙
7 6 necomd R Ring I U I 0 ˙ 0 ˙ I
8 df-pss 0 ˙ I 0 ˙ I 0 ˙ I
9 5 7 8 sylanbrc R Ring I U I 0 ˙ 0 ˙ I
10 pssnel 0 ˙ I x x I ¬ x 0 ˙
11 9 10 syl R Ring I U I 0 ˙ x x I ¬ x 0 ˙
12 velsn x 0 ˙ x = 0 ˙
13 12 necon3bbii ¬ x 0 ˙ x 0 ˙
14 13 anbi2i x I ¬ x 0 ˙ x I x 0 ˙
15 14 exbii x x I ¬ x 0 ˙ x x I x 0 ˙
16 df-rex x I x 0 ˙ x x I x 0 ˙
17 15 16 bitr4i x x I ¬ x 0 ˙ x I x 0 ˙
18 11 17 sylib R Ring I U I 0 ˙ x I x 0 ˙