This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑊 ) )