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

Metamath Proof Explorer

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 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )