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 | |
|
idlmulssprm.2 | |
||
idlmulssprm.3 | No typesetting found for |- ( ph -> P e. ( PrmIdeal ` R ) ) with typecode |- | ||
idlmulssprm.4 | |
||
idlmulssprm.5 | |
||
idlmulssprm.6 | |
||
Assertion | idlmulssprm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idlmulssprm.1 | |
|
2 | idlmulssprm.2 | |
|
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 | |
|
5 | idlmulssprm.5 | |
|
6 | idlmulssprm.6 | |
|
7 | 4 5 | jca | |
8 | 6 | ad2antrr | |
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 9 12 | lidlss | |
14 | 4 13 | syl | |
15 | 14 | ad2antrr | |
16 | 9 12 | lidlss | |
17 | 5 16 | syl | |
18 | 17 | ad2antrr | |
19 | simplr | |
|
20 | simpr | |
|
21 | 9 10 11 1 15 18 19 20 | elringlsmd | |
22 | 8 21 | sseldd | |
23 | 22 | anasss | |
24 | 23 | ralrimivva | |
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 | |