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 = LIdeal (R)$
	rnglidlabl.i	$⊢ I = R ↾_{𝑠} U$
	rnglidlabl.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	rnglidlmmgm	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to {mulGrp}_{I} \in Mgm$

Proof

Step	Hyp	Ref	Expression
1		rnglidlabl.l	$⊢ L = LIdeal (R)$
2		rnglidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		rnglidlabl.z	$⊢ \underset{˙}{0} = 0_{R}$
4		simp1	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to R \in Rng$
5	1 2	lidlbas	$⊢ U \in L \to {Base}_{I} = U$
6		eleq1a	$⊢ U \in L \to ({Base}_{I} = U \to {Base}_{I} \in L)$
7	5 6	mpd	$⊢ U \in L \to {Base}_{I} \in L$
8	7	3ad2ant2	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to {Base}_{I} \in L$
9	5	eqcomd	$⊢ U \in L \to U = {Base}_{I}$
10	9	eleq2d	$⊢ U \in L \to (\underset{˙}{0} \in U \leftrightarrow \underset{˙}{0} \in {Base}_{I})$
11	10	biimpa	$⊢ (U \in L \land \underset{˙}{0} \in U) \to \underset{˙}{0} \in {Base}_{I}$
12	11	3adant1	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to \underset{˙}{0} \in {Base}_{I}$
13	4 8 12	3jca	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to (R \in Rng \land {Base}_{I} \in L \land \underset{˙}{0} \in {Base}_{I})$
14	1 2	lidlssbas	$⊢ U \in L \to {Base}_{I} \subseteq {Base}_{R}$
15	14	sseld	$⊢ U \in L \to (a \in {Base}_{I} \to a \in {Base}_{R})$
16	15	3ad2ant2	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to (a \in {Base}_{I} \to a \in {Base}_{R})$
17	16	anim1d	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to ((a \in {Base}_{I} \land b \in {Base}_{I}) \to (a \in {Base}_{R} \land b \in {Base}_{I}))$
18	17	imp	$⊢ ((R \in Rng \land U \in L \land \underset{˙}{0} \in U) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to (a \in {Base}_{R} \land b \in {Base}_{I})$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20		eqid	$⊢ \cdot_{R} = \cdot_{R}$
21	3 19 20 1	rnglidlmcl	$⊢ ((R \in Rng \land {Base}_{I} \in L \land \underset{˙}{0} \in {Base}_{I}) \land (a \in {Base}_{R} \land b \in {Base}_{I})) \to a \cdot_{R} b \in {Base}_{I}$
22	13 18 21	syl2an2r	$⊢ ((R \in Rng \land U \in L \land \underset{˙}{0} \in U) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to a \cdot_{R} b \in {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 (a \cdot_{I} b \in {Base}_{I} \leftrightarrow a \cdot_{R} b \in {Base}_{I})$
27	26	3ad2ant2	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to (a \cdot_{I} b \in {Base}_{I} \leftrightarrow a \cdot_{R} b \in {Base}_{I})$
28	27	adantr	$⊢ ((R \in Rng \land U \in L \land \underset{˙}{0} \in U) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to (a \cdot_{I} b \in {Base}_{I} \leftrightarrow a \cdot_{R} b \in {Base}_{I})$
29	22 28	mpbird	$⊢ ((R \in Rng \land U \in L \land \underset{˙}{0} \in U) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to a \cdot_{I} b \in {Base}_{I}$
30	29	ralrimivva	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{I} b \in {Base}_{I}$
31		fvex	$⊢ {mulGrp}_{I} \in V$
32		eqid	$⊢ {mulGrp}_{I} = {mulGrp}_{I}$
33		eqid	$⊢ {Base}_{I} = {Base}_{I}$
34	32 33	mgpbas	$⊢ {Base}_{I} = {Base}_{{mulGrp}_{I}}$
35		eqid	$⊢ \cdot_{I} = \cdot_{I}$
36	32 35	mgpplusg	$⊢ \cdot_{I} = +_{{mulGrp}_{I}}$
37	34 36	ismgm	$⊢ {mulGrp}_{I} \in V \to ({mulGrp}_{I} \in Mgm \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{I} b \in {Base}_{I})$
38	31 37	mp1i	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to ({mulGrp}_{I} \in Mgm \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{I} b \in {Base}_{I})$
39	30 38	mpbird	$⊢ (R \in Rng \land U \in L \land \underset{˙}{0} \in U) \to {mulGrp}_{I} \in Mgm$

Metamath Proof Explorer

Theorem rnglidlmmgm

Proof