Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
lidl1
Next ⟩
lidlacs
Metamath Proof Explorer
Ascii
Unicode
Theorem
lidl1
Description:
Every ring contains a unit ideal.
(Contributed by
Stefan O'Rear
, 3-Jan-2015)
Ref
Expression
Hypotheses
lidl0.u
⊢
U
=
LIdeal
⁡
R
lidl1.b
⊢
B
=
Base
R
Assertion
lidl1
⊢
R
∈
Ring
→
B
∈
U
Proof
Step
Hyp
Ref
Expression
1
lidl0.u
⊢
U
=
LIdeal
⁡
R
2
lidl1.b
⊢
B
=
Base
R
3
rlmlmod
⊢
R
∈
Ring
→
ringLMod
⁡
R
∈
LMod
4
rlmbas
⊢
Base
R
=
Base
ringLMod
⁡
R
5
2
4
eqtri
⊢
B
=
Base
ringLMod
⁡
R
6
eqid
⊢
LSubSp
⁡
ringLMod
⁡
R
=
LSubSp
⁡
ringLMod
⁡
R
7
5
6
lss1
⊢
ringLMod
⁡
R
∈
LMod
→
B
∈
LSubSp
⁡
ringLMod
⁡
R
8
3
7
syl
⊢
R
∈
Ring
→
B
∈
LSubSp
⁡
ringLMod
⁡
R
9
lidlval
⊢
LIdeal
⁡
R
=
LSubSp
⁡
ringLMod
⁡
R
10
1
9
eqtri
⊢
U
=
LSubSp
⁡
ringLMod
⁡
R
11
8
10
eleqtrrdi
⊢
R
∈
Ring
→
B
∈
U