Metamath Proof Explorer


Theorem ispridl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ispridl2.1
|- G = ( 1st ` R )
ispridl2.2
|- H = ( 2nd ` R )
ispridl2.3
|- X = ran G
Assertion ispridl2
|- ( ( R e. RingOps /\ ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) ) -> P e. ( PrIdl ` R ) )

Proof

Step Hyp Ref Expression
1 ispridl2.1
 |-  G = ( 1st ` R )
2 ispridl2.2
 |-  H = ( 2nd ` R )
3 ispridl2.3
 |-  X = ran G
4 1 3 idlss
 |-  ( ( R e. RingOps /\ r e. ( Idl ` R ) ) -> r C_ X )
5 ssralv
 |-  ( r C_ X -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
6 4 5 syl
 |-  ( ( R e. RingOps /\ r e. ( Idl ` R ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
7 6 adantrr
 |-  ( ( R e. RingOps /\ ( r e. ( Idl ` R ) /\ s e. ( Idl ` R ) ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
8 1 3 idlss
 |-  ( ( R e. RingOps /\ s e. ( Idl ` R ) ) -> s C_ X )
9 ssralv
 |-  ( s C_ X -> ( A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
10 9 ralimdv
 |-  ( s C_ X -> ( A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
11 8 10 syl
 |-  ( ( R e. RingOps /\ s e. ( Idl ` R ) ) -> ( A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
12 11 adantrl
 |-  ( ( R e. RingOps /\ ( r e. ( Idl ` R ) /\ s e. ( Idl ` R ) ) ) -> ( A. a e. r A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
13 7 12 syld
 |-  ( ( R e. RingOps /\ ( r e. ( Idl ` R ) /\ s e. ( Idl ` R ) ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
14 13 adantlr
 |-  ( ( ( R e. RingOps /\ P e. ( Idl ` R ) ) /\ ( r e. ( Idl ` R ) /\ s e. ( Idl ` R ) ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
15 r19.26-2
 |-  ( A. a e. r A. b e. s ( ( a H b ) e. P /\ ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) <-> ( A. a e. r A. b e. s ( a H b ) e. P /\ A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
16 pm3.35
 |-  ( ( ( a H b ) e. P /\ ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> ( a e. P \/ b e. P ) )
17 16 2ralimi
 |-  ( A. a e. r A. b e. s ( ( a H b ) e. P /\ ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> A. a e. r A. b e. s ( a e. P \/ b e. P ) )
18 2ralor
 |-  ( A. a e. r A. b e. s ( a e. P \/ b e. P ) <-> ( A. a e. r a e. P \/ A. b e. s b e. P ) )
19 dfss3
 |-  ( r C_ P <-> A. a e. r a e. P )
20 dfss3
 |-  ( s C_ P <-> A. b e. s b e. P )
21 19 20 orbi12i
 |-  ( ( r C_ P \/ s C_ P ) <-> ( A. a e. r a e. P \/ A. b e. s b e. P ) )
22 18 21 sylbb2
 |-  ( A. a e. r A. b e. s ( a e. P \/ b e. P ) -> ( r C_ P \/ s C_ P ) )
23 17 22 syl
 |-  ( A. a e. r A. b e. s ( ( a H b ) e. P /\ ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> ( r C_ P \/ s C_ P ) )
24 15 23 sylbir
 |-  ( ( A. a e. r A. b e. s ( a H b ) e. P /\ A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> ( r C_ P \/ s C_ P ) )
25 24 expcom
 |-  ( A. a e. r A. b e. s ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) )
26 14 25 syl6
 |-  ( ( ( R e. RingOps /\ P e. ( Idl ` R ) ) /\ ( r e. ( Idl ` R ) /\ s e. ( Idl ` R ) ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) )
27 26 ralrimdvva
 |-  ( ( R e. RingOps /\ P e. ( Idl ` R ) ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) )
28 27 ex
 |-  ( R e. RingOps -> ( P e. ( Idl ` R ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) ) )
29 28 adantrd
 |-  ( R e. RingOps -> ( ( P e. ( Idl ` R ) /\ P =/= X ) -> ( A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) -> A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) ) )
30 29 imdistand
 |-  ( R e. RingOps -> ( ( ( P e. ( Idl ` R ) /\ P =/= X ) /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> ( ( P e. ( Idl ` R ) /\ P =/= X ) /\ A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) ) )
31 df-3an
 |-  ( ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) <-> ( ( P e. ( Idl ` R ) /\ P =/= X ) /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) )
32 df-3an
 |-  ( ( P e. ( Idl ` R ) /\ P =/= X /\ A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) <-> ( ( P e. ( Idl ` R ) /\ P =/= X ) /\ A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) )
33 30 31 32 3imtr4g
 |-  ( R e. RingOps -> ( ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> ( P e. ( Idl ` R ) /\ P =/= X /\ A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) ) )
34 1 2 3 ispridl
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. r e. ( Idl ` R ) A. s e. ( Idl ` R ) ( A. a e. r A. b e. s ( a H b ) e. P -> ( r C_ P \/ s C_ P ) ) ) ) )
35 33 34 sylibrd
 |-  ( R e. RingOps -> ( ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) -> P e. ( PrIdl ` R ) ) )
36 35 imp
 |-  ( ( R e. RingOps /\ ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) ) -> P e. ( PrIdl ` R ) )