Metamath Proof Explorer

Theorem idlval

Description: The class of ideals of a ring. (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 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 ) ) ) } )

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 fveq2 
 |-  ( r = R -> ( 1st ` r ) = ( 1st ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( 1st ` r ) = G )
7 6 rneqd 
 |-  ( r = R -> ran ( 1st ` r ) = ran G )
8 7 3 eqtr4di 
 |-  ( r = R -> ran ( 1st ` r ) = X )
9 8 pweqd 
 |-  ( r = R -> ~P ran ( 1st ` r ) = ~P X )
10 6 fveq2d 
 |-  ( r = R -> ( GId ` ( 1st ` r ) ) = ( GId ` G ) )
11 10 4 eqtr4di 
 |-  ( r = R -> ( GId ` ( 1st ` r ) ) = Z )
12 11 eleq1d 
 |-  ( r = R -> ( ( GId ` ( 1st ` r ) ) e. i <-> Z e. i ) )
13 6 oveqd 
 |-  ( r = R -> ( x ( 1st ` r ) y ) = ( x G y ) )
14 13 eleq1d 
 |-  ( r = R -> ( ( x ( 1st ` r ) y ) e. i <-> ( x G y ) e. i ) )
15 14 ralbidv 
 |-  ( r = R -> ( A. y e. i ( x ( 1st ` r ) y ) e. i <-> A. y e. i ( x G y ) e. i ) )
16 fveq2 
 |-  ( r = R -> ( 2nd ` r ) = ( 2nd ` R ) )
17 16 2 eqtr4di 
 |-  ( r = R -> ( 2nd ` r ) = H )
18 17 oveqd 
 |-  ( r = R -> ( z ( 2nd ` r ) x ) = ( z H x ) )
19 18 eleq1d 
 |-  ( r = R -> ( ( z ( 2nd ` r ) x ) e. i <-> ( z H x ) e. i ) )
20 17 oveqd 
 |-  ( r = R -> ( x ( 2nd ` r ) z ) = ( x H z ) )
21 20 eleq1d 
 |-  ( r = R -> ( ( x ( 2nd ` r ) z ) e. i <-> ( x H z ) e. i ) )
22 19 21 anbi12d 
 |-  ( r = R -> ( ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i ) <-> ( ( z H x ) e. i /\ ( x H z ) e. i ) ) )
23 8 22 raleqbidv 
 |-  ( r = R -> ( A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i ) <-> A. z e. X ( ( z H x ) e. i /\ ( x H z ) e. i ) ) )
24 15 23 anbi12d 
 |-  ( r = R -> ( ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) 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 ) ) ) )
25 24 ralbidv 
 |-  ( r = R -> ( A. x e. i ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) 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 ) ) ) )
26 12 25 anbi12d 
 |-  ( r = R -> ( ( ( GId ` ( 1st ` r ) ) e. i /\ A. x e. i ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) 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 ) ) ) ) )
27 9 26 rabeqbidv 
 |-  ( r = R -> { i e. ~P ran ( 1st ` r ) | ( ( GId ` ( 1st ` r ) ) e. i /\ A. x e. i ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) 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 ) ) ) } )
28 df-idl 
 |-  Idl = ( r e. RingOps |-> { i e. ~P ran ( 1st ` r ) | ( ( GId ` ( 1st ` r ) ) e. i /\ A. x e. i ( A. y e. i ( x ( 1st ` r ) y ) e. i /\ A. z e. ran ( 1st ` r ) ( ( z ( 2nd ` r ) x ) e. i /\ ( x ( 2nd ` r ) z ) e. i ) ) ) } )
29 1 fvexi 
 |-  G e. _V
30 29 rnex 
 |-  ran G e. _V
31 3 30 eqeltri 
 |-  X e. _V
32 31 pwex 
 |-  ~P X e. _V
33 32 rabex 
 |-  { 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 ) ) ) } e. _V
34 27 28 33 fvmpt 
 |-  ( 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 ) ) ) } )