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

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		simp1	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to R\in \mathrm{Rng}$$
5	1 2	lidlbas	$$⊢U\in L\to {\mathrm{Base}}_I=U$$
6		eleq1a	$$⊢U\in L\to \left({\mathrm{Base}}_I=U\to {\mathrm{Base}}_I\in L\right)$$
7	5 6	mpd	$$⊢U\in L\to {\mathrm{Base}}_I\in L$$
8	7	3ad2ant2	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{Base}}_I\in L$$
9	5	eqcomd	$$⊢U\in L\to U={\mathrm{Base}}_I$$
10	9	eleq2d	$$⊢U\in L\to \left(\underset{\dot{}}{0}\in U\leftrightarrow \underset{\dot{}}{0}\in {\mathrm{Base}}_I\right)$$
11	10	biimpa	$$⊢\left(U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_I$$
12	11	3adant1	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_I$$
13	4 8 12	3jca	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left(R\in \mathrm{Rng}\wedge {\mathrm{Base}}_I\in L\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_I\right)$$
14	1 2	lidlssbas	$$⊢U\in L\to {\mathrm{Base}}_I\subseteq {\mathrm{Base}}_R$$
15	14	sseld	$$⊢U\in L\to \left(a\in {\mathrm{Base}}_I\to a\in {\mathrm{Base}}_R\right)$$
16	15	3ad2ant2	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left(a\in {\mathrm{Base}}_I\to a\in {\mathrm{Base}}_R\right)$$
17	16	anim1d	$$⊢\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\right)\to \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_I\right)\right)$$
18	17	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\right)\right)\to \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_I\right)$$
19		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
20		eqid	$$⊢{\cdot }_R={\cdot }_R$$
21	3 19 20 1	rnglidlmcl	$$⊢\left(\left(R\in \mathrm{Rng}\wedge {\mathrm{Base}}_I\in L\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_I\right)\wedge \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_I\right)\right)\to a{\cdot }_{R}b\in {\mathrm{Base}}_I$$
22	13 18 21	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\right)\right)\to a{\cdot }_{R}b\in {\mathrm{Base}}_I$$
23	2 20	ressmulr	$$⊢U\in L\to {\cdot }_R={\cdot }_I$$
24	23	eqcomd	$$⊢U\in L\to {\cdot }_I={\cdot }_R$$
25	24	oveqd	$$⊢U\in L\to a{\cdot }_{I}b=a{\cdot }_{R}b$$
26	25	eleq1d	$$⊢U\in L\to \left(a{\cdot }_{I}b\in {\mathrm{Base}}_I\leftrightarrow a{\cdot }_{R}b\in {\mathrm{Base}}_I\right)$$
27	26	3ad2ant2	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left(a{\cdot }_{I}b\in {\mathrm{Base}}_I\leftrightarrow a{\cdot }_{R}b\in {\mathrm{Base}}_I\right)$$
28	27	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\right)\right)\to \left(a{\cdot }_{I}b\in {\mathrm{Base}}_I\leftrightarrow a{\cdot }_{R}b\in {\mathrm{Base}}_I\right)$$
29	22 28	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\right)\right)\to a{\cdot }_{I}b\in {\mathrm{Base}}_I$$
30	29	ralrimivva	$$⊢\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}a{\cdot }_{I}b\in {\mathrm{Base}}_I$$
31		fvex	$$⊢{\mathrm{mulGrp}}_I\in \mathrm{V}$$
32		eqid	$$⊢{\mathrm{mulGrp}}_I={\mathrm{mulGrp}}_I$$
33		eqid	$$⊢{\mathrm{Base}}_I={\mathrm{Base}}_I$$
34	32 33	mgpbas	$$⊢{\mathrm{Base}}_I={\mathrm{Base}}_{{\mathrm{mulGrp}}_I}$$
35		eqid	$$⊢{\cdot }_I={\cdot }_I$$
36	32 35	mgpplusg	$$⊢{\cdot }_I={+}_{{\mathrm{mulGrp}}_I}$$
37	34 36	ismgm	$$⊢{\mathrm{mulGrp}}_I\in \mathrm{V}\to \left({\mathrm{mulGrp}}_I\in \mathrm{Mgm}\leftrightarrow \forall a\in {\mathrm{Base}}_I\forall b\in {\mathrm{Base}}_{I}a{\cdot }_{I}b\in {\mathrm{Base}}_I\right)$$
38	31 37	mp1i	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to \left({\mathrm{mulGrp}}_I\in \mathrm{Mgm}\leftrightarrow \forall a\in {\mathrm{Base}}_I\forall b\in {\mathrm{Base}}_{I}a{\cdot }_{I}b\in {\mathrm{Base}}_I\right)$$
39	30 38	mpbird	$$⊢\left(R\in \mathrm{Rng}\wedge U\in L\wedge \underset{\dot{}}{0}\in U\right)\to {\mathrm{mulGrp}}_I\in \mathrm{Mgm}$$