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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	fxpsubm.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
	fxpsubm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
	fxpsubm.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
	fxpsubg.1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
Assertion	fxpsubg	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		fxpsubm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		fxpsubm.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
3		fxpsubm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
4		fxpsubm.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
5		fxpsubg.1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
6		oveq1	⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑝 𝐴 𝑥 ) = ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) )
7	6	mpteq2dv	⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
8	3 7	eqtrid	⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
9	8	eleq1d	⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) ↔ ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 GrpHom 𝑊 ) ) )
10	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
11		gagrp	⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐺 ∈ Grp )
12		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13	1 12	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
14	4 11 13	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
15	9 10 14	rspcdva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 GrpHom 𝑊 ) )
16		ghmgrp1	⊢ ( ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 GrpHom 𝑊 ) → 𝑊 ∈ Grp )
17	15 16	syl	⊢ ( 𝜑 → 𝑊 ∈ Grp )
18		ghmmhm	⊢ ( 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )
19	5 18	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )
20	1 2 3 4 19	fxpsubm	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) )
21	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
22		gaset	⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐶 ∈ V )
23	4 22	syl	⊢ ( 𝜑 → 𝐶 ∈ V )
24	23 4	fxpss	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
25	24	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑧 ∈ 𝐶 )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
27		eqid	⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
28	2 27 27	ghminv	⊢ ( ( 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝐹 ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) )
29	21 26 28	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) )
30		oveq2	⊢ ( 𝑥 = ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) )
31	17	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑊 ∈ Grp )
32	2 27 31 25	grpinvcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ 𝐶 )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ 𝐶 )
34		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) ∈ V )
35	3 30 33 34	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) )
36		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑧 ) )
37		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) ∈ V )
38	3 36 26 37	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑝 𝐴 𝑧 ) )
39	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
40	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
41		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) )
42		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
43	1 40 41 42	fxpgaeq	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) = 𝑧 )
44	38 43	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
45	44	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) )
46	29 35 45	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) )
47	46	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) )
48	1 39 32	isfxp	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ) )
49	47 48	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) )
50	49	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) )
51	27	issubg3	⊢ ( 𝑊 ∈ Grp → ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) ↔ ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) )
52	51	biimpar	⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ( ( invg ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) → ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) )
53	17 20 50 52	syl12anc	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) )