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 e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( N ` A ) e. 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 e. RingOps /\ I e. ( Idl ` R ) ) -> I C_ ran G )
5 ssel2 
 |-  ( ( I C_ ran G /\ A e. I ) -> A e. ran G )
6 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
7 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
8 1 6 3 2 7 rngonegmn1l 
 |-  ( ( R e. RingOps /\ A e. ran G ) -> ( N ` A ) = ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) )
9 5 8 sylan2 
 |-  ( ( R e. RingOps /\ ( I C_ ran G /\ A e. I ) ) -> ( N ` A ) = ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) )
10 9 anassrs 
 |-  ( ( ( R e. RingOps /\ I C_ ran G ) /\ A e. I ) -> ( N ` A ) = ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) )
11 4 10 syldanl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( N ` A ) = ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) )
12 1 rneqi 
 |-  ran G = ran ( 1st ` R )
13 12 6 7 rngo1cl 
 |-  ( R e. RingOps -> ( GId ` ( 2nd ` R ) ) e. ran G )
14 1 3 2 rngonegcl 
 |-  ( ( R e. RingOps /\ ( GId ` ( 2nd ` R ) ) e. ran G ) -> ( N ` ( GId ` ( 2nd ` R ) ) ) e. ran G )
15 13 14 mpdan 
 |-  ( R e. RingOps -> ( N ` ( GId ` ( 2nd ` R ) ) ) e. ran G )
16 15 ad2antrr 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( N ` ( GId ` ( 2nd ` R ) ) ) e. ran G )
17 1 6 3 idllmulcl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ ( N ` ( GId ` ( 2nd ` R ) ) ) e. ran G ) ) -> ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) e. I )
18 17 anassrs 
 |-  ( ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) /\ ( N ` ( GId ` ( 2nd ` R ) ) ) e. ran G ) -> ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) e. I )
19 16 18 mpdan 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( ( N ` ( GId ` ( 2nd ` R ) ) ) ( 2nd ` R ) A ) e. I )
20 11 19 eqeltrd 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> ( N ` A ) e. I )