Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
lidlnegcl
Next ⟩
lidlsubg
Metamath Proof Explorer
Ascii
Unicode
Theorem
lidlnegcl
Description:
An ideal contains negatives.
(Contributed by
Stefan O'Rear
, 3-Jan-2015)
Ref
Expression
Hypotheses
lidlcl.u
⊢
U
=
LIdeal
⁡
R
lidlnegcl.n
⊢
N
=
inv
g
⁡
R
Assertion
lidlnegcl
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
N
⁡
X
∈
I
Proof
Step
Hyp
Ref
Expression
1
lidlcl.u
⊢
U
=
LIdeal
⁡
R
2
lidlnegcl.n
⊢
N
=
inv
g
⁡
R
3
rlmvneg
⊢
inv
g
⁡
R
=
inv
g
⁡
ringLMod
⁡
R
4
2
3
eqtri
⊢
N
=
inv
g
⁡
ringLMod
⁡
R
5
4
fveq1i
⊢
N
⁡
X
=
inv
g
⁡
ringLMod
⁡
R
⁡
X
6
rlmlmod
⊢
R
∈
Ring
→
ringLMod
⁡
R
∈
LMod
7
6
3ad2ant1
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
ringLMod
⁡
R
∈
LMod
8
simpr
⊢
R
∈
Ring
∧
I
∈
U
→
I
∈
U
9
lidlval
⊢
LIdeal
⁡
R
=
LSubSp
⁡
ringLMod
⁡
R
10
1
9
eqtri
⊢
U
=
LSubSp
⁡
ringLMod
⁡
R
11
8
10
eleqtrdi
⊢
R
∈
Ring
∧
I
∈
U
→
I
∈
LSubSp
⁡
ringLMod
⁡
R
12
11
3adant3
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
I
∈
LSubSp
⁡
ringLMod
⁡
R
13
simp3
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
X
∈
I
14
eqid
⊢
LSubSp
⁡
ringLMod
⁡
R
=
LSubSp
⁡
ringLMod
⁡
R
15
eqid
⊢
inv
g
⁡
ringLMod
⁡
R
=
inv
g
⁡
ringLMod
⁡
R
16
14
15
lssvnegcl
⊢
ringLMod
⁡
R
∈
LMod
∧
I
∈
LSubSp
⁡
ringLMod
⁡
R
∧
X
∈
I
→
inv
g
⁡
ringLMod
⁡
R
⁡
X
∈
I
17
7
12
13
16
syl3anc
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
inv
g
⁡
ringLMod
⁡
R
⁡
X
∈
I
18
5
17
eqeltrid
⊢
R
∈
Ring
∧
I
∈
U
∧
X
∈
I
→
N
⁡
X
∈
I