Metamath Proof Explorer

Theorem pridl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypothesis pridl.1 
|- H = ( 2nd ` R )
Assertion pridl 
|- ( ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( Idl ` R ) /\ B e. ( Idl ` R ) /\ A. x e. A A. y e. B ( x H y ) e. P ) ) -> ( A C_ P \/ B C_ P ) )

Proof

Step Hyp Ref Expression
1 pridl.1 
 |-  H = ( 2nd ` R )
2 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
3 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
4 2 1 3 ispridl 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
5 df-3an 
 |-  ( ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) <-> ( ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
6 4 5 bitrdi 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
7 6 simplbda 
 |-  ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) )
8 raleq 
 |-  ( a = A -> ( A. x e. a A. y e. b ( x H y ) e. P <-> A. x e. A A. y e. b ( x H y ) e. P ) )
9 sseq1 
 |-  ( a = A -> ( a C_ P <-> A C_ P ) )
10 9 orbi1d 
 |-  ( a = A -> ( ( a C_ P \/ b C_ P ) <-> ( A C_ P \/ b C_ P ) ) )
11 8 10 imbi12d 
 |-  ( a = A -> ( ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) <-> ( A. x e. A A. y e. b ( x H y ) e. P -> ( A C_ P \/ b C_ P ) ) ) )
12 raleq 
 |-  ( b = B -> ( A. y e. b ( x H y ) e. P <-> A. y e. B ( x H y ) e. P ) )
13 12 ralbidv 
 |-  ( b = B -> ( A. x e. A A. y e. b ( x H y ) e. P <-> A. x e. A A. y e. B ( x H y ) e. P ) )
14 sseq1 
 |-  ( b = B -> ( b C_ P <-> B C_ P ) )
15 14 orbi2d 
 |-  ( b = B -> ( ( A C_ P \/ b C_ P ) <-> ( A C_ P \/ B C_ P ) ) )
16 13 15 imbi12d 
 |-  ( b = B -> ( ( A. x e. A A. y e. b ( x H y ) e. P -> ( A C_ P \/ b C_ P ) ) <-> ( A. x e. A A. y e. B ( x H y ) e. P -> ( A C_ P \/ B C_ P ) ) ) )
17 11 16 rspc2v 
 |-  ( ( A e. ( Idl ` R ) /\ B e. ( Idl ` R ) ) -> ( A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) -> ( A. x e. A A. y e. B ( x H y ) e. P -> ( A C_ P \/ B C_ P ) ) ) )
18 7 17 syl5com 
 |-  ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> ( ( A e. ( Idl ` R ) /\ B e. ( Idl ` R ) ) -> ( A. x e. A A. y e. B ( x H y ) e. P -> ( A C_ P \/ B C_ P ) ) ) )
19 18 expd 
 |-  ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> ( A e. ( Idl ` R ) -> ( B e. ( Idl ` R ) -> ( A. x e. A A. y e. B ( x H y ) e. P -> ( A C_ P \/ B C_ P ) ) ) ) )
20 19 3imp2 
 |-  ( ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( Idl ` R ) /\ B e. ( Idl ` R ) /\ A. x e. A A. y e. B ( x H y ) e. P ) ) -> ( A C_ P \/ B C_ P ) )