lidlmsgrp

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

	Ref	Expression
Hypotheses	lidlabl.l	$⊢ L = LIdeal (R)$
	lidlabl.i	$⊢ I = R ↾_{𝑠} U$
Assertion	lidlmsgrp	Could not format assertion : No typesetting found for \|- ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3	1 2	lidlmmgm	$⊢ (R \in Ring \land U \in L) \to {mulGrp}_{I} \in Mgm$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
6	5	ad2antrr	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to {mulGrp}_{R} \in Mnd$
7	1 2	lidlssbas	$⊢ U \in L \to {Base}_{I} \subseteq {Base}_{R}$
8	7	sseld	$⊢ U \in L \to (a \in {Base}_{I} \to a \in {Base}_{R})$
9	7	sseld	$⊢ U \in L \to (b \in {Base}_{I} \to b \in {Base}_{R})$
10	7	sseld	$⊢ U \in L \to (c \in {Base}_{I} \to c \in {Base}_{R})$
11	8 9 10	3anim123d	$⊢ U \in L \to ((a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I}) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R}))$
12	11	adantl	$⊢ (R \in Ring \land U \in L) \to ((a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I}) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R}))$
13	12	imp	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R})$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	4 14	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	4 16	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
18	15 17	mndass	$⊢ ({mulGrp}_{R} \in Mnd \land (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R})) \to (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c)$
19	6 13 18	syl2anc	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c)$
20	19	ralrimivvva	$⊢ (R \in Ring \land U \in L) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c)$
21	2 16	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 (a \cdot_{I} b) \cdot_{I} c = (a \cdot_{R} b) \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} (b \cdot_{I} c) = a \cdot_{R} (b \cdot_{R} c)$
29	25 28	eqeq12d	$⊢ U \in L \to ((a \cdot_{I} b) \cdot_{I} c = a \cdot_{I} (b \cdot_{I} c) \leftrightarrow (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c))$
30	29	adantl	$⊢ (R \in Ring \land U \in L) \to ((a \cdot_{I} b) \cdot_{I} c = a \cdot_{I} (b \cdot_{I} c) \leftrightarrow (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c))$
31	30	ralbidv	$⊢ (R \in Ring \land U \in L) \to (\forall c \in {Base}_{I} (a \cdot_{I} b) \cdot_{I} c = a \cdot_{I} (b \cdot_{I} c) \leftrightarrow \forall c \in {Base}_{I} (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c))$
32	31	2ralbidv	$⊢ (R \in Ring \land U \in L) \to (\forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (a \cdot_{I} b) \cdot_{I} c = a \cdot_{I} (b \cdot_{I} c) \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (a \cdot_{R} b) \cdot_{R} c = a \cdot_{R} (b \cdot_{R} c))$
33	20 32	mpbird	$⊢ (R \in Ring \land U \in L) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (a \cdot_{I} b) \cdot_{I} c = a \cdot_{I} (b \cdot_{I} c)$
34		eqid	$⊢ {mulGrp}_{I} = {mulGrp}_{I}$
35		eqid	$⊢ {Base}_{I} = {Base}_{I}$
36	34 35	mgpbas	$⊢ {Base}_{I} = {Base}_{{mulGrp}_{I}}$
37		eqid	$⊢ \cdot_{I} = \cdot_{I}$
38	34 37	mgpplusg	$⊢ \cdot_{I} = +_{{mulGrp}_{I}}$
39	36 38	issgrp	Could not format ( ( mulGrp ` I ) e. Smgrp <-> ( ( mulGrp ` I ) e. Mgm /\ A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) ) ) : No typesetting found for \|- ( ( mulGrp ` I ) e. Smgrp <-> ( ( mulGrp ` I ) e. Mgm /\ A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) b ) ( .r ` I ) c ) = ( a ( .r ` I ) ( b ( .r ` I ) c ) ) ) ) with typecode \|-
40	3 33 39	sylanbrc	Could not format ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp ) : No typesetting found for \|- ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp ) with typecode \|-

Metamath Proof Explorer

Theorem lidlmsgrp

Proof