cntzsgrpcl

Description: Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025)

	Ref	Expression
Hypotheses	cntzsgrpcl.b	$⊢ B = {Base}_{M}$
	cntzsgrpcl.z	$⊢ Z = Cntz (M)$
	cntzsgrpcl.c	$⊢ C = Z (S)$
Assertion	cntzsgrpcl	$⊢ (M \in Smgrp \land S \subseteq B) \to \forall y \in C \forall z \in C y +_{M} z \in C$

Proof

Step	Hyp	Ref	Expression
1		cntzsgrpcl.b	$⊢ B = {Base}_{M}$
2		cntzsgrpcl.z	$⊢ Z = Cntz (M)$
3		cntzsgrpcl.c	$⊢ C = Z (S)$
4		simpll	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to M \in Smgrp$
5	1 2	cntzssv	$⊢ Z (S) \subseteq B$
6	3 5	eqsstri	$⊢ C \subseteq B$
7		simprl	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to y \in C$
8	6 7	sselid	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to y \in B$
9		simprr	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to z \in C$
10	6 9	sselid	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to z \in B$
11		eqid	$⊢ +_{M} = +_{M}$
12	1 11	sgrpcl	$⊢ (M \in Smgrp \land y \in B \land z \in B) \to y +_{M} z \in B$
13	4 8 10 12	syl3anc	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to y +_{M} z \in B$
14	4	adantr	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to M \in Smgrp$
15	8	adantr	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to y \in B$
16	10	adantr	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to z \in B$
17		simpr	$⊢ (M \in Smgrp \land S \subseteq B) \to S \subseteq B$
18	17	sselda	$⊢ ((M \in Smgrp \land S \subseteq B) \land x \in S) \to x \in B$
19	18	adantlr	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to x \in B$
20	1 11	sgrpass	$⊢ (M \in Smgrp \land (y \in B \land z \in B \land x \in B)) \to (y +_{M} z) +_{M} x = y +_{M} (z +_{M} x)$
21	14 15 16 19 20	syl13anc	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to (y +_{M} z) +_{M} x = y +_{M} (z +_{M} x)$
22	3	eleq2i	$⊢ z \in C \leftrightarrow z \in Z (S)$
23	11 2	cntzi	$⊢ (z \in Z (S) \land x \in S) \to z +_{M} x = x +_{M} z$
24	22 23	sylanb	$⊢ (z \in C \land x \in S) \to z +_{M} x = x +_{M} z$
25	9 24	sylan	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to z +_{M} x = x +_{M} z$
26	25	oveq2d	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to y +_{M} (z +_{M} x) = y +_{M} (x +_{M} z)$
27	1 11	sgrpass	$⊢ (M \in Smgrp \land (y \in B \land x \in B \land z \in B)) \to (y +_{M} x) +_{M} z = y +_{M} (x +_{M} z)$
28	14 15 19 16 27	syl13anc	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to (y +_{M} x) +_{M} z = y +_{M} (x +_{M} z)$
29	3	eleq2i	$⊢ y \in C \leftrightarrow y \in Z (S)$
30	11 2	cntzi	$⊢ (y \in Z (S) \land x \in S) \to y +_{M} x = x +_{M} y$
31	29 30	sylanb	$⊢ (y \in C \land x \in S) \to y +_{M} x = x +_{M} y$
32	7 31	sylan	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to y +_{M} x = x +_{M} y$
33	32	oveq1d	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to (y +_{M} x) +_{M} z = (x +_{M} y) +_{M} z$
34	26 28 33	3eqtr2d	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to y +_{M} (z +_{M} x) = (x +_{M} y) +_{M} z$
35	1 11	sgrpass	$⊢ (M \in Smgrp \land (x \in B \land y \in B \land z \in B)) \to (x +_{M} y) +_{M} z = x +_{M} (y +_{M} z)$
36	14 19 15 16 35	syl13anc	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to (x +_{M} y) +_{M} z = x +_{M} (y +_{M} z)$
37	21 34 36	3eqtrd	$⊢ (((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \land x \in S) \to (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)$
38	37	ralrimiva	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)$
39	3	eleq2i	$⊢ y +_{M} z \in C \leftrightarrow y +_{M} z \in Z (S)$
40	1 11 2	elcntz	$⊢ S \subseteq B \to (y +_{M} z \in Z (S) \leftrightarrow (y +_{M} z \in B \land \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)))$
41	39 40	bitrid	$⊢ S \subseteq B \to (y +_{M} z \in C \leftrightarrow (y +_{M} z \in B \land \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)))$
42	41	ad2antlr	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to (y +_{M} z \in C \leftrightarrow (y +_{M} z \in B \land \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)))$
43	13 38 42	mpbir2and	$⊢ ((M \in Smgrp \land S \subseteq B) \land (y \in C \land z \in C)) \to y +_{M} z \in C$
44	43	ralrimivva	$⊢ (M \in Smgrp \land S \subseteq B) \to \forall y \in C \forall z \in C y +_{M} z \in C$

Metamath Proof Explorer

Theorem cntzsgrpcl

Proof