Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ideals
maxidlidl
Next ⟩
maxidlnr
Metamath Proof Explorer
Ascii
Unicode
Theorem
maxidlidl
Description:
A maximal ideal is an ideal.
(Contributed by
Jeff Madsen
, 5-Jan-2011)
Ref
Expression
Assertion
maxidlidl
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
M
∈
Idl
⁡
R
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
1
st
⁡
R
=
1
st
⁡
R
2
eqid
⊢
ran
⁡
1
st
⁡
R
=
ran
⁡
1
st
⁡
R
3
1
2
ismaxidl
⊢
R
∈
RingOps
→
M
∈
MaxIdl
⁡
R
↔
M
∈
Idl
⁡
R
∧
M
≠
ran
⁡
1
st
⁡
R
∧
∀
j
∈
Idl
⁡
R
M
⊆
j
→
j
=
M
∨
j
=
ran
⁡
1
st
⁡
R
4
3anass
⊢
M
∈
Idl
⁡
R
∧
M
≠
ran
⁡
1
st
⁡
R
∧
∀
j
∈
Idl
⁡
R
M
⊆
j
→
j
=
M
∨
j
=
ran
⁡
1
st
⁡
R
↔
M
∈
Idl
⁡
R
∧
M
≠
ran
⁡
1
st
⁡
R
∧
∀
j
∈
Idl
⁡
R
M
⊆
j
→
j
=
M
∨
j
=
ran
⁡
1
st
⁡
R
5
3
4
syl6bb
⊢
R
∈
RingOps
→
M
∈
MaxIdl
⁡
R
↔
M
∈
Idl
⁡
R
∧
M
≠
ran
⁡
1
st
⁡
R
∧
∀
j
∈
Idl
⁡
R
M
⊆
j
→
j
=
M
∨
j
=
ran
⁡
1
st
⁡
R
6
5
simprbda
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
M
∈
Idl
⁡
R