This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-pridl

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 ispridl2 and ispridlc . (Contributed by Jeff Madsen, 10-Jun-2010)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpridl 
 |-  PrIdl
1 vr 
 |-  r
2 crngo 
 |-  RingOps
3 vi 
 |-  i
4 cidl 
 |-  Idl
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Idl ` r )
7 3 cv 
 |-  i
8 c1st 
 |-  1st
9 5 8 cfv 
 |-  ( 1st ` r )
10 9 crn 
 |-  ran ( 1st ` r )
11 7 10 wne 
 |-  i =/= ran ( 1st ` r )
12 va 
 |-  a
13 vb 
 |-  b
14 vx 
 |-  x
15 12 cv 
 |-  a
16 vy 
 |-  y
17 13 cv 
 |-  b
18 14 cv 
 |-  x
19 c2nd 
 |-  2nd
20 5 19 cfv 
 |-  ( 2nd ` r )
21 16 cv 
 |-  y
22 18 21 20 co 
 |-  ( x ( 2nd ` r ) y )
23 22 7 wcel 
 |-  ( x ( 2nd ` r ) y ) e. i
24 23 16 17 wral 
 |-  A. y e. b ( x ( 2nd ` r ) y ) e. i
25 24 14 15 wral 
 |-  A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i
26 15 7 wss 
 |-  a C_ i
27 17 7 wss 
 |-  b C_ i
28 26 27 wo 
 |-  ( a C_ i \/ b C_ i )
29 25 28 wi 
 |-  ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) )
30 29 13 6 wral 
 |-  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 ) )
31 30 12 6 wral 
 |-  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 ) )
32 11 31 wa 
 |-  ( 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 ) ) )
33 32 3 6 crab 
 |-  { 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 ) ) ) }
34 1 2 33 cmpt 
 |-  ( 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 ) ) ) } )
35 0 34 wceq 
 |-  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 ) ) ) } )