Theorem ringlsmss1

Description: The product of an ideal I of a commutative ring R with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024)

	Ref	Expression
Hypotheses	ringlsmss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringlsmss.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	ringlsmss.3	⊢ × = ( LSSum ‘ 𝐺 )
	ringlsmss1.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	ringlsmss1.2	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
	ringlsmss1.3	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion	ringlsmss1	⊢ ( 𝜑 → ( 𝐼 × 𝐸 ) ⊆ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ringlsmss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringlsmss.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3		ringlsmss.3	⊢ × = ( LSSum ‘ 𝐺 )
4		ringlsmss1.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		ringlsmss1.2	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
6		ringlsmss1.3	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ) → 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) )
8	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑅 ∈ CRing )
9	5	sselda	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐵 )
10	9	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐵 )
11		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
12	1 11	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
13	6 12	syl	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
14	13	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐵 )
15	14	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑖 ∈ 𝐵 )
16		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17	1 16	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑒 ∈ 𝐵 ∧ 𝑖 ∈ 𝐵 ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) )
18	8 10 15 17	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) )
19		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20	4 19	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
21	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑅 ∈ Ring )
22	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
23		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑖 ∈ 𝐼 )
24	11 1 16	lidlmcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑖 ) ∈ 𝐼 )
25	21 22 10 23 24	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑖 ) ∈ 𝐼 )
26	18 25	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ∈ 𝐼 )
27	26	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ∈ 𝐼 )
28	27	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ) → ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ∈ 𝐼 )
29	7 28	eqeltrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ) → 𝑎 ∈ 𝐼 )
30	1 16 2 3 13 5	elmgplsm	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐼 × 𝐸 ) ↔ ∃ 𝑖 ∈ 𝐼 ∃ 𝑒 ∈ 𝐸 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) ) )
31	30	biimpa	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) → ∃ 𝑖 ∈ 𝐼 ∃ 𝑒 ∈ 𝐸 𝑎 = ( 𝑖 ( .r ‘ 𝑅 ) 𝑒 ) )
32	29 31	r19.29vva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐼 × 𝐸 ) ) → 𝑎 ∈ 𝐼 )
33	32	ex	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐼 × 𝐸 ) → 𝑎 ∈ 𝐼 ) )
34	33	ssrdv	⊢ ( 𝜑 → ( 𝐼 × 𝐸 ) ⊆ 𝐼 )