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}$
	fxpsubm.c	$⊢ C = {Base}_{W}$
	fxpsubm.f	$⊢ F = (x \in C ⟼ p A x)$
	fxpsubm.a	$⊢ φ \to A \in (G GrpAct C)$
	fxpsubm.1	$⊢ (φ \land p \in B) \to F \in (W MndHom W)$
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 = {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		fxpsubm.1	$⊢ (φ \land p \in B) \to F \in (W MndHom 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 MndHom W) \leftrightarrow (x \in C ⟼ 0_{G} A x) \in (W MndHom W))$
10	5	ralrimiva	$⊢ φ \to \forall p \in B F \in (W MndHom W)$
11		gagrp	$⊢ A \in (G GrpAct C) \to G \in Grp$
12	4 11	syl	$⊢ φ \to G \in Grp$
13		eqid	$⊢ 0_{G} = 0_{G}$
14	1 13	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
15	12 14	syl	$⊢ φ \to 0_{G} \in B$
16	9 10 15	rspcdva	$⊢ φ \to (x \in C ⟼ 0_{G} A x) \in (W MndHom W)$
17		mhmrcl1	$⊢ (x \in C ⟼ 0_{G} A x) \in (W MndHom W) \to W \in Mnd$
18	16 17	syl	$⊢ φ \to W \in Mnd$
19		gaset	$⊢ A \in (G GrpAct C) \to C \in V$
20	4 19	syl	$⊢ φ \to C \in 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 p A x = p A 0_{W}$
23		eqid	$⊢ 0_{W} = 0_{W}$
24	2 23	mndidcl	$⊢ W \in Mnd \to 0_{W} \in C$
25	18 24	syl	$⊢ φ \to 0_{W} \in C$
26	25	adantr	$⊢ (φ \land p \in B) \to 0_{W} \in C$
27		ovexd	$⊢ (φ \land p \in B) \to p A 0_{W} \in V$
28	3 22 26 27	fvmptd3	$⊢ (φ \land p \in B) \to F (0_{W}) = p A 0_{W}$
29	23 23	mhm0	$⊢ F \in (W MndHom W) \to F (0_{W}) = 0_{W}$
30	5 29	syl	$⊢ (φ \land p \in B) \to F (0_{W}) = 0_{W}$
31	28 30	eqtr3d	$⊢ (φ \land p \in B) \to p A 0_{W} = 0_{W}$
32	31	ralrimiva	$⊢ φ \to \forall p \in B p A 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	$⊢ (F \in (W MndHom W) \land z \in C \land y \in C) \to F (z +_{W} y) = F (z) +_{W} F (y)$
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 p A x = p A (z +_{W} y)$
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 p A x = p A z$
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 p A x = p A y$
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 \|-

Metamath Proof Explorer

Theorem fxpsubm

Proof