Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 fxpsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fxpsubg.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
3 fxpsubm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
4 fxpsubg.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
5 fxpsubm.1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )
6 oveq1 ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑝 𝐴 𝑥 ) = ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) )
7 6 mpteq2dv ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
8 3 7 eqtrid ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
9 8 eleq1d ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) ↔ ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 MndHom 𝑊 ) ) )
10 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )
11 gagrp ⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐺 ∈ Grp )
12 4 11 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
13 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14 1 13 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
15 12 14 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
16 9 10 15 rspcdva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 MndHom 𝑊 ) )
17 mhmrcl1 ⊢ ( ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 MndHom 𝑊 ) → 𝑊 ∈ Mnd )
18 16 17 syl ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
19 gaset ⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐶 ∈ V )
20 4 19 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
21 20 4 fxpss ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
22 oveq2 ⊢ ( 𝑥 = ( 0g ‘ 𝑊 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) )
23 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
24 2 23 mndidcl ⊢ ( 𝑊 ∈ Mnd → ( 0g ‘ 𝑊 ) ∈ 𝐶 )
25 18 24 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ 𝐶 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 0g ‘ 𝑊 ) ∈ 𝐶 )
27 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) ∈ V )
28 3 22 26 27 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) )
29 23 23 mhm0 ⊢ ( 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) → ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
30 5 29 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
31 28 30 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
33 1 4 25 isfxp ⊢ ( 𝜑 → ( ( 0g ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) ) )
34 32 33 mpbird ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) )
35 5 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )
36 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
37 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) )
38 36 37 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑧 ∈ 𝐶 )
39 38 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
40 21 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
41 40 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑦 ∈ 𝐶 )
42 41 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑦 ∈ 𝐶 )
43 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
44 2 43 43 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) ∧ 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
45 35 39 42 44 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
46 oveq2 ⊢ ( 𝑥 = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) )
47 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑊 ∈ Mnd )
48 2 43 47 38 41 mndcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝐶 )
49 48 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝐶 )
50 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) ∈ V )
51 3 46 49 50 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) )
52 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑧 ) )
53 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) ∈ V )
54 3 52 39 53 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑝 𝐴 𝑧 ) )
55 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
56 55 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
57 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) )
58 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
59 1 56 57 58 fxpgaeq ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) = 𝑧 )
60 54 59 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
61 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑦 ) )
62 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑦 ) ∈ V )
63 3 61 42 62 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑝 𝐴 𝑦 ) )
64 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) )
65 1 56 64 58 fxpgaeq ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑦 ) = 𝑦 )
66 63 65 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = 𝑦 )
67 60 66 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
68 45 51 67 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
69 68 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
70 1 55 48 isfxp ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) )
71 69 70 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
72 71 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
73 72 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
74 2 23 43 issubm ⊢ ( 𝑊 ∈ Mnd → ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) ↔ ( ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 ∧ ( 0g ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) )
75 74 biimpar ⊢ ( ( 𝑊 ∈ Mnd ∧ ( ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 ∧ ( 0g ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) → ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) )
76 18 21 34 73 75 syl13anc ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubMnd ‘ 𝑊 ) )