cntrval2

Description: Express the center Z of a group M as the set of fixed points of the conjugation operation .(+) . (Contributed by Thierry Arnoux, 18-Nov-2025)

	Ref	Expression
Hypotheses	cntrval2.1	$⊢ B = {Base}_{M}$
	cntrval2.2	$⊢ \underset{˙}{+} = +_{M}$
	cntrval2.3	$⊢ \underset{˙}{-} = -_{M}$
	cntrval2.4	$⊢ \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
	cntrval2.5	$⊢ Z = Cntr (M)$
Assertion	cntrval2	Could not format assertion : No typesetting found for \|- ( M e. Grp -> Z = ( B FixPts .(+) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		cntrval2.1	$⊢ B = {Base}_{M}$
2		cntrval2.2	$⊢ \underset{˙}{+} = +_{M}$
3		cntrval2.3	$⊢ \underset{˙}{-} = -_{M}$
4		cntrval2.4	$⊢ \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
5		cntrval2.5	$⊢ Z = Cntr (M)$
6		simpll	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to M \in Grp$
7		simpr	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to p \in B$
8		simplr	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to z \in B$
9	1 2 6 7 8	grpcld	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to p \underset{˙}{+} z \in B$
10	1 3 6 9 7	grpsubcld	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (p \underset{˙}{+} z) \underset{˙}{-} p \in B$
11	1 2	grprcan	$⊢ (M \in Grp \land ((p \underset{˙}{+} z) \underset{˙}{-} p \in B \land z \in B \land p \in B)) \to (((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = z \underset{˙}{+} p \leftrightarrow (p \underset{˙}{+} z) \underset{˙}{-} p = z)$
12	6 10 8 7 11	syl13anc	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = z \underset{˙}{+} p \leftrightarrow (p \underset{˙}{+} z) \underset{˙}{-} p = z)$
13	1 2 3	grpnpcan	$⊢ (M \in Grp \land p \underset{˙}{+} z \in B \land p \in B) \to ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = p \underset{˙}{+} z$
14	6 9 7 13	syl3anc	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = p \underset{˙}{+} z$
15	14	eqeq2d	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (z \underset{˙}{+} p = ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p \leftrightarrow z \underset{˙}{+} p = p \underset{˙}{+} z)$
16		eqcom	$⊢ z \underset{˙}{+} p = ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p \leftrightarrow ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = z \underset{˙}{+} p$
17	15 16	bitr3di	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (z \underset{˙}{+} p = p \underset{˙}{+} z \leftrightarrow ((p \underset{˙}{+} z) \underset{˙}{-} p) \underset{˙}{+} p = z \underset{˙}{+} p)$
18	4	a1i	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
19		simprl	$⊢ (((M \in Grp \land z \in B) \land p \in B) \land (x = p \land y = z)) \to x = p$
20		simprr	$⊢ (((M \in Grp \land z \in B) \land p \in B) \land (x = p \land y = z)) \to y = z$
21	19 20	oveq12d	$⊢ (((M \in Grp \land z \in B) \land p \in B) \land (x = p \land y = z)) \to x \underset{˙}{+} y = p \underset{˙}{+} z$
22	21 19	oveq12d	$⊢ (((M \in Grp \land z \in B) \land p \in B) \land (x = p \land y = z)) \to (x \underset{˙}{+} y) \underset{˙}{-} x = (p \underset{˙}{+} z) \underset{˙}{-} p$
23		ovexd	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (p \underset{˙}{+} z) \underset{˙}{-} p \in V$
24	18 22 7 8 23	ovmpod	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to p \underset{˙}{\oplus} z = (p \underset{˙}{+} z) \underset{˙}{-} p$
25	24	eqeq1d	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (p \underset{˙}{\oplus} z = z \leftrightarrow (p \underset{˙}{+} z) \underset{˙}{-} p = z)$
26	12 17 25	3bitr4d	$⊢ ((M \in Grp \land z \in B) \land p \in B) \to (z \underset{˙}{+} p = p \underset{˙}{+} z \leftrightarrow p \underset{˙}{\oplus} z = z)$
27	26	ralbidva	$⊢ (M \in Grp \land z \in B) \to (\forall p \in B z \underset{˙}{+} p = p \underset{˙}{+} z \leftrightarrow \forall p \in B p \underset{˙}{\oplus} z = z)$
28	27	pm5.32da	$⊢ M \in Grp \to ((z \in B \land \forall p \in B z \underset{˙}{+} p = p \underset{˙}{+} z) \leftrightarrow (z \in B \land \forall p \in B p \underset{˙}{\oplus} z = z))$
29	1 2 5	elcntr	$⊢ z \in Z \leftrightarrow (z \in B \land \forall p \in B z \underset{˙}{+} p = p \underset{˙}{+} z)$
30		rabid	$⊢ z \in \{z \in B \| \forall p \in B p \underset{˙}{\oplus} z = z\} \leftrightarrow (z \in B \land \forall p \in B p \underset{˙}{\oplus} z = z)$
31	28 29 30	3bitr4g	$⊢ M \in Grp \to (z \in Z \leftrightarrow z \in \{z \in B \| \forall p \in B p \underset{˙}{\oplus} z = z\})$
32	1 2 3 4	conjga	$⊢ M \in Grp \to \underset{˙}{\oplus} \in (M GrpAct B)$
33	1 32	fxpgaval	Could not format ( M e. Grp -> ( B FixPts .(+) ) = { z e. B \| A. p e. B ( p .(+) z ) = z } ) : No typesetting found for \|- ( M e. Grp -> ( B FixPts .(+) ) = { z e. B \| A. p e. B ( p .(+) z ) = z } ) with typecode \|-
34	33	eleq2d	Could not format ( M e. Grp -> ( z e. ( B FixPts .(+) ) <-> z e. { z e. B \| A. p e. B ( p .(+) z ) = z } ) ) : No typesetting found for \|- ( M e. Grp -> ( z e. ( B FixPts .(+) ) <-> z e. { z e. B \| A. p e. B ( p .(+) z ) = z } ) ) with typecode \|-
35	31 34	bitr4d	Could not format ( M e. Grp -> ( z e. Z <-> z e. ( B FixPts .(+) ) ) ) : No typesetting found for \|- ( M e. Grp -> ( z e. Z <-> z e. ( B FixPts .(+) ) ) ) with typecode \|-
36	35	eqrdv	Could not format ( M e. Grp -> Z = ( B FixPts .(+) ) ) : No typesetting found for \|- ( M e. Grp -> Z = ( B FixPts .(+) ) ) with typecode \|-

Metamath Proof Explorer

Theorem cntrval2

Proof