Database
BASIC ALGEBRAIC STRUCTURES
Ideals
Principal ideal rings. Divisibility in the integers
lpi1
Next ⟩
islpir
Metamath Proof Explorer
Ascii
Unicode
Theorem
lpi1
Description:
The unit ideal is always principal.
(Contributed by
Stefan O'Rear
, 3-Jan-2015)
Ref
Expression
Hypotheses
lpival.p
⊢
P
=
LPIdeal
⁡
R
lpi1.b
⊢
B
=
Base
R
Assertion
lpi1
⊢
R
∈
Ring
→
B
∈
P
Proof
Step
Hyp
Ref
Expression
1
lpival.p
⊢
P
=
LPIdeal
⁡
R
2
lpi1.b
⊢
B
=
Base
R
3
eqid
⊢
1
R
=
1
R
4
2
3
ringidcl
⊢
R
∈
Ring
→
1
R
∈
B
5
eqid
⊢
RSpan
⁡
R
=
RSpan
⁡
R
6
5
2
3
rsp1
⊢
R
∈
Ring
→
RSpan
⁡
R
⁡
1
R
=
B
7
6
eqcomd
⊢
R
∈
Ring
→
B
=
RSpan
⁡
R
⁡
1
R
8
sneq
⊢
g
=
1
R
→
g
=
1
R
9
8
fveq2d
⊢
g
=
1
R
→
RSpan
⁡
R
⁡
g
=
RSpan
⁡
R
⁡
1
R
10
9
rspceeqv
⊢
1
R
∈
B
∧
B
=
RSpan
⁡
R
⁡
1
R
→
∃
g
∈
B
B
=
RSpan
⁡
R
⁡
g
11
4
7
10
syl2anc
⊢
R
∈
Ring
→
∃
g
∈
B
B
=
RSpan
⁡
R
⁡
g
12
1
5
2
islpidl
⊢
R
∈
Ring
→
B
∈
P
↔
∃
g
∈
B
B
=
RSpan
⁡
R
⁡
g
13
11
12
mpbird
⊢
R
∈
Ring
→
B
∈
P