Metamath Proof Explorer

Theorem prmidlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 
|- B = ( Base ` R )
prmidlval.2 
|- .x. = ( .r ` R )
Assertion prmidlval 
|- ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )

Proof

Step Hyp Ref Expression
1 prmidlval.1 
 |-  B = ( Base ` R )
2 prmidlval.2 
 |-  .x. = ( .r ` R )
3 df-prmidl 
 |-  PrmIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
4 fveq2 
 |-  ( r = R -> ( LIdeal ` r ) = ( LIdeal ` R ) )
5 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
7 6 neeq2d 
 |-  ( r = R -> ( i =/= ( Base ` r ) <-> i =/= B ) )
8 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
9 8 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
10 9 oveqd 
 |-  ( r = R -> ( x ( .r ` r ) y ) = ( x .x. y ) )
11 10 eleq1d 
 |-  ( r = R -> ( ( x ( .r ` r ) y ) e. i <-> ( x .x. y ) e. i ) )
12 11 2ralbidv 
 |-  ( r = R -> ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i <-> A. x e. a A. y e. b ( x .x. y ) e. i ) )
13 12 imbi1d 
 |-  ( r = R -> ( ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
14 4 13 raleqbidv 
 |-  ( r = R -> ( A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
15 4 14 raleqbidv 
 |-  ( r = R -> ( A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) )
16 7 15 anbi12d 
 |-  ( r = R -> ( ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) <-> ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) ) )
17 4 16 rabeqbidv 
 |-  ( r = R -> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. a e. ( LIdeal ` r ) A. b e. ( LIdeal ` r ) ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
18 id 
 |-  ( R e. Ring -> R e. Ring )
19 eqid 
 |-  { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) }
20 fvexd 
 |-  ( R e. Ring -> ( LIdeal ` R ) e. _V )
21 19 20 rabexd 
 |-  ( R e. Ring -> { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } e. _V )
22 3 17 18 21 fvmptd3 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )