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

Metamath Proof Explorer

Theorem rnglidlmsgrp

Description: The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (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 rnglidlmsgrp ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 rnglidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 rnglidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 rnglidlabl.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 1 2 3 rnglidlmmgm ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Mgm )
5 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
6 5 rngmgp ⊢ ( 𝑅 ∈ Rng → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
7 6 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
8 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
9 8 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
10 8 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ∈ ( Base ‘ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
11 8 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑐 ∈ ( Base ‘ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
12 9 10 11 3anim123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
13 12 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
14 13 imp ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 5 15 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 5 17 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
19 16 18 sgrpass ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
20 7 14 19 syl2an2r ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
21 2 17 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
22 21 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
23 22 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
24 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑐 = 𝑐 )
25 22 23 24 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) )
26 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑎 = 𝑎 )
27 22 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) )
28 22 26 27 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
29 25 28 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
30 29 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
31 30 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
32 20 31 mpbird ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) )
33 32 ralrimivvva ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) )
34 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
35 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
36 34 35 mgpbas ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ ( mulGrp ‘ 𝐼 ) )
37 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
38 34 37 mgpplusg ⊢ ( .r ‘ 𝐼 ) = ( +g ‘ ( mulGrp ‘ 𝐼 ) )
39 36 38 issgrp ⊢ ( ( mulGrp ‘ 𝐼 ) ∈ Smgrp ↔ ( ( mulGrp ‘ 𝐼 ) ∈ Mgm ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) )
40 4 33 39 sylanbrc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑈 ∈ 𝐿 ∧ 0 ∈ 𝑈 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )