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

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 ) )