Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ideals
maxidln1
Next ⟩
maxidln0
Metamath Proof Explorer
Ascii
Unicode
Theorem
maxidln1
Description:
One is not contained in any maximal ideal.
(Contributed by
Jeff Madsen
, 17-Jun-2011)
Ref
Expression
Hypotheses
maxidln1.1
⊢
H
=
2
nd
⁡
R
maxidln1.2
⊢
U
=
GId
⁡
H
Assertion
maxidln1
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
¬
U
∈
M
Proof
Step
Hyp
Ref
Expression
1
maxidln1.1
⊢
H
=
2
nd
⁡
R
2
maxidln1.2
⊢
U
=
GId
⁡
H
3
eqid
⊢
1
st
⁡
R
=
1
st
⁡
R
4
eqid
⊢
ran
⁡
1
st
⁡
R
=
ran
⁡
1
st
⁡
R
5
3
4
maxidlnr
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
M
≠
ran
⁡
1
st
⁡
R
6
maxidlidl
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
M
∈
Idl
⁡
R
7
3
1
4
2
1idl
⊢
R
∈
RingOps
∧
M
∈
Idl
⁡
R
→
U
∈
M
↔
M
=
ran
⁡
1
st
⁡
R
8
7
necon3bbid
⊢
R
∈
RingOps
∧
M
∈
Idl
⁡
R
→
¬
U
∈
M
↔
M
≠
ran
⁡
1
st
⁡
R
9
6
8
syldan
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
¬
U
∈
M
↔
M
≠
ran
⁡
1
st
⁡
R
10
5
9
mpbird
⊢
R
∈
RingOps
∧
M
∈
MaxIdl
⁡
R
→
¬
U
∈
M