Theorem ringlsmss2

Description: The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024)

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

Proof

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