This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dflidl2rng

Description: Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 dflidl2rng.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 dflidl2rng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 dflidl2rng.t ⊢ · = ( .r ‘ 𝑅 )
4 simpll ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) → 𝑅 ∈ Rng )
5 simpr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 6 subg0cl ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
8 7 ad2antlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
9 4 5 8 3jca ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) )
10 6 2 3 1 rnglidlmcl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ 𝑈 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐼 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐼 )
11 9 10 sylan ⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐼 )
12 11 ralrimivva ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 )
13 2 subgss ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
14 13 ad2antlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ⊆ 𝐵 )
15 7 ne0d ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ≠ ∅ )
16 15 ad2antlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ≠ ∅ )
17 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
18 17 subgcl ⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
19 18 ad5ant245 ⊢ ( ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
20 19 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) ∧ ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
21 20 ex ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝐼 → ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
22 21 ralimdvva ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
23 22 imp ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 )
24 1 2 17 3 islidl ⊢ ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ⊆ 𝐵 ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐼 ) )
25 14 16 23 24 syl3anbrc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) → 𝐼 ∈ 𝑈 )
26 12 25 impbida ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ 𝑈 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )