Metamath Proof Explorer

Theorem rnglidlmmgm

Description: The multiplicative group of a (left) ideal of a non-unital ring is a magma. (Contributed by AV, 17-Feb-2020) Generalization for non-unital rings. The assumption .0. e. U 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 𝑈 )
rnglidlabl.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rnglidlmmgm ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Mgm )

Proof

Step Hyp Ref Expression
1 rnglidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 rnglidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 rnglidlabl.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 simp1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → 𝑅 ∈ Rng )
5 1 2 lidlbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )
6 eleq1a ⊢ ( 𝑈 ∈ 𝐿 → ( ( Base ‘ 𝐼 ) = 𝑈 → ( Base ‘ 𝐼 ) ∈ 𝐿 ) )
7 5 6 mpd ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ∈ 𝐿 )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( Base ‘ 𝐼 ) ∈ 𝐿 )
9 5 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 = ( Base ‘ 𝐼 ) )
10 9 eleq2d ⊢ ( 𝑈 ∈ 𝐿 → ( 0 ∈ 𝑈 ↔ 0 ∈ ( Base ‘ 𝐼 ) ) )
11 10 biimpa ⊢ ( ( 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → 0 ∈ ( Base ‘ 𝐼 ) )
12 11 3adant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → 0 ∈ ( Base ‘ 𝐼 ) )
13 4 8 12 3jca ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( 𝑅 ∈ Rng ∧ ( Base ‘ 𝐼 ) ∈ 𝐿 ∧ 0 ∈ ( Base ‘ 𝐼 ) ) )
14 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
15 14 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
16 15 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
17 16 anim1d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) )
18 17 imp ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) )
19 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 3 19 20 1 rnglidlmcl ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( Base ‘ 𝐼 ) ∈ 𝐿 ∧ 0 ∈ ( Base ‘ 𝐼 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
22 13 18 21 syl2an2r ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
23 2 20 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
24 23 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
25 24 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
26 25 eleq1d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
27 26 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
29 22 28 mpbird ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
30 29 ralrimivva ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) )
31 fvex ⊢ ( mulGrp ‘ 𝐼 ) ∈ V
32 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
33 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
34 32 33 mgpbas ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ ( mulGrp ‘ 𝐼 ) )
35 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
36 32 35 mgpplusg ⊢ ( .r ‘ 𝐼 ) = ( +g ‘ ( mulGrp ‘ 𝐼 ) )
37 34 36 ismgm ⊢ ( ( mulGrp ‘ 𝐼 ) ∈ V → ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
38 31 37 mp1i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ∈ ( Base ‘ 𝐼 ) ) )
39 30 38 mpbird ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Mgm )