Metamath Proof Explorer

Theorem fxpsubm

Description: Provided the group action A induces monoid automorphisms, the set of fixed points of A on a monoid W is a submonoid, which could be called the fixed submonoid under A . (Contributed by Thierry Arnoux, 18-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 fxpsubm.b 
 |-  B = ( Base ` G )
2 fxpsubg.c 
 |-  C = ( Base ` W )
3 fxpsubm.f 
 |-  F = ( x e. C |-> ( p A x ) )
4 fxpsubg.a 
 |-  ( ph -> A e. ( G GrpAct C ) )
5 fxpsubm.1 
 |-  ( ( ph /\ p e. B ) -> F e. ( W MndHom 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 MndHom W ) <-> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W MndHom W ) ) )
10 5 ralrimiva 
 |-  ( ph -> A. p e. B F e. ( W MndHom W ) )
11 gagrp 
 |-  ( A e. ( G GrpAct C ) -> G e. Grp )
12 4 11 syl 
 |-  ( ph -> G e. Grp )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 1 13 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
15 12 14 syl 
 |-  ( ph -> ( 0g ` G ) e. B )
16 9 10 15 rspcdva 
 |-  ( ph -> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W MndHom W ) )
17 mhmrcl1 
 |-  ( ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W MndHom W ) -> W e. Mnd )
18 16 17 syl 
 |-  ( ph -> W e. Mnd )
19 gaset 
 |-  ( A e. ( G GrpAct C ) -> C e. _V )
20 4 19 syl 
 |-  ( ph -> C e. _V )
21 20 4 fxpss 
 |-  ( ph -> ( C FixPts A ) C_ C )
22 oveq2 
 |-  ( x = ( 0g ` W ) -> ( p A x ) = ( p A ( 0g ` W ) ) )
23 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
24 2 23 mndidcl 
 |-  ( W e. Mnd -> ( 0g ` W ) e. C )
25 18 24 syl 
 |-  ( ph -> ( 0g ` W ) e. C )
26 25 adantr 
 |-  ( ( ph /\ p e. B ) -> ( 0g ` W ) e. C )
27 ovexd 
 |-  ( ( ph /\ p e. B ) -> ( p A ( 0g ` W ) ) e. _V )
28 3 22 26 27 fvmptd3 
 |-  ( ( ph /\ p e. B ) -> ( F ` ( 0g ` W ) ) = ( p A ( 0g ` W ) ) )
29 23 23 mhm0 
 |-  ( F e. ( W MndHom W ) -> ( F ` ( 0g ` W ) ) = ( 0g ` W ) )
30 5 29 syl 
 |-  ( ( ph /\ p e. B ) -> ( F ` ( 0g ` W ) ) = ( 0g ` W ) )
31 28 30 eqtr3d 
 |-  ( ( ph /\ p e. B ) -> ( p A ( 0g ` W ) ) = ( 0g ` W ) )
32 31 ralrimiva 
 |-  ( ph -> A. p e. B ( p A ( 0g ` W ) ) = ( 0g ` W ) )
33 1 4 25 isfxp 
 |-  ( ph -> ( ( 0g ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 0g ` W ) ) = ( 0g ` W ) ) )
34 32 33 mpbird 
 |-  ( ph -> ( 0g ` W ) e. ( C FixPts A ) )
35 5 ad4ant14 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W MndHom W ) )
36 21 ad2antrr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C )
37 simplr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. ( C FixPts A ) )
38 36 37 sseldd 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C )
39 38 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C )
40 21 adantr 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C )
41 40 sselda 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C )
42 41 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C )
43 eqid 
 |-  ( +g ` W ) = ( +g ` W )
44 2 43 43 mhmlin 
 |-  ( ( F e. ( W MndHom W ) /\ z e. C /\ y e. C ) -> ( F ` ( z ( +g ` W ) y ) ) = ( ( F ` z ) ( +g ` W ) ( F ` y ) ) )
45 35 39 42 44 syl3anc 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( +g ` W ) y ) ) = ( ( F ` z ) ( +g ` W ) ( F ` y ) ) )
46 oveq2 
 |-  ( x = ( z ( +g ` W ) y ) -> ( p A x ) = ( p A ( z ( +g ` W ) y ) ) )
47 18 ad2antrr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Mnd )
48 2 43 47 38 41 mndcld 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. C )
49 48 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( z ( +g ` W ) y ) e. C )
50 ovexd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) e. _V )
51 3 46 49 50 fvmptd3 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( +g ` W ) y ) ) = ( p A ( z ( +g ` W ) y ) ) )
52 oveq2 
 |-  ( x = z -> ( p A x ) = ( p A z ) )
53 ovexd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V )
54 3 52 39 53 fvmptd3 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) )
55 4 ad2antrr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) )
56 55 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) )
57 37 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) )
58 simpr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B )
59 1 56 57 58 fxpgaeq 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z )
60 54 59 eqtrd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z )
61 oveq2 
 |-  ( x = y -> ( p A x ) = ( p A y ) )
62 ovexd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V )
63 3 61 42 62 fvmptd3 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) )
64 simplr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) )
65 1 56 64 58 fxpgaeq 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y )
66 63 65 eqtrd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y )
67 60 66 oveq12d 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( +g ` W ) ( F ` y ) ) = ( z ( +g ` W ) y ) )
68 45 51 67 3eqtr3d 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) = ( z ( +g ` W ) y ) )
69 68 ralrimiva 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A. p e. B ( p A ( z ( +g ` W ) y ) ) = ( z ( +g ` W ) y ) )
70 1 55 48 isfxp 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( ( z ( +g ` W ) y ) e. ( C FixPts A ) <-> A. p e. B ( p A ( z ( +g ` W ) y ) ) = ( z ( +g ` W ) y ) ) )
71 69 70 mpbird 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. ( C FixPts A ) )
72 71 ralrimiva 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) )
73 72 ralrimiva 
 |-  ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) )
74 2 23 43 issubm 
 |-  ( W e. Mnd -> ( ( C FixPts A ) e. ( SubMnd ` W ) <-> ( ( C FixPts A ) C_ C /\ ( 0g ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) ) )
75 74 biimpar 
 |-  ( ( W e. Mnd /\ ( ( C FixPts A ) C_ C /\ ( 0g ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) ) -> ( C FixPts A ) e. ( SubMnd ` W ) )
76 18 21 34 73 75 syl13anc 
 |-  ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) )