Theorem dflidl2lem

Description: Lemma for dflidl2 : a sufficient condition for a set to be a left ideal. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	dflidl2.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	dflidl2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dflidl2.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	dflidl2lem	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		dflidl2.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		dflidl2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		dflidl2.t	⊢ · = ( .r ‘ 𝑅 )
4	2	subgss	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
5	4	adantr	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ⊆ 𝐵 )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7	6	subg0cl	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
8	7	ne0d	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ≠ ∅ )
9	8	adantr	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ≠ ∅ )
10		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11	10	subgcl	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
12	11	ad4ant134	⊢ ( ( ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
13	12	ralrimiva	⊢ ( ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
14	13	ex	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝐼 → ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
15	14	ralimdvva	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
16	15	imp	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
17	1 2 10 3	islidl	⊢ ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
18	5 9 16 17	syl3anbrc	⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ∈ 𝑈 )