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

Proof

Step	Hyp	Ref	Expression
1		fxpsubm.b	$$⊢B={\mathrm{Base}}_G$$
2		fxpsubm.c	$$⊢C={\mathrm{Base}}_W$$
3		fxpsubm.f	$$⊢F=\left(x\in C⟼pAx\right)$$
4		fxpsubm.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
5		fxpsubg.1	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{GrpHom}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{GrpHom}W\right)\leftrightarrow \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{GrpHom}W\right)\right)$$
10	5	ralrimiva	$$⊢\phi \to \forall p\in BF\in \left(W\mathrm{GrpHom}W\right)$$
11		gagrp	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to G\in \mathrm{Grp}$$
12		eqid	$$⊢0_G=0_G$$
13	1 12	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
14	4 11 13	3syl	$$⊢\phi \to 0_G\in B$$
15	9 10 14	rspcdva	$$⊢\phi \to \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{GrpHom}W\right)$$
16		ghmgrp1	$$⊢\left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{GrpHom}W\right)\to W\in \mathrm{Grp}$$
17	15 16	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
18		ghmmhm	$$⊢F\in \left(W\mathrm{GrpHom}W\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
19	5 18	syl	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
20	1 2 3 4 19	fxpsubm	Could not format ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) ) : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubMnd ` W ) ) with typecode |-
21	5	adantlr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W GrpHom W ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W GrpHom W ) ) with typecode |-
22		gaset	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to C\in \mathrm{V}$$
23	4 22	syl	$$⊢\phi \to C\in \mathrm{V}$$
24	23 4	fxpss	Could not format ( ph -> ( C FixPts A ) C_ C ) : No typesetting found for |- ( ph -> ( C FixPts A ) C_ C ) with typecode |-
25	24	sselda	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C ) with typecode |-
26	25	adantr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) with typecode |-
27		eqid	$$⊢{inv}_g\left(W\right)={inv}_g\left(W\right)$$
28	2 27 27	ghminv	$$⊢\left(F\in \left(W\mathrm{GrpHom}W\right)\wedge z\in C\right)\to F\left({inv}_g\left(W\right)\left(z\right)\right)={inv}_g\left(W\right)\left(F\left(z\right)\right)$$
29	21 26 28	syl2anc	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` ( F ` z ) ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` ( F ` z ) ) ) with typecode |-
30		oveq2	$$⊢x={inv}_g\left(W\right)\left(z\right)\to pAx=pA{inv}_g\left(W\right)\left(z\right)$$
31	17	adantr	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> W e. Grp ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> W e. Grp ) with typecode |-
32	2 27 31 25	grpinvcld	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. C ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. C ) with typecode |-
33	32	adantr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` z ) e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` z ) e. C ) with typecode |-
34		ovexd	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) e. _V ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) e. _V ) with typecode |-
35	3 30 33 34	fvmptd3	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( p A ( ( invg ` W ) ` z ) ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( ( invg ` W ) ` z ) ) = ( p A ( ( invg ` W ) ` z ) ) ) with typecode |-
36		oveq2	$$⊢x=z\to pAx=pAz$$
37		ovexd	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) with typecode |-
38	3 36 26 37	fvmptd3	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) with typecode |-
39	4	adantr	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) with typecode |-
40	39	adantr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) with typecode |-
41		simplr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) with typecode |-
42		simpr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) with typecode |-
43	1 40 41 42	fxpgaeq	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) with typecode |-
44	38 43	eqtrd	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) with typecode |-
45	44	fveq2d	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` ( F ` z ) ) = ( ( invg ` W ) ` z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( ( invg ` W ) ` ( F ` z ) ) = ( ( invg ` W ) ` z ) ) with typecode |-
46	29 35 45	3eqtr3d	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) ) with typecode |-
47	46	ralrimiva	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> A. p e. B ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> A. p e. B ( p A ( ( invg ` W ) ` z ) ) = ( ( invg ` W ) ` z ) ) with typecode |-
48	1 39 32	isfxp	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
49	47 48	mpbird	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) : No typesetting found for |- ( ( ph /\ z e. ( C FixPts A ) ) -> ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) with typecode |-
50	49	ralrimiva	Could not format ( ph -> A. z e. ( C FixPts A ) ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) : No typesetting found for |- ( ph -> A. z e. ( C FixPts A ) ( ( invg ` W ) ` z ) e. ( C FixPts A ) ) with typecode |-
51	27	issubg3	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
52	51	biimpar	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
53	17 20 50 52	syl12anc	Could not format ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) ) : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) ) with typecode |-