Metamath Proof Explorer

Theorem idlsubcl

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

Ref Expression
Hypotheses idlsubcl.1 
|- G = ( 1st ` R )
idlsubcl.2 
|- D = ( /g ` G )
Assertion idlsubcl 
|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A D B ) e. I )

Proof

Step Hyp Ref Expression
1 idlsubcl.1 
 |-  G = ( 1st ` R )
2 idlsubcl.2 
 |-  D = ( /g ` G )
3 eqid 
 |-  ran G = ran G
4 1 3 idlcl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> A e. ran G )
5 1 3 idlcl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ B e. I ) -> B e. ran G )
6 4 5 anim12dan 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A e. ran G /\ B e. ran G ) )
7 eqid 
 |-  ( inv ` G ) = ( inv ` G )
8 1 3 7 2 rngosub 
 |-  ( ( R e. RingOps /\ A e. ran G /\ B e. ran G ) -> ( A D B ) = ( A G ( ( inv ` G ) ` B ) ) )
9 8 3expb 
 |-  ( ( R e. RingOps /\ ( A e. ran G /\ B e. ran G ) ) -> ( A D B ) = ( A G ( ( inv ` G ) ` B ) ) )
10 9 adantlr 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. ran G /\ B e. ran G ) ) -> ( A D B ) = ( A G ( ( inv ` G ) ` B ) ) )
11 6 10 syldan 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A D B ) = ( A G ( ( inv ` G ) ` B ) ) )
12 simprl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> A e. I )
13 1 7 idlnegcl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ B e. I ) -> ( ( inv ` G ) ` B ) e. I )
14 13 adantrl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( ( inv ` G ) ` B ) e. I )
15 12 14 jca 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A e. I /\ ( ( inv ` G ) ` B ) e. I ) )
16 1 idladdcl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ ( ( inv ` G ) ` B ) e. I ) ) -> ( A G ( ( inv ` G ) ` B ) ) e. I )
17 15 16 syldan 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A G ( ( inv ` G ) ` B ) ) e. I )
18 11 17 eqeltrd 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. I ) ) -> ( A D B ) e. I )