Metamath Proof Explorer

Theorem isidlc

Description: The predicate "is an ideal of the commutative ring R ". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlval.1 
|- G = ( 1st ` R )
idlval.2 
|- H = ( 2nd ` R )
idlval.3 
|- X = ran G
idlval.4 
|- Z = ( GId ` G )
Assertion isidlc 
|- ( R e. CRingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) ) )

Proof

Step Hyp Ref Expression
1 idlval.1 
 |-  G = ( 1st ` R )
2 idlval.2 
 |-  H = ( 2nd ` R )
3 idlval.3 
 |-  X = ran G
4 idlval.4 
 |-  Z = ( GId ` G )
5 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
6 1 2 3 4 isidl 
 |-  ( R e. RingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) ) )
7 5 6 syl 
 |-  ( R e. CRingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) ) )
8 ssel2 
 |-  ( ( I C_ X /\ x e. I ) -> x e. X )
9 1 2 3 crngocom 
 |-  ( ( R e. CRingOps /\ x e. X /\ z e. X ) -> ( x H z ) = ( z H x ) )
10 9 eleq1d 
 |-  ( ( R e. CRingOps /\ x e. X /\ z e. X ) -> ( ( x H z ) e. I <-> ( z H x ) e. I ) )
11 10 biimprd 
 |-  ( ( R e. CRingOps /\ x e. X /\ z e. X ) -> ( ( z H x ) e. I -> ( x H z ) e. I ) )
12 11 3expa 
 |-  ( ( ( R e. CRingOps /\ x e. X ) /\ z e. X ) -> ( ( z H x ) e. I -> ( x H z ) e. I ) )
13 12 pm4.71d 
 |-  ( ( ( R e. CRingOps /\ x e. X ) /\ z e. X ) -> ( ( z H x ) e. I <-> ( ( z H x ) e. I /\ ( x H z ) e. I ) ) )
14 13 bicomd 
 |-  ( ( ( R e. CRingOps /\ x e. X ) /\ z e. X ) -> ( ( ( z H x ) e. I /\ ( x H z ) e. I ) <-> ( z H x ) e. I ) )
15 14 ralbidva 
 |-  ( ( R e. CRingOps /\ x e. X ) -> ( A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) <-> A. z e. X ( z H x ) e. I ) )
16 15 anbi2d 
 |-  ( ( R e. CRingOps /\ x e. X ) -> ( ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) <-> ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
17 8 16 sylan2 
 |-  ( ( R e. CRingOps /\ ( I C_ X /\ x e. I ) ) -> ( ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) <-> ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
18 17 anassrs 
 |-  ( ( ( R e. CRingOps /\ I C_ X ) /\ x e. I ) -> ( ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) <-> ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
19 18 ralbidva 
 |-  ( ( R e. CRingOps /\ I C_ X ) -> ( A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) <-> A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
20 19 adantrr 
 |-  ( ( R e. CRingOps /\ ( I C_ X /\ Z e. I ) ) -> ( A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) <-> A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
21 20 pm5.32da 
 |-  ( R e. CRingOps -> ( ( ( I C_ X /\ Z e. I ) /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) <-> ( ( I C_ X /\ Z e. I ) /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) ) )
22 df-3an 
 |-  ( ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) <-> ( ( I C_ X /\ Z e. I ) /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) )
23 df-3an 
 |-  ( ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) <-> ( ( I C_ X /\ Z e. I ) /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) )
24 21 22 23 3bitr4g 
 |-  ( R e. CRingOps -> ( ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) ) )
25 7 24 bitrd 
 |-  ( R e. CRingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( z H x ) e. I ) ) ) )