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 ×˙=LSSummulGrpR
idlmulssprm.2 φRRing
idlmulssprm.3 No typesetting found for |- ( ph -> P e. ( PrmIdeal ` R ) ) with typecode |-
idlmulssprm.4 φILIdealR
idlmulssprm.5 φJLIdealR
idlmulssprm.6 φI×˙JP
Assertion idlmulssprm φIPJP

Proof

Step Hyp Ref Expression
1 idlmulssprm.1 ×˙=LSSummulGrpR
2 idlmulssprm.2 φRRing
3 idlmulssprm.3 Could not format ( ph -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ph -> P e. ( PrmIdeal ` R ) ) with typecode |-
4 idlmulssprm.4 φILIdealR
5 idlmulssprm.5 φJLIdealR
6 idlmulssprm.6 φI×˙JP
7 4 5 jca φILIdealRJLIdealR
8 6 ad2antrr φxIyJI×˙JP
9 eqid BaseR=BaseR
10 eqid R=R
11 eqid mulGrpR=mulGrpR
12 eqid LIdealR=LIdealR
13 9 12 lidlss ILIdealRIBaseR
14 4 13 syl φIBaseR
15 14 ad2antrr φxIyJIBaseR
16 9 12 lidlss JLIdealRJBaseR
17 5 16 syl φJBaseR
18 17 ad2antrr φxIyJJBaseR
19 simplr φxIyJxI
20 simpr φxIyJyJ
21 9 10 11 1 15 18 19 20 elringlsmd φxIyJxRyI×˙J
22 8 21 sseldd φxIyJxRyP
23 22 anasss φxIyJxRyP
24 23 ralrimivva φxIyJxRyP
25 9 10 prmidl Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
26 2 3 7 24 25 syl1111anc φIPJP