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