Theorem cntzsgrpcl

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

	Ref	Expression
Hypotheses	cntzsgrpcl.b	$$⊢B={\mathrm{Base}}_M$$
	cntzsgrpcl.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
	cntzsgrpcl.c	$$⊢C=Z\left(S\right)$$
Assertion	cntzsgrpcl	Could not format assertion : No typesetting found for |- ( ( M e. Smgrp /\ S C_ B ) -> A. y e. C A. z e. C ( y ( +g ` M ) z ) e. C ) with typecode |-

Proof

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