Metamath Proof Explorer

Theorem isidl

Description: The predicate "is an ideal of the 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 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 ) ) ) ) )

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 1 2 3 4 idlval 
 |-  ( R e. RingOps -> ( Idl ` R ) = { i e. ~P 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 ) ) ) } )
6 5 eleq2d 
 |-  ( R e. RingOps -> ( I e. ( Idl ` R ) <-> I e. { i e. ~P 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 1 fvexi 
 |-  G e. _V
8 7 rnex 
 |-  ran G e. _V
9 3 8 eqeltri 
 |-  X e. _V
10 9 elpw2 
 |-  ( I e. ~P X <-> I C_ X )
11 10 anbi1i 
 |-  ( ( I e. ~P 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 ) ) ) ) )
12 eleq2 
 |-  ( i = I -> ( Z e. i <-> Z e. I ) )
13 eleq2 
 |-  ( i = I -> ( ( x G y ) e. i <-> ( x G y ) e. I ) )
14 13 raleqbi1dv 
 |-  ( i = I -> ( A. y e. i ( x G y ) e. i <-> A. y e. I ( x G y ) e. I ) )
15 eleq2 
 |-  ( i = I -> ( ( z H x ) e. i <-> ( z H x ) e. I ) )
16 eleq2 
 |-  ( i = I -> ( ( x H z ) e. i <-> ( x H z ) e. I ) )
17 15 16 anbi12d 
 |-  ( i = I -> ( ( ( z H x ) e. i /\ ( x H z ) e. i ) <-> ( ( z H x ) e. I /\ ( x H z ) e. I ) ) )
18 17 ralbidv 
 |-  ( i = I -> ( A. z e. X ( ( z H x ) e. i /\ ( x H z ) e. i ) <-> A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) )
19 14 18 anbi12d 
 |-  ( i = 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 /\ ( x H z ) e. I ) ) ) )
20 19 raleqbi1dv 
 |-  ( i = 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 /\ ( x H z ) e. I ) ) ) )
21 12 20 anbi12d 
 |-  ( i = I -> ( ( 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 ) ) ) <-> ( 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 ) ) ) ) )
22 21 elrab 
 |-  ( I e. { i e. ~P 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 e. ~P 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 3anass 
 |-  ( ( 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 ) ) ) ) )
24 11 22 23 3bitr4i 
 |-  ( I e. { i e. ~P 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 ) ) ) )
25 6 24 bitrdi 
 |-  ( 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 ) ) ) ) )