Metamath Proof Explorer

Theorem idlnegcl

Description: An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlnegcl.1 ⊢G=1st⁡R
idlnegcl.2 ⊢N=inv⁡G
Assertion idlnegcl ⊢R∈RingOps∧I∈Idl⁡R∧A∈I→N⁡A∈I

Proof

Step Hyp Ref Expression
1 idlnegcl.1 ⊢G=1st⁡R
2 idlnegcl.2 ⊢N=inv⁡G
3 eqid ⊢ran⁡G=ran⁡G
4 1 3 idlss ⊢R∈RingOps∧I∈Idl⁡R→I⊆ran⁡G
5 ssel2 ⊢I⊆ran⁡G∧A∈I→A∈ran⁡G
6 eqid ⊢2nd⁡R=2nd⁡R
7 eqid ⊢GId⁡2nd⁡R=GId⁡2nd⁡R
8 1 6 3 2 7 rngonegmn1l ⊢R∈RingOps∧A∈ran⁡G→N⁡A=N⁡GId⁡2nd⁡R2nd⁡RA
9 5 8 sylan2 ⊢R∈RingOps∧I⊆ran⁡G∧A∈I→N⁡A=N⁡GId⁡2nd⁡R2nd⁡RA
10 9 anassrs ⊢R∈RingOps∧I⊆ran⁡G∧A∈I→N⁡A=N⁡GId⁡2nd⁡R2nd⁡RA
11 4 10 syldanl ⊢R∈RingOps∧I∈Idl⁡R∧A∈I→N⁡A=N⁡GId⁡2nd⁡R2nd⁡RA
12 1 rneqi ⊢ran⁡G=ran⁡1st⁡R
13 12 6 7 rngo1cl ⊢R∈RingOps→GId⁡2nd⁡R∈ran⁡G
14 1 3 2 rngonegcl ⊢R∈RingOps∧GId⁡2nd⁡R∈ran⁡G→N⁡GId⁡2nd⁡R∈ran⁡G
15 13 14 mpdan ⊢R∈RingOps→N⁡GId⁡2nd⁡R∈ran⁡G
16 15 ad2antrr ⊢R∈RingOps∧I∈Idl⁡R∧A∈I→N⁡GId⁡2nd⁡R∈ran⁡G
17 1 6 3 idllmulcl ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧N⁡GId⁡2nd⁡R∈ran⁡G→N⁡GId⁡2nd⁡R2nd⁡RA∈I
18 17 anassrs ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧N⁡GId⁡2nd⁡R∈ran⁡G→N⁡GId⁡2nd⁡R2nd⁡RA∈I
19 16 18 mpdan ⊢R∈RingOps∧I∈Idl⁡R∧A∈I→N⁡GId⁡2nd⁡R2nd⁡RA∈I
20 11 19 eqeltrd ⊢R∈RingOps∧I∈Idl⁡R∧A∈I→N⁡A∈I