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	$⊢ \underset{˙}{\times} = LSSum ({mulGrp}_{R})$
	idlmulssprm.2	$⊢ φ \to R \in Ring$
	idlmulssprm.3	$⊢ φ \to P \in PrmIdeal (R)$
	idlmulssprm.4	$⊢ φ \to I \in LIdeal (R)$
	idlmulssprm.5	$⊢ φ \to J \in LIdeal (R)$
	idlmulssprm.6	$⊢ φ \to I \underset{˙}{\times} J \subseteq P$
Assertion	idlmulssprm	$⊢ φ \to (I \subseteq P \lor J \subseteq P)$

Proof

Step	Hyp	Ref	Expression
1		idlmulssprm.1	$⊢ \underset{˙}{\times} = LSSum ({mulGrp}_{R})$
2		idlmulssprm.2	$⊢ φ \to R \in Ring$
3		idlmulssprm.3	$⊢ φ \to P \in PrmIdeal (R)$
4		idlmulssprm.4	$⊢ φ \to I \in LIdeal (R)$
5		idlmulssprm.5	$⊢ φ \to J \in LIdeal (R)$
6		idlmulssprm.6	$⊢ φ \to I \underset{˙}{\times} J \subseteq P$
7	4 5	jca	$⊢ φ \to (I \in LIdeal (R) \land J \in LIdeal (R))$
8	6	ad2antrr	$⊢ ((φ \land x \in I) \land y \in J) \to I \underset{˙}{\times} J \subseteq P$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
12		eqid	$⊢ LIdeal (R) = LIdeal (R)$
13	9 12	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq {Base}_{R}$
14	4 13	syl	$⊢ φ \to I \subseteq {Base}_{R}$
15	14	ad2antrr	$⊢ ((φ \land x \in I) \land y \in J) \to I \subseteq {Base}_{R}$
16	9 12	lidlss	$⊢ J \in LIdeal (R) \to J \subseteq {Base}_{R}$
17	5 16	syl	$⊢ φ \to J \subseteq {Base}_{R}$
18	17	ad2antrr	$⊢ ((φ \land x \in I) \land y \in J) \to J \subseteq {Base}_{R}$
19		simplr	$⊢ ((φ \land x \in I) \land y \in J) \to x \in I$
20		simpr	$⊢ ((φ \land x \in I) \land y \in J) \to y \in J$
21	9 10 11 1 15 18 19 20	elmgplsmd	$⊢ ((φ \land x \in I) \land y \in J) \to x \cdot_{R} y \in (I \underset{˙}{\times} J)$
22	8 21	sseldd	$⊢ ((φ \land x \in I) \land y \in J) \to x \cdot_{R} y \in P$
23	22	anasss	$⊢ (φ \land (x \in I \land y \in J)) \to x \cdot_{R} y \in P$
24	23	ralrimivva	$⊢ φ \to \forall x \in I \forall y \in J x \cdot_{R} y \in P$
25	9 10	prmidl	$⊢ (((R \in Ring \land P \in PrmIdeal (R)) \land (I \in LIdeal (R) \land J \in LIdeal (R))) \land \forall x \in I \forall y \in J x \cdot_{R} y \in P) \to (I \subseteq P \lor J \subseteq P)$
26	2 3 7 24 25	syl1111anc	$⊢ φ \to (I \subseteq P \lor J \subseteq P)$

Metamath Proof Explorer

Theorem idlmulssprm

Proof