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	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
	idlmulssprm.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	idlmulssprm.3	No typesetting found for |- ( ph -> P e. ( PrmIdeal ` R ) ) with typecode |-
	idlmulssprm.4	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
	idlmulssprm.5	$$⊢\phi \to J\in \mathrm{LIdeal}\left(R\right)$$
	idlmulssprm.6	$$⊢\phi \to I\underset{\dot{}}{\times }J\subseteq P$$
Assertion	idlmulssprm	$$⊢\phi \to \left(I\subseteq P\vee J\subseteq P\right)$$

Proof

Step	Hyp	Ref	Expression
1		idlmulssprm.1	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
2		idlmulssprm.2	$$⊢\phi \to R\in \mathrm{Ring}$$
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	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
5		idlmulssprm.5	$$⊢\phi \to J\in \mathrm{LIdeal}\left(R\right)$$
6		idlmulssprm.6	$$⊢\phi \to I\underset{\dot{}}{\times }J\subseteq P$$
7	4 5	jca	$$⊢\phi \to \left(I\in \mathrm{LIdeal}\left(R\right)\wedge J\in \mathrm{LIdeal}\left(R\right)\right)$$
8	6	ad2antrr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to I\underset{\dot{}}{\times }J\subseteq P$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
12		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
13	9 12	lidlss	$$⊢I\in \mathrm{LIdeal}\left(R\right)\to I\subseteq {\mathrm{Base}}_R$$
14	4 13	syl	$$⊢\phi \to I\subseteq {\mathrm{Base}}_R$$
15	14	ad2antrr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to I\subseteq {\mathrm{Base}}_R$$
16	9 12	lidlss	$$⊢J\in \mathrm{LIdeal}\left(R\right)\to J\subseteq {\mathrm{Base}}_R$$
17	5 16	syl	$$⊢\phi \to J\subseteq {\mathrm{Base}}_R$$
18	17	ad2antrr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to J\subseteq {\mathrm{Base}}_R$$
19		simplr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to x\in I$$
20		simpr	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to y\in J$$
21	9 10 11 1 15 18 19 20	elringlsmd	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to x{\cdot }_{R}y\in \left(I\underset{\dot{}}{\times }J\right)$$
22	8 21	sseldd	$$⊢\left(\left(\phi \wedge x\in I\right)\wedge y\in J\right)\to x{\cdot }_{R}y\in P$$
23	22	anasss	$$⊢\left(\phi \wedge \left(x\in I\wedge y\in J\right)\right)\to x{\cdot }_{R}y\in P$$
24	23	ralrimivva	$$⊢\phi \to \forall x\in I\forall y\in Jx{\cdot }_{R}y\in P$$
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	$$⊢\phi \to \left(I\subseteq P\vee J\subseteq P\right)$$