Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
lidlnz
Next ⟩
drngnidl
Metamath Proof Explorer
Ascii
Unicode
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
˙