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