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	⊢ × = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
	idlmulssprm.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	idlmulssprm.3	⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
	idlmulssprm.4	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	idlmulssprm.5	⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
	idlmulssprm.6	⊢ ( 𝜑 → ( 𝐼 × 𝐽 ) ⊆ 𝑃 )
Assertion	idlmulssprm	⊢ ( 𝜑 → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		idlmulssprm.1	⊢ × = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
2		idlmulssprm.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		idlmulssprm.3	⊢ ( 𝜑 → 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) )
4		idlmulssprm.4	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5		idlmulssprm.5	⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
6		idlmulssprm.6	⊢ ( 𝜑 → ( 𝐼 × 𝐽 ) ⊆ 𝑃 )
7	4 5	jca	⊢ ( 𝜑 → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) )
8	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐼 × 𝐽 ) ⊆ 𝑃 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
11		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
12		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
13	9 12	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
14	4 13	syl	⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
15	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
16	9 12	lidlss	⊢ ( 𝐽 ∈ ( LIdeal ‘ 𝑅 ) → 𝐽 ⊆ ( Base ‘ 𝑅 ) )
17	5 16	syl	⊢ ( 𝜑 → 𝐽 ⊆ ( Base ‘ 𝑅 ) )
18	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝐽 ⊆ ( Base ‘ 𝑅 ) )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑥 ∈ 𝐼 )
20		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ 𝐽 )
21	9 10 11 1 15 18 19 20	elmgplsmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ( ._r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐼 × 𝐽 ) )
22	8 21	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ( ._r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 )
23	22	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ( ._r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 )
24	23	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ( ._r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 )
25	9 10	prmidl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ( ._r ‘ 𝑅 ) 𝑦 ) ∈ 𝑃 ) → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) )
26	2 3 7 24 25	syl1111anc	⊢ ( 𝜑 → ( 𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃 ) )

Metamath Proof Explorer

Theorem idlmulssprm

Proof