Database
BASIC ALGEBRAIC STRUCTURES
Ideals
Principal ideal rings. Divisibility in the integers
lpiss
Next ⟩
islpir2
Metamath Proof Explorer
Ascii
Unicode
Theorem
lpiss
Description:
Principal ideals are a subclass of ideal.
(Contributed by
Stefan O'Rear
, 3-Jan-2015)
Ref
Expression
Hypotheses
lpival.p
⊢
P
=
LPIdeal
⁡
R
lpiss.u
⊢
U
=
LIdeal
⁡
R
Assertion
lpiss
⊢
R
∈
Ring
→
P
⊆
U
Proof
Step
Hyp
Ref
Expression
1
lpival.p
⊢
P
=
LPIdeal
⁡
R
2
lpiss.u
⊢
U
=
LIdeal
⁡
R
3
eqid
⊢
RSpan
⁡
R
=
RSpan
⁡
R
4
eqid
⊢
Base
R
=
Base
R
5
1
3
4
islpidl
⊢
R
∈
Ring
→
a
∈
P
↔
∃
g
∈
Base
R
a
=
RSpan
⁡
R
⁡
g
6
snssi
⊢
g
∈
Base
R
→
g
⊆
Base
R
7
3
4
2
rspcl
⊢
R
∈
Ring
∧
g
⊆
Base
R
→
RSpan
⁡
R
⁡
g
∈
U
8
6
7
sylan2
⊢
R
∈
Ring
∧
g
∈
Base
R
→
RSpan
⁡
R
⁡
g
∈
U
9
eleq1
⊢
a
=
RSpan
⁡
R
⁡
g
→
a
∈
U
↔
RSpan
⁡
R
⁡
g
∈
U
10
8
9
syl5ibrcom
⊢
R
∈
Ring
∧
g
∈
Base
R
→
a
=
RSpan
⁡
R
⁡
g
→
a
∈
U
11
10
rexlimdva
⊢
R
∈
Ring
→
∃
g
∈
Base
R
a
=
RSpan
⁡
R
⁡
g
→
a
∈
U
12
5
11
sylbid
⊢
R
∈
Ring
→
a
∈
P
→
a
∈
U
13
12
ssrdv
⊢
R
∈
Ring
→
P
⊆
U