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={\mathrm{Base}}_G$$
	fxpsubg.c	$$⊢C={\mathrm{Base}}_W$$
	fxpsubm.f	$$⊢F=\left(x\in C⟼pAx\right)$$
	fxpsubg.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
	fxpsubm.1	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
Assertion	fxpsubm	Could not format assertion : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fxpsubm.b	$$⊢B={\mathrm{Base}}_G$$
2		fxpsubg.c	$$⊢C={\mathrm{Base}}_W$$
3		fxpsubm.f	$$⊢F=\left(x\in C⟼pAx\right)$$
4		fxpsubg.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
5		fxpsubm.1	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
6		oveq1	$$⊢p=0_G\to pAx=0_{G}Ax$$
7	6	mpteq2dv	$$⊢p=0_G\to \left(x\in C⟼pAx\right)=\left(x\in C⟼0_{G}Ax\right)$$
8	3 7	eqtrid	$$⊢p=0_G\to F=\left(x\in C⟼0_{G}Ax\right)$$
9	8	eleq1d	$$⊢p=0_G\to \left(F\in \left(W\mathrm{MndHom}W\right)\leftrightarrow \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{MndHom}W\right)\right)$$
10	5	ralrimiva	$$⊢\phi \to \forall p\in BF\in \left(W\mathrm{MndHom}W\right)$$
11		gagrp	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to G\in \mathrm{Grp}$$
12	4 11	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
13		eqid	$$⊢0_G=0_G$$
14	1 13	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
15	12 14	syl	$$⊢\phi \to 0_G\in B$$
16	9 10 15	rspcdva	$$⊢\phi \to \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{MndHom}W\right)$$
17		mhmrcl1	$$⊢\left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{MndHom}W\right)\to W\in \mathrm{Mnd}$$
18	16 17	syl	$$⊢\phi \to W\in \mathrm{Mnd}$$
19		gaset	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to C\in \mathrm{V}$$
20	4 19	syl	$$⊢\phi \to C\in \mathrm{V}$$
21	20 4	fxpss	Could not format ( ph -> ( C FixPts A ) C_ C ) : No typesetting found for |- ( ph -> ( C FixPts A ) C_ C ) with typecode |-
22		oveq2	$$⊢x=0_W\to pAx=pA{0}_W$$
23		eqid	$$⊢0_W=0_W$$
24	2 23	mndidcl	$$⊢W\in \mathrm{Mnd}\to 0_W\in C$$
25	18 24	syl	$$⊢\phi \to 0_W\in C$$
26	25	adantr	$$⊢\left(\phi \wedge p\in B\right)\to 0_W\in C$$
27		ovexd	$$⊢\left(\phi \wedge p\in B\right)\to pA{0}_W\in \mathrm{V}$$
28	3 22 26 27	fvmptd3	$$⊢\left(\phi \wedge p\in B\right)\to F\left(0_W\right)=pA{0}_W$$
29	23 23	mhm0	$$⊢F\in \left(W\mathrm{MndHom}W\right)\to F\left(0_W\right)=0_W$$
30	5 29	syl	$$⊢\left(\phi \wedge p\in B\right)\to F\left(0_W\right)=0_W$$
31	28 30	eqtr3d	$$⊢\left(\phi \wedge p\in B\right)\to pA{0}_W=0_W$$
32	31	ralrimiva	$$⊢\phi \to \forall p\in BpA{0}_W=0_W$$
33	1 4 25	isfxp	Could not format ( ph -> ( ( 0g ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 0g ` W ) ) = ( 0g ` W ) ) ) : No typesetting found for |- ( ph -> ( ( 0g ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 0g ` W ) ) = ( 0g ` W ) ) ) with typecode |-
34	32 33	mpbird	Could not format ( ph -> ( 0g ` W ) e. ( C FixPts A ) ) : No typesetting found for |- ( ph -> ( 0g ` W ) e. ( C FixPts A ) ) with typecode |-
35	5	ad4ant14	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W MndHom W ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W MndHom W ) ) with typecode |-
36	21	ad2antrr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) with typecode |-
37		simplr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. ( C FixPts A ) ) with typecode |-
38	36 37	sseldd	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C ) with typecode |-
39	38	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) with typecode |-
40	21	adantr	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) with typecode |-
41	40	sselda	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C ) with typecode |-
42	41	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C ) with typecode |-
43		eqid	$$⊢{+}_W={+}_W$$
44	2 43 43	mhmlin	$$⊢\left(F\in \left(W\mathrm{MndHom}W\right)\wedge z\in C\wedge y\in C\right)\to F\left(z{+}_{W}y\right)=F\left(z\right){+}_{W}F\left(y\right)$$
45	35 39 42 44	syl3anc	Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
46		oveq2	$$⊢x=z{+}_{W}y\to pAx=pA\left(z{+}_{W}y\right)$$
47	18	ad2antrr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Mnd ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Mnd ) with typecode |-
48	2 43 47 38 41	mndcld	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. C ) with typecode |-
49	48	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( z ( +g ` W ) y ) e. C ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( z ( +g ` W ) y ) e. C ) with typecode |-
50		ovexd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) e. _V ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) e. _V ) with typecode |-
51	3 46 49 50	fvmptd3	Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
52		oveq2	$$⊢x=z\to pAx=pAz$$
53		ovexd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) with typecode |-
54	3 52 39 53	fvmptd3	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) with typecode |-
55	4	ad2antrr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) with typecode |-
56	55	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) with typecode |-
57	37	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) with typecode |-
58		simpr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) with typecode |-
59	1 56 57 58	fxpgaeq	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) with typecode |-
60	54 59	eqtrd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) with typecode |-
61		oveq2	$$⊢x=y\to pAx=pAy$$
62		ovexd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V ) with typecode |-
63	3 61 42 62	fvmptd3	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) ) with typecode |-
64		simplr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) ) with typecode |-
65	1 56 64 58	fxpgaeq	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y ) with typecode |-
66	63 65	eqtrd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y ) with typecode |-
67	60 66	oveq12d	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( +g ` W ) ( F ` y ) ) = ( z ( +g ` W ) y ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( +g ` W ) ( F ` y ) ) = ( z ( +g ` W ) y ) ) with typecode |-
68	45 51 67	3eqtr3d	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) = ( z ( +g ` W ) y ) ) : No typesetting found for |- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( +g ` W ) y ) ) = ( z ( +g ` W ) y ) ) with typecode |-
69	68	ralrimiva	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
70	1 55 48	isfxp	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
71	69 70	mpbird	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( +g ` W ) y ) e. ( C FixPts A ) ) with typecode |-
72	71	ralrimiva	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) with typecode |-
73	72	ralrimiva	Could not format ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for |- ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( +g ` W ) y ) e. ( C FixPts A ) ) with typecode |-
74	2 23 43	issubm	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
75	74	biimpar	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
76	18 21 34 73 75	syl13anc	Could not format ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) ) : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) ) with typecode |-