Metamath Proof Explorer

Theorem idlmulssprm

Description: Let P be a prime ideal containing the product ( I .X. J ) of two ideals I and J . Then I C_ P or J C_ P . (Contributed by Thierry Arnoux, 13-Apr-2024)

Ref Expression
Hypotheses idlmulssprm.1 
|- .X. = ( LSSum ` ( mulGrp ` R ) )
idlmulssprm.2 
|- ( ph -> R e. Ring )
idlmulssprm.3 
|- ( ph -> P e. ( PrmIdeal ` R ) )
idlmulssprm.4 
|- ( ph -> I e. ( LIdeal ` R ) )
idlmulssprm.5 
|- ( ph -> J e. ( LIdeal ` R ) )
idlmulssprm.6 
|- ( ph -> ( I .X. J ) C_ P )
Assertion idlmulssprm 
|- ( ph -> ( I C_ P \/ J C_ P ) )

Proof

Step Hyp Ref Expression
1 idlmulssprm.1 
 |-  .X. = ( LSSum ` ( mulGrp ` R ) )
2 idlmulssprm.2 
 |-  ( ph -> R e. Ring )
3 idlmulssprm.3 
 |-  ( ph -> P e. ( PrmIdeal ` R ) )
4 idlmulssprm.4 
 |-  ( ph -> I e. ( LIdeal ` R ) )
5 idlmulssprm.5 
 |-  ( ph -> J e. ( LIdeal ` R ) )
6 idlmulssprm.6 
 |-  ( ph -> ( I .X. J ) C_ P )
7 4 5 jca 
 |-  ( ph -> ( I e. ( LIdeal ` R ) /\ J e. ( LIdeal ` R ) ) )
8 6 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( I .X. J ) C_ P )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
12 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
13 9 12 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ ( Base ` R ) )
14 4 13 syl 
 |-  ( ph -> I C_ ( Base ` R ) )
15 14 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> I C_ ( Base ` R ) )
16 9 12 lidlss 
 |-  ( J e. ( LIdeal ` R ) -> J C_ ( Base ` R ) )
17 5 16 syl 
 |-  ( ph -> J C_ ( Base ` R ) )
18 17 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> J C_ ( Base ` R ) )
19 simplr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> x e. I )
20 simpr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> y e. J )
21 9 10 11 1 15 18 19 20 elringlsmd 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( x ( .r ` R ) y ) e. ( I .X. J ) )
22 8 21 sseldd 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( x ( .r ` R ) y ) e. P )
23 22 anasss 
 |-  ( ( ph /\ ( x e. I /\ y e. J ) ) -> ( x ( .r ` R ) y ) e. P )
24 23 ralrimivva 
 |-  ( ph -> A. x e. I A. y e. J ( x ( .r ` R ) y ) e. P )
25 9 10 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 ( .r ` R ) y ) e. P ) -> ( I C_ P \/ J C_ P ) )
26 2 3 7 24 25 syl1111anc 
 |-  ( ph -> ( I C_ P \/ J C_ P ) )