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 = 2 nd R
Assertion pridl R RingOps P PrIdl R A Idl R B Idl R x A y B x H y P A P B P

Proof

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