Metamath Proof Explorer

Definition df-prmidl

Description: Define the class of prime ideals of a ring R . A proper ideal I of R is prime if whenever A B C_ I for ideals A and B , either A C_ I or B C_ I . The more familiar definition using elements rather than ideals is equivalent provided R is commutative; see prmidl2 and isprmidlc . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 14-Jan-2024)

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprmidl 
 |-  PrmIdeal
1 vr 
 |-  r
2 crg 
 |-  Ring
3 vi 
 |-  i
4 clidl 
 |-  LIdeal
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( LIdeal ` r )
7 3 cv 
 |-  i
8 cbs 
 |-  Base
9 5 8 cfv 
 |-  ( Base ` r )
10 7 9 wne 
 |-  i =/= ( Base ` r )
11 va 
 |-  a
12 vb 
 |-  b
13 vx 
 |-  x
14 11 cv 
 |-  a
15 vy 
 |-  y
16 12 cv 
 |-  b
17 13 cv 
 |-  x
18 cmulr 
 |-  .r
19 5 18 cfv 
 |-  ( .r ` r )
20 15 cv 
 |-  y
21 17 20 19 co 
 |-  ( x ( .r ` r ) y )
22 21 7 wcel 
 |-  ( x ( .r ` r ) y ) e. i
23 22 15 16 wral 
 |-  A. y e. b ( x ( .r ` r ) y ) e. i
24 23 13 14 wral 
 |-  A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i
25 14 7 wss 
 |-  a C_ i
26 16 7 wss 
 |-  b C_ i
27 25 26 wo 
 |-  ( a C_ i \/ b C_ i )
28 24 27 wi 
 |-  ( A. x e. a A. y e. b ( x ( .r ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) )
29 28 12 6 wral 
 |-  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 ) )
30 29 11 6 wral 
 |-  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 ) )
31 10 30 wa 
 |-  ( 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 ) ) )
32 31 3 6 crab 
 |-  { 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 ) ) ) }
33 1 2 32 cmpt 
 |-  ( 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 ) ) ) } )
34 0 33 wceq 
 |-  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 ) ) ) } )