Step |
Hyp |
Ref |
Expression |
1 |
|
prmidlval.1 |
|- B = ( Base ` R ) |
2 |
|
prmidlval.2 |
|- .x. = ( .r ` R ) |
3 |
|
raleq |
|- ( b = J -> ( A. y e. b ( x .x. y ) e. P <-> A. y e. J ( x .x. y ) e. P ) ) |
4 |
3
|
ralbidv |
|- ( b = J -> ( A. x e. I A. y e. b ( x .x. y ) e. P <-> A. x e. I A. y e. J ( x .x. y ) e. P ) ) |
5 |
|
sseq1 |
|- ( b = J -> ( b C_ P <-> J C_ P ) ) |
6 |
5
|
orbi2d |
|- ( b = J -> ( ( I C_ P \/ b C_ P ) <-> ( I C_ P \/ J C_ P ) ) ) |
7 |
4 6
|
imbi12d |
|- ( b = J -> ( ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) <-> ( A. x e. I A. y e. J ( x .x. y ) e. P -> ( I C_ P \/ J C_ P ) ) ) ) |
8 |
|
raleq |
|- ( a = I -> ( A. x e. a A. y e. b ( x .x. y ) e. P <-> A. x e. I A. y e. b ( x .x. y ) e. P ) ) |
9 |
|
sseq1 |
|- ( a = I -> ( a C_ P <-> I C_ P ) ) |
10 |
9
|
orbi1d |
|- ( a = I -> ( ( a C_ P \/ b C_ P ) <-> ( I C_ P \/ b C_ P ) ) ) |
11 |
8 10
|
imbi12d |
|- ( a = I -> ( ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) <-> ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) ) ) |
12 |
11
|
ralbidv |
|- ( a = I -> ( A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) <-> A. b e. ( LIdeal ` R ) ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) ) ) |
13 |
1 2
|
isprmidl |
|- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) |
14 |
13
|
biimpa |
|- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) |
15 |
14
|
simp3d |
|- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) |
16 |
15
|
adantr |
|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) |
17 |
|
simprl |
|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> I e. ( LIdeal ` R ) ) |
18 |
12 16 17
|
rspcdva |
|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> A. b e. ( LIdeal ` R ) ( A. x e. I A. y e. b ( x .x. y ) e. P -> ( I C_ P \/ b C_ P ) ) ) |
19 |
|
simprr |
|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> J e. ( LIdeal ` R ) ) |
20 |
7 18 19
|
rspcdva |
|- ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) -> ( A. x e. I A. y e. J ( x .x. y ) e. P -> ( I C_ P \/ J C_ P ) ) ) |
21 |
20
|
imp |
|- ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) ) /\ A. x e. I A. y e. J ( x .x. y ) e. P ) -> ( I C_ P \/ J C_ P ) ) |