Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` M )
cntrval2.3 
|- .- = ( -g ` M )
cntrval2.4 
|- .(+) = ( x e. B , y e. B |-> ( ( x .+ y ) .- x ) )
cntrval2.5 
|- Z = ( Cntr ` M )
Assertion cntrval2 
|- ( M e. Grp -> Z = ( B FixPts .(+) ) )

Proof

Step Hyp Ref Expression
1 cntrval2.1 
 |-  B = ( Base ` M )
2 cntrval2.2 
 |-  .+ = ( +g ` M )
3 cntrval2.3 
 |-  .- = ( -g ` M )
4 cntrval2.4 
 |-  .(+) = ( x e. B , y e. B |-> ( ( x .+ y ) .- x ) )
5 cntrval2.5 
 |-  Z = ( Cntr ` M )
6 simpll 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> M e. Grp )
7 simpr 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> p e. B )
8 simplr 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> z e. B )
9 1 2 6 7 8 grpcld 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( p .+ z ) e. B )
10 1 3 6 9 7 grpsubcld 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( p .+ z ) .- p ) e. B )
11 1 2 grprcan 
 |-  ( ( M e. Grp /\ ( ( ( p .+ z ) .- p ) e. B /\ z e. B /\ p e. B ) ) -> ( ( ( ( p .+ z ) .- p ) .+ p ) = ( z .+ p ) <-> ( ( p .+ z ) .- p ) = z ) )
12 6 10 8 7 11 syl13anc 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( ( ( p .+ z ) .- p ) .+ p ) = ( z .+ p ) <-> ( ( p .+ z ) .- p ) = z ) )
13 1 2 3 grpnpcan 
 |-  ( ( M e. Grp /\ ( p .+ z ) e. B /\ p e. B ) -> ( ( ( p .+ z ) .- p ) .+ p ) = ( p .+ z ) )
14 6 9 7 13 syl3anc 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( ( p .+ z ) .- p ) .+ p ) = ( p .+ z ) )
15 14 eqeq2d 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( z .+ p ) = ( ( ( p .+ z ) .- p ) .+ p ) <-> ( z .+ p ) = ( p .+ z ) ) )
16 eqcom 
 |-  ( ( z .+ p ) = ( ( ( p .+ z ) .- p ) .+ p ) <-> ( ( ( p .+ z ) .- p ) .+ p ) = ( z .+ p ) )
17 15 16 bitr3di 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( z .+ p ) = ( p .+ z ) <-> ( ( ( p .+ z ) .- p ) .+ p ) = ( z .+ p ) ) )
18 4 a1i 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> .(+) = ( x e. B , y e. B |-> ( ( x .+ y ) .- x ) ) )
19 simprl 
 |-  ( ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) /\ ( x = p /\ y = z ) ) -> x = p )
20 simprr 
 |-  ( ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) /\ ( x = p /\ y = z ) ) -> y = z )
21 19 20 oveq12d 
 |-  ( ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) /\ ( x = p /\ y = z ) ) -> ( x .+ y ) = ( p .+ z ) )
22 21 19 oveq12d 
 |-  ( ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) /\ ( x = p /\ y = z ) ) -> ( ( x .+ y ) .- x ) = ( ( p .+ z ) .- p ) )
23 ovexd 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( p .+ z ) .- p ) e. _V )
24 18 22 7 8 23 ovmpod 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( p .(+) z ) = ( ( p .+ z ) .- p ) )
25 24 eqeq1d 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( p .(+) z ) = z <-> ( ( p .+ z ) .- p ) = z ) )
26 12 17 25 3bitr4d 
 |-  ( ( ( M e. Grp /\ z e. B ) /\ p e. B ) -> ( ( z .+ p ) = ( p .+ z ) <-> ( p .(+) z ) = z ) )
27 26 ralbidva 
 |-  ( ( M e. Grp /\ z e. B ) -> ( A. p e. B ( z .+ p ) = ( p .+ z ) <-> A. p e. B ( p .(+) z ) = z ) )
28 27 pm5.32da 
 |-  ( M e. Grp -> ( ( z e. B /\ A. p e. B ( z .+ p ) = ( p .+ z ) ) <-> ( z e. B /\ A. p e. B ( p .(+) z ) = z ) ) )
29 1 2 5 elcntr 
 |-  ( z e. Z <-> ( z e. B /\ A. p e. B ( z .+ p ) = ( p .+ z ) ) )
30 rabid 
 |-  ( z e. { z e. B | A. p e. B ( p .(+) z ) = z } <-> ( z e. B /\ A. p e. B ( p .(+) z ) = z ) )
31 28 29 30 3bitr4g 
 |-  ( M e. Grp -> ( z e. Z <-> z e. { z e. B | A. p e. B ( p .(+) z ) = z } ) )
32 1 2 3 4 conjga 
 |-  ( M e. Grp -> .(+) e. ( M GrpAct B ) )
33 1 32 fxpgaval 
 |-  ( M e. Grp -> ( B FixPts .(+) ) = { z e. B | A. p e. B ( p .(+) z ) = z } )
34 33 eleq2d 
 |-  ( M e. Grp -> ( z e. ( B FixPts .(+) ) <-> z e. { z e. B | A. p e. B ( p .(+) z ) = z } ) )
35 31 34 bitr4d 
 |-  ( M e. Grp -> ( z e. Z <-> z e. ( B FixPts .(+) ) ) )
36 35 eqrdv 
 |-  ( M e. Grp -> Z = ( B FixPts .(+) ) )