rrgsubm

Description: The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025)

	Ref	Expression
Hypotheses	rrgsubm.1	$⊢ E = RLReg (R)$
	rrgsubm.2	$⊢ M = {mulGrp}_{R}$
	rrgsubm.3	$⊢ φ \to R \in Ring$
Assertion	rrgsubm	$⊢ φ \to E \in SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		rrgsubm.1	$⊢ E = RLReg (R)$
2		rrgsubm.2	$⊢ M = {mulGrp}_{R}$
3		rrgsubm.3	$⊢ φ \to R \in Ring$
4	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
5	3 4	syl	$⊢ φ \to M \in Mnd$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	1 6	rrgss	$⊢ E \subseteq {Base}_{R}$
8	7	a1i	$⊢ φ \to E \subseteq {Base}_{R}$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	9 1 3	1rrg	$⊢ φ \to 1_{R} \in E$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12	3	ad2antrr	$⊢ ((φ \land x \in E) \land y \in E) \to R \in Ring$
13		simplr	$⊢ ((φ \land x \in E) \land y \in E) \to x \in E$
14	7 13	sselid	$⊢ ((φ \land x \in E) \land y \in E) \to x \in {Base}_{R}$
15		simpr	$⊢ ((φ \land x \in E) \land y \in E) \to y \in E$
16	7 15	sselid	$⊢ ((φ \land x \in E) \land y \in E) \to y \in {Base}_{R}$
17	6 11 12 14 16	ringcld	$⊢ ((φ \land x \in E) \land y \in E) \to x \cdot_{R} y \in {Base}_{R}$
18	15	ad2antrr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to y \in E$
19		simplr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to z \in {Base}_{R}$
20	13	ad2antrr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to x \in E$
21	12	ad2antrr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to R \in Ring$
22	16	ad2antrr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to y \in {Base}_{R}$
23	6 11 21 22 19	ringcld	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to y \cdot_{R} z \in {Base}_{R}$
24	14	ad2antrr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to x \in {Base}_{R}$
25	6 11 21 24 22 19	ringassd	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z)$
26		simpr	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to (x \cdot_{R} y) \cdot_{R} z = 0_{R}$
27	25 26	eqtr3d	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to x \cdot_{R} (y \cdot_{R} z) = 0_{R}$
28		eqid	$⊢ 0_{R} = 0_{R}$
29	1 6 11 28	rrgeq0i	$⊢ (x \in E \land y \cdot_{R} z \in {Base}_{R}) \to (x \cdot_{R} (y \cdot_{R} z) = 0_{R} \to y \cdot_{R} z = 0_{R})$
30	29	imp	$⊢ ((x \in E \land y \cdot_{R} z \in {Base}_{R}) \land x \cdot_{R} (y \cdot_{R} z) = 0_{R}) \to y \cdot_{R} z = 0_{R}$
31	20 23 27 30	syl21anc	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to y \cdot_{R} z = 0_{R}$
32	1 6 11 28	rrgeq0i	$⊢ (y \in E \land z \in {Base}_{R}) \to (y \cdot_{R} z = 0_{R} \to z = 0_{R})$
33	32	imp	$⊢ ((y \in E \land z \in {Base}_{R}) \land y \cdot_{R} z = 0_{R}) \to z = 0_{R}$
34	18 19 31 33	syl21anc	$⊢ ((((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \land (x \cdot_{R} y) \cdot_{R} z = 0_{R}) \to z = 0_{R}$
35	34	ex	$⊢ (((φ \land x \in E) \land y \in E) \land z \in {Base}_{R}) \to ((x \cdot_{R} y) \cdot_{R} z = 0_{R} \to z = 0_{R})$
36	35	ralrimiva	$⊢ ((φ \land x \in E) \land y \in E) \to \forall z \in {Base}_{R} ((x \cdot_{R} y) \cdot_{R} z = 0_{R} \to z = 0_{R})$
37	1 6 11 28	isrrg	$⊢ x \cdot_{R} y \in E \leftrightarrow (x \cdot_{R} y \in {Base}_{R} \land \forall z \in {Base}_{R} ((x \cdot_{R} y) \cdot_{R} z = 0_{R} \to z = 0_{R}))$
38	17 36 37	sylanbrc	$⊢ ((φ \land x \in E) \land y \in E) \to x \cdot_{R} y \in E$
39	38	anasss	$⊢ (φ \land (x \in E \land y \in E)) \to x \cdot_{R} y \in E$
40	39	ralrimivva	$⊢ φ \to \forall x \in E \forall y \in E x \cdot_{R} y \in E$
41	2 6	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
42	2 9	ringidval	$⊢ 1_{R} = 0_{M}$
43	2 11	mgpplusg	$⊢ \cdot_{R} = +_{M}$
44	41 42 43	issubm	$⊢ M \in Mnd \to (E \in SubMnd (M) \leftrightarrow (E \subseteq {Base}_{R} \land 1_{R} \in E \land \forall x \in E \forall y \in E x \cdot_{R} y \in E))$
45	44	biimpar	$⊢ (M \in Mnd \land (E \subseteq {Base}_{R} \land 1_{R} \in E \land \forall x \in E \forall y \in E x \cdot_{R} y \in E)) \to E \in SubMnd (M)$
46	5 8 10 40 45	syl13anc	$⊢ φ \to E \in SubMnd (M)$

Metamath Proof Explorer

Theorem rrgsubm

Proof