Theorem rnglidlmcl

Description: A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven as in lidlmcl . (Contributed by AV, 18-Feb-2025)

	Ref	Expression
Hypotheses	rnglidlmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	rnglidlmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rnglidlmcl.t	⊢ · = ( .r ‘ 𝑅 )
	rnglidlmcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion	rnglidlmcl	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		rnglidlmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		rnglidlmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		rnglidlmcl.t	⊢ · = ( .r ‘ 𝑅 )
4		rnglidlmcl.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
5		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6	4 2 5 3	islidl	⊢ ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
7		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑎 ) = ( 𝑋 · 𝑎 ) )
8	7	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) )
9	8	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
10	9	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ↔ ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
11		oveq2	⊢ ( 𝑎 = 𝑌 → ( 𝑋 · 𝑎 ) = ( 𝑋 · 𝑌 ) )
12	11	oveq1d	⊢ ( 𝑎 = 𝑌 → ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) )
13	12	eleq1d	⊢ ( 𝑎 = 𝑌 → ( ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
14	13	ralbidv	⊢ ( 𝑎 = 𝑌 → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ↔ ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
15	10 14	rspc2v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
16	15	adantl	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) )
17		oveq2	⊢ ( 𝑏 = 0 → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) )
18	17	eleq1d	⊢ ( 𝑏 = 0 → ( ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 ) )
19	18	rspcv	⊢ ( 0 ∈ 𝐼 → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 ) )
20	19	adantl	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 ) )
21		rnggrp	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
22	21	3ad2ant1	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) → 𝑅 ∈ Grp )
23	22	adantr	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → 𝑅 ∈ Grp )
24	23	adantr	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑅 ∈ Grp )
25		simpll1	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑅 ∈ Rng )
26		simprl	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ 𝐵 )
27		ssel	⊢ ( 𝐼 ⊆ 𝐵 → ( 𝑌 ∈ 𝐼 → 𝑌 ∈ 𝐵 ) )
28	27	3ad2ant2	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑌 ∈ 𝐼 → 𝑌 ∈ 𝐵 ) )
29	28	adantr	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( 𝑌 ∈ 𝐼 → 𝑌 ∈ 𝐵 ) )
30	29	adantld	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐵 ) )
31	30	imp	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ 𝐵 )
32	2 3	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
33	25 26 31 32	syl3anc	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
34	2 5 1 24 33	grpridd	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) = ( 𝑋 · 𝑌 ) )
35	34	eleq1d	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 ↔ ( 𝑋 · 𝑌 ) ∈ 𝐼 ) )
36	35	biimpd	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) )
37	36	ex	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 0 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) )
38	20 37	syl5d	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) )
39	38	imp	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ∀ 𝑏 ∈ 𝐼 ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) )
40	16 39	syld	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) )
41	40	ex	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) )
42	41	com23	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) ∧ 0 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) )
43	42	ex	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 0 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) ) )
44	43	com23	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 0 ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) ) )
45	44	3exp	⊢ ( 𝑅 ∈ Rng → ( 𝐼 ⊆ 𝐵 → ( 𝐼 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 → ( 0 ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) ) ) ) )
46	45	3impd	⊢ ( 𝑅 ∈ Rng → ( ( 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) → ( 0 ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) ) )
47	6 46	biimtrid	⊢ ( 𝑅 ∈ Rng → ( 𝐼 ∈ 𝑈 → ( 0 ∈ 𝐼 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 ) ) ) )
48	47	3imp1	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ 0 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )