Metamath Proof Explorer

Theorem pridlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses pridlval.1 
|- G = ( 1st ` R )
pridlval.2 
|- H = ( 2nd ` R )
pridlval.3 
|- X = ran G
Assertion pridlval 
|- ( R e. RingOps -> ( PrIdl ` R ) = { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )

Proof

Step Hyp Ref Expression
1 pridlval.1 
 |-  G = ( 1st ` R )
2 pridlval.2 
 |-  H = ( 2nd ` R )
3 pridlval.3 
 |-  X = ran G
4 fveq2 
 |-  ( r = R -> ( Idl ` r ) = ( Idl ` R ) )
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 neeq2d 
 |-  ( r = R -> ( i =/= ran ( 1st ` r ) <-> i =/= X ) )
10 fveq2 
 |-  ( r = R -> ( 2nd ` r ) = ( 2nd ` R ) )
11 10 2 eqtr4di 
 |-  ( r = R -> ( 2nd ` r ) = H )
12 11 oveqd 
 |-  ( r = R -> ( x ( 2nd ` r ) y ) = ( x H y ) )
13 12 eleq1d 
 |-  ( r = R -> ( ( x ( 2nd ` r ) y ) e. i <-> ( x H y ) e. i ) )
14 13 2ralbidv 
 |-  ( r = R -> ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i <-> A. x e. a A. y e. b ( x H y ) e. i ) )
15 14 imbi1d 
 |-  ( r = R -> ( ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
16 4 15 raleqbidv 
 |-  ( r = R -> ( A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
17 4 16 raleqbidv 
 |-  ( r = R -> ( A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
18 9 17 anbi12d 
 |-  ( r = R -> ( ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) <-> ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) ) )
19 4 18 rabeqbidv 
 |-  ( r = R -> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } = { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
20 df-pridl 
 |-  PrIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
21 fvex 
 |-  ( Idl ` R ) e. _V
22 21 rabex 
 |-  { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } e. _V
23 19 20 22 fvmpt 
 |-  ( R e. RingOps -> ( PrIdl ` R ) = { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )