Metamath Proof Explorer

Theorem rnglidlrng

Description: A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020) Generalization for non-unital rings. The assumption U e. ( SubGrpR ) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025)

Ref Expression
Hypotheses rnglidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
rnglidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion rnglidlrng ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Rng )

Proof

Step Hyp Ref Expression
1 rnglidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 rnglidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
4 3 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Abel )
5 simp3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑅 ) )
6 2 subgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Abel )
7 4 5 6 syl2anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Abel )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 8 subg0cl ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑈 )
10 1 2 8 rnglidlmsgrp ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )
11 9 10 syl3an3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )
12 simpl1 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → 𝑅 ∈ Rng )
13 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
14 13 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
15 13 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ∈ ( Base ‘ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
16 13 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑐 ∈ ( Base ‘ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
17 14 15 16 3anim123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
18 17 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
19 18 imp ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
20 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
22 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23 20 21 22 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
24 12 19 23 syl2anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
25 20 21 22 rngdir ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
26 12 19 25 syl2anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
27 2 22 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
28 27 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
29 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑎 = 𝑎 )
30 2 21 ressplusg ⊢ ( 𝑈 ∈ 𝐿 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐼 ) )
31 30 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( +g ‘ 𝐼 ) = ( +g ‘ 𝑅 ) )
32 31 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) )
33 28 29 32 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) )
34 28 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
35 28 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) )
36 31 34 35 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
37 33 36 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
38 31 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) )
39 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑐 = 𝑐 )
40 28 38 39 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) )
41 28 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) )
42 31 35 41 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
43 40 42 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
44 37 43 anbi12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
45 44 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
46 45 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
47 24 26 46 mpbir2and ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) )
48 47 ralrimivvva ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) )
49 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
50 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
51 eqid ⊢ ( +g ‘ 𝐼 ) = ( +g ‘ 𝐼 )
52 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
53 49 50 51 52 isrng ⊢ ( 𝐼 ∈ Rng ↔ ( 𝐼 ∈ Abel ∧ ( mulGrp ‘ 𝐼 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ) )
54 7 11 48 53 syl3anbrc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ∈ Rng )