Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ideals
idladdcl
Next ⟩
idllmulcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
idladdcl
Description:
An ideal is closed under addition.
(Contributed by
Jeff Madsen
, 10-Jun-2010)
Ref
Expression
Hypothesis
idladdcl.1
⊢
G
=
1
st
⁡
R
Assertion
idladdcl
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
∧
A
∈
I
∧
B
∈
I
→
A
G
B
∈
I
Proof
Step
Hyp
Ref
Expression
1
idladdcl.1
⊢
G
=
1
st
⁡
R
2
eqid
⊢
2
nd
⁡
R
=
2
nd
⁡
R
3
eqid
⊢
ran
⁡
G
=
ran
⁡
G
4
eqid
⊢
GId
⁡
G
=
GId
⁡
G
5
1
2
3
4
isidl
⊢
R
∈
RingOps
→
I
∈
Idl
⁡
R
↔
I
⊆
ran
⁡
G
∧
GId
⁡
G
∈
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
∧
GId
⁡
G
∈
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
simp3d
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
→
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
∧
∀
z
∈
ran
⁡
G
z
2
nd
⁡
R
x
∈
I
∧
x
2
nd
⁡
R
z
∈
I
8
simpl
⊢
∀
y
∈
I
x
G
y
∈
I
∧
∀
z
∈
ran
⁡
G
z
2
nd
⁡
R
x
∈
I
∧
x
2
nd
⁡
R
z
∈
I
→
∀
y
∈
I
x
G
y
∈
I
9
8
ralimi
⊢
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
∧
∀
z
∈
ran
⁡
G
z
2
nd
⁡
R
x
∈
I
∧
x
2
nd
⁡
R
z
∈
I
→
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
10
7
9
syl
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
→
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
11
oveq1
⊢
x
=
A
→
x
G
y
=
A
G
y
12
11
eleq1d
⊢
x
=
A
→
x
G
y
∈
I
↔
A
G
y
∈
I
13
oveq2
⊢
y
=
B
→
A
G
y
=
A
G
B
14
13
eleq1d
⊢
y
=
B
→
A
G
y
∈
I
↔
A
G
B
∈
I
15
12
14
rspc2v
⊢
A
∈
I
∧
B
∈
I
→
∀
x
∈
I
∀
y
∈
I
x
G
y
∈
I
→
A
G
B
∈
I
16
10
15
mpan9
⊢
R
∈
RingOps
∧
I
∈
Idl
⁡
R
∧
A
∈
I
∧
B
∈
I
→
A
G
B
∈
I