Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ideals
idl0cl
Next ⟩
idladdcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
idl0cl
Description:
An ideal contains
0
.
(Contributed by
Jeff Madsen
, 10-Jun-2010)
Ref
Expression
Hypotheses
idl0cl.1
⊢
G
=
1
st
⁡
R
idl0cl.2
⊢
Z
=
GId
⁡
G
Assertion
idl0cl
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
→
Z
∈
I
Proof
Step
Hyp
Ref
Expression
1
idl0cl.1
⊢
G
=
1
st
⁡
R
2
idl0cl.2
⊢
Z
=
GId
⁡
G
3
eqid
⊢
2
nd
⁡
R
=
2
nd
⁡
R
4
eqid
⊢
ran
⁡
G
=
ran
⁡
G
5
1
3
4
2
isidl
⊢
R
∈
RingOps
→
I
∈
Idl
⁡
R
↔
I
⊆
ran
⁡
G
∧
Z
∈
I
∧
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
∧
∀
z
∈
ran
⁡
G
z
2
nd
⁡
R
x
∈
I
∧
x
2
nd
⁡
R
z
∈
I
6
5
biimpa
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
→
I
⊆
ran
⁡
G
∧
Z
∈
I
∧
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
∧
∀
z
∈
ran
⁡
G
z
2
nd
⁡
R
x
∈
I
∧
x
2
nd
⁡
R
z
∈
I
7
6
simp2d
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
→
Z
∈
I