Metamath Proof Explorer

Theorem fxpsubg

Description: The fixed points of a group action A on a group W is a subgroup. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses fxpsubm.b 
|- B = ( Base ` G )
fxpsubm.c 
|- C = ( Base ` W )
fxpsubm.f 
|- F = ( x e. C |-> ( p A x ) )
fxpsubm.a 
|- ( ph -> A e. ( G GrpAct C ) )
fxpsubg.1 
|- ( ( ph /\ p e. B ) -> F e. ( W GrpHom W ) )
Assertion fxpsubg 
|- ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) )

Proof

Step Hyp Ref Expression
1 fxpsubm.b 
 |-  B = ( Base ` G )
2 fxpsubm.c 
 |-  C = ( Base ` W )
3 fxpsubm.f 
 |-  F = ( x e. C |-> ( p A x ) )
4 fxpsubm.a 
 |-  ( ph -> A e. ( G GrpAct C ) )
5 fxpsubg.1 
 |-  ( ( ph /\ p e. B ) -> F e. ( W GrpHom W ) )
6 oveq1 
 |-  ( p = ( 0g ` G ) -> ( p A x ) = ( ( 0g ` G ) A x ) )
7 6 mpteq2dv 
 |-  ( p = ( 0g ` G ) -> ( x e. C |-> ( p A x ) ) = ( x e. C |-> ( ( 0g ` G ) A x ) ) )
8 3 7 eqtrid 
 |-  ( p = ( 0g ` G ) -> F = ( x e. C |-> ( ( 0g ` G ) A x ) ) )
9 8 eleq1d 
 |-  ( p = ( 0g ` G ) -> ( F e. ( W GrpHom W ) <-> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W GrpHom W ) ) )
10 5 ralrimiva 
 |-  ( ph -> A. p e. B F e. ( W GrpHom W ) )
11 gagrp 
 |-  ( A e. ( G GrpAct C ) -> G e. Grp )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 1 12 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
14 4 11 13 3syl 
 |-  ( ph -> ( 0g ` G ) e. B )
15 9 10 14 rspcdva 
 |-  ( ph -> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W GrpHom W ) )
16 ghmgrp1 
 |-  ( ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W GrpHom W ) -> W e. Grp )
17 15 16 syl 
 |-  ( ph -> W e. Grp )
18 ghmmhm 
 |-  ( F e. ( W GrpHom W ) -> F e. ( W MndHom W ) )
19 5 18 syl 
 |-  ( ( ph /\ p e. B ) -> F e. ( W MndHom W ) )
20 1 2 3 4 19 fxpsubm 
 |-  ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) )
21 5 adantlr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W GrpHom W ) )
22 gaset 
 |-  ( A e. ( G GrpAct C ) -> C e. _V )
23 4 22 syl 
 |-  ( ph -> C e. _V )
24 23 4 fxpss 
 |-  ( ph -> ( C FixPts A ) C_ C )
25 24 sselda 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C )
26 25 adantr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. C )
27 eqid 
 |-  ( invg ` W ) = ( invg ` W )
28 2 27 27 ghminv 
 |-  ( ( F e. ( W GrpHom W ) /\ z e. C ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` ( F ` z ) ) )
29 21 26 28 syl2anc 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` ( F ` z ) ) )
30 oveq2 
 |-  ( x = ( ( invg ` W ) ` z ) -> ( p A x ) = ( p A ( ( invg ` W ) ` z ) ) )
31 17 adantr 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> W e. Grp )
32 2 27 31 25 grpinvcld 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. C )
33 32 adantr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` z ) e. C )
34 ovexd 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) e. _V )
35 3 30 33 34 fvmptd3 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( p A ( ( invg ` W ) ` z ) ) )
36 oveq2 
 |-  ( x = z -> ( p A x ) = ( p A z ) )
37 ovexd 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V )
38 3 36 26 37 fvmptd3 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) )
39 4 adantr 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) )
40 39 adantr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) )
41 simplr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) )
42 simpr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> p e. B )
43 1 40 41 42 fxpgaeq 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z )
44 38 43 eqtrd 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z )
45 44 fveq2d 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` ( F ` z ) ) = ( ( invg ` W ) ` z ) )
46 29 35 45 3eqtr3d 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) )
47 46 ralrimiva 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> A. p e. B ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) )
48 1 39 32 isfxp 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( ( invg ` W ) ` z ) e. ( C FixPts A ) <-> A. p e. B ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) ) )
49 47 48 mpbird 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. ( C FixPts A ) )
50 49 ralrimiva 
 |-  ( ph -> A. z e. ( C FixPts A ) ( ( invg ` W ) ` z ) e. ( C FixPts A ) )
51 27 issubg3 
 |-  ( W e. Grp -> ( ( C FixPts A ) e. ( SubGrp ` W ) <-> ( ( C FixPts A ) e. ( SubMnd ` W ) /\ A. z e. ( C FixPts A ) ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) ) )
52 51 biimpar 
 |-  ( ( W e. Grp /\ ( ( C FixPts A ) e. ( SubMnd ` W ) /\ A. z e. ( C FixPts A ) ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) ) -> ( C FixPts A ) e. ( SubGrp ` W ) )
53 17 20 50 52 syl12anc 
 |-  ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) )