Metamath Proof Explorer


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