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

Metamath Proof Explorer

Theorem prmidl

Description: The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 
|- B = ( Base ` R )
prmidlval.2 
|- .x. = ( .r ` R )
Assertion prmidl 
|- ( ( ( ( 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 ) )

Proof

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