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	$$⊢L=\mathrm{LIdeal}\left(R\right)$$
	rnglidlabl.i	$$⊢I=R{\upharpoonright }_{𝑠}U$$
	rnglidlabl.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rnglidlmsgrp	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{mulGrp}}_I\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		rnglidlabl.l	$$⊢L=\mathrm{LIdeal}\left(R\right)$$
2		rnglidlabl.i	$$⊢I=R{\upharpoonright }_{𝑠}U$$
3		rnglidlabl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 2 3	rnglidlmmgm	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{mulGrp}}_I\in \mathrm{Mgm}$$
5		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
6	5	rngmgp	$$⊢R\in \mathrm{Rng}\to {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}$$
7	6	3ad2ant1	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}$$
8	1 2	lidlssbas	$$⊢U\in L\to {\mathrm{Base}}_I\subseteq {\mathrm{Base}}_R$$
9	8	sseld	$$⊢U\in L\to \left(a\in {\mathrm{Base}}_I\to a\in {\mathrm{Base}}_R\right)$$
10	8	sseld	$$⊢U\in L\to \left(b\in {\mathrm{Base}}_I\to b\in {\mathrm{Base}}_R\right)$$
11	8	sseld	$$⊢U\in L\to \left(c\in {\mathrm{Base}}_I\to c\in {\mathrm{Base}}_R\right)$$
12	9 10 11	3anim123d	$$⊢U\in L\to \left(\left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\to \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\wedge c\in {\mathrm{Base}}_R\right)\right)$$
13	12	3ad2ant2	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left(\left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\to \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\wedge c\in {\mathrm{Base}}_R\right)\right)$$
14	13	imp	$$⊢\left(\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\wedge \left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\right)\to \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\wedge c\in {\mathrm{Base}}_R\right)$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16	5 15	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
17		eqid	$$⊢{\cdot }_R={\cdot }_R$$
18	5 17	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
19	16 18	sgrpass	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Smgrp}\wedge \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\wedge c\in {\mathrm{Base}}_R\right)\right)\to \left(a{\cdot }_{R}b\right){\cdot }_{R}c=a{\cdot }_R\left(b{\cdot }_{R}c\right)$$
20	7 14 19	syl2an2r	$$⊢\left(\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\wedge \left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\right)\to \left(a{\cdot }_{R}b\right){\cdot }_{R}c=a{\cdot }_R\left(b{\cdot }_{R}c\right)$$
21	2 17	ressmulr	$$⊢U\in L\to {\cdot }_R={\cdot }_I$$
22	21	eqcomd	$$⊢U\in L\to {\cdot }_I={\cdot }_R$$
23	22	oveqd	$$⊢U\in L\to a{\cdot }_{I}b=a{\cdot }_{R}b$$
24		eqidd	$$⊢U\in L\to c=c$$
25	22 23 24	oveq123d	$$⊢U\in L\to \left(a{\cdot }_{I}b\right){\cdot }_{I}c=\left(a{\cdot }_{R}b\right){\cdot }_{R}c$$
26		eqidd	$$⊢U\in L\to a=a$$
27	22	oveqd	$$⊢U\in L\to b{\cdot }_{I}c=b{\cdot }_{R}c$$
28	22 26 27	oveq123d	$$⊢U\in L\to a{\cdot }_I\left(b{\cdot }_{I}c\right)=a{\cdot }_R\left(b{\cdot }_{R}c\right)$$
29	25 28	eqeq12d	$$⊢U\in L\to \left(\left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)\leftrightarrow \left(a{\cdot }_{R}b\right){\cdot }_{R}c=a{\cdot }_R\left(b{\cdot }_{R}c\right)\right)$$
30	29	3ad2ant2	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left(\left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)\leftrightarrow \left(a{\cdot }_{R}b\right){\cdot }_{R}c=a{\cdot }_R\left(b{\cdot }_{R}c\right)\right)$$
31	30	adantr	$$⊢\left(\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\wedge \left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\right)\to \left(\left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)\leftrightarrow \left(a{\cdot }_{R}b\right){\cdot }_{R}c=a{\cdot }_R\left(b{\cdot }_{R}c\right)\right)$$
32	20 31	mpbird	$$⊢\left(\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\wedge \left(a\in {\mathrm{Base}}_I\wedge b\in {\mathrm{Base}}_I\wedge c\in {\mathrm{Base}}_I\right)\right)\to \left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)$$
33	32	ralrimivvva	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \forall a\in {\mathrm{Base}}_I\forall b\in {\mathrm{Base}}_I\forall c\in {\mathrm{Base}}_I\left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)$$
34		eqid	$$⊢{\mathrm{mulGrp}}_I={\mathrm{mulGrp}}_I$$
35		eqid	$$⊢{\mathrm{Base}}_I={\mathrm{Base}}_I$$
36	34 35	mgpbas	$$⊢{\mathrm{Base}}_I={\mathrm{Base}}_{{\mathrm{mulGrp}}_I}$$
37		eqid	$$⊢{\cdot }_I={\cdot }_I$$
38	34 37	mgpplusg	$$⊢{\cdot }_I={+}_{{\mathrm{mulGrp}}_I}$$
39	36 38	issgrp	$$⊢{\mathrm{mulGrp}}_I\in \mathrm{Smgrp}\leftrightarrow \left({\mathrm{mulGrp}}_I\in \mathrm{Mgm}\wedge \forall a\in {\mathrm{Base}}_I\forall b\in {\mathrm{Base}}_I\forall c\in {\mathrm{Base}}_I\left(a{\cdot }_{I}b\right){\cdot }_{I}c=a{\cdot }_I\left(b{\cdot }_{I}c\right)\right)$$
40	4 33 39	sylanbrc	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{mulGrp}}_I\in \mathrm{Smgrp}$$