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 \in C ⟼ p A x)$
	fxpsubm.a	$⊢ φ \to A \in (G GrpAct C)$
	fxpsubg.1	$⊢ (φ \land p \in B) \to F \in (W GrpHom W)$
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 = {Base}_{G}$
2		fxpsubm.c	$⊢ C = {Base}_{W}$
3		fxpsubm.f	$⊢ F = (x \in C ⟼ p A x)$
4		fxpsubm.a	$⊢ φ \to A \in (G GrpAct C)$
5		fxpsubg.1	$⊢ (φ \land p \in B) \to F \in (W GrpHom W)$
6		oveq1	$⊢ p = 0_{G} \to p A x = 0_{G} A x$
7	6	mpteq2dv	$⊢ p = 0_{G} \to (x \in C ⟼ p A x) = (x \in C ⟼ 0_{G} A x)$
8	3 7	eqtrid	$⊢ p = 0_{G} \to F = (x \in C ⟼ 0_{G} A x)$
9	8	eleq1d	$⊢ p = 0_{G} \to (F \in (W GrpHom W) \leftrightarrow (x \in C ⟼ 0_{G} A x) \in (W GrpHom W))$
10	5	ralrimiva	$⊢ φ \to \forall p \in B F \in (W GrpHom W)$
11		gagrp	$⊢ A \in (G GrpAct C) \to G \in Grp$
12		eqid	$⊢ 0_{G} = 0_{G}$
13	1 12	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
14	4 11 13	3syl	$⊢ φ \to 0_{G} \in B$
15	9 10 14	rspcdva	$⊢ φ \to (x \in C ⟼ 0_{G} A x) \in (W GrpHom W)$
16		ghmgrp1	$⊢ (x \in C ⟼ 0_{G} A x) \in (W GrpHom W) \to W \in Grp$
17	15 16	syl	$⊢ φ \to W \in Grp$
18		ghmmhm	$⊢ F \in (W GrpHom W) \to F \in (W MndHom W)$
19	5 18	syl	$⊢ (φ \land p \in B) \to F \in (W MndHom W)$
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 (G GrpAct C) \to C \in V$
23	4 22	syl	$⊢ φ \to C \in 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} (W) = {inv}_{g} (W)$
28	2 27 27	ghminv	$⊢ (F \in (W GrpHom W) \land z \in C) \to F ({inv}_{g} (W) (z)) = {inv}_{g} (W) (F (z))$
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} (W) (z) \to p A x = p A {inv}_{g} (W) (z)$
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 p A x = p A z$
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 \|-

Metamath Proof Explorer

Theorem fxpsubg

Proof