lidlmmgm

Description: The multiplicative group of a (left) ideal of a ring is a magma. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypotheses	lidlabl.l	$⊢ L = LIdeal (R)$
	lidlabl.i	$⊢ I = R ↾_{𝑠} U$
Assertion	lidlmmgm	$⊢ (R \in Ring \land U \in L) \to {mulGrp}_{I} \in Mgm$

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3	1 2	lidlbas	$⊢ U \in L \to {Base}_{I} = U$
4		eleq1a	$⊢ U \in L \to ({Base}_{I} = U \to {Base}_{I} \in L)$
5	3 4	mpd	$⊢ U \in L \to {Base}_{I} \in L$
6	5	anim2i	$⊢ (R \in Ring \land U \in L) \to (R \in Ring \land {Base}_{I} \in L)$
7	6	adantr	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to (R \in Ring \land {Base}_{I} \in L)$
8	1 2	lidlssbas	$⊢ U \in L \to {Base}_{I} \subseteq {Base}_{R}$
9	8	adantl	$⊢ (R \in Ring \land U \in L) \to {Base}_{I} \subseteq {Base}_{R}$
10	9	sseld	$⊢ (R \in Ring \land U \in L) \to (a \in {Base}_{I} \to a \in {Base}_{R})$
11	10	com12	$⊢ a \in {Base}_{I} \to ((R \in Ring \land U \in L) \to a \in {Base}_{R})$
12	11	adantr	$⊢ (a \in {Base}_{I} \land b \in {Base}_{I}) \to ((R \in Ring \land U \in L) \to a \in {Base}_{R})$
13	12	impcom	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to a \in {Base}_{R}$
14		simprr	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to b \in {Base}_{I}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	1 15 16	lidlmcl	$⊢ ((R \in Ring \land {Base}_{I} \in L) \land (a \in {Base}_{R} \land b \in {Base}_{I})) \to a \cdot_{R} b \in {Base}_{I}$
18	7 13 14 17	syl12anc	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to a \cdot_{R} b \in {Base}_{I}$
19	18	ralrimivva	$⊢ (R \in Ring \land U \in L) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{R} b \in {Base}_{I}$
20		fvex	$⊢ {mulGrp}_{I} \in V$
21		eqid	$⊢ {mulGrp}_{I} = {mulGrp}_{I}$
22		eqid	$⊢ {Base}_{I} = {Base}_{I}$
23	21 22	mgpbas	$⊢ {Base}_{I} = {Base}_{{mulGrp}_{I}}$
24		eqid	$⊢ \cdot_{I} = \cdot_{I}$
25	21 24	mgpplusg	$⊢ \cdot_{I} = +_{{mulGrp}_{I}}$
26	23 25	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})$
27	20 26	mp1i	$⊢ (R \in Ring \land U \in L) \to ({mulGrp}_{I} \in Mgm \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{I} b \in {Base}_{I})$
28	2 16	ressmulr	$⊢ U \in L \to \cdot_{R} = \cdot_{I}$
29	28	eqcomd	$⊢ U \in L \to \cdot_{I} = \cdot_{R}$
30	29	adantl	$⊢ (R \in Ring \land U \in L) \to \cdot_{I} = \cdot_{R}$
31	30	oveqdr	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I})) \to a \cdot_{I} b = a \cdot_{R} b$
32	31	eleq1d	$⊢ ((R \in Ring \land U \in L) \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})$
33	32	2ralbidva	$⊢ (R \in Ring \land U \in L) \to (\forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{I} b \in {Base}_{I} \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{R} b \in {Base}_{I})$
34	27 33	bitrd	$⊢ (R \in Ring \land U \in L) \to ({mulGrp}_{I} \in Mgm \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} a \cdot_{R} b \in {Base}_{I})$
35	19 34	mpbird	$⊢ (R \in Ring \land U \in L) \to {mulGrp}_{I} \in Mgm$

Metamath Proof Explorer

Theorem lidlmmgm

Proof