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

Metamath Proof Explorer

Theorem fxpsubrg

Description: The fixed points of a group action A on a ring W is a subgring. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses fxpsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
fxpsubm.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
fxpsubm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
fxpsubm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
fxpsubrg.1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
Assertion fxpsubrg ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 fxpsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fxpsubm.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
3 fxpsubm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
4 fxpsubm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
5 fxpsubrg.1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
6 oveq1 ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑝 𝐴 𝑥 ) = ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) )
7 6 mpteq2dv ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
8 3 7 eqtrid ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) )
9 8 eleq1d ⊢ ( 𝑝 = ( 0g ‘ 𝐺 ) → ( 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) ↔ ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 RingHom 𝑊 ) ) )
10 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
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 ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 RingHom 𝑊 ) )
16 rhmrcl1 ⊢ ( ( 𝑥 ∈ 𝐶 ↦ ( ( 0g ‘ 𝐺 ) 𝐴 𝑥 ) ) ∈ ( 𝑊 RingHom 𝑊 ) → 𝑊 ∈ Ring )
17 15 16 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
18 rhmghm ⊢ ( 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) → 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
19 5 18 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 GrpHom 𝑊 ) )
20 1 2 3 4 19 fxpsubg ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) )
21 oveq2 ⊢ ( 𝑥 = ( 1r ‘ 𝑊 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) )
22 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
23 2 22 17 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ 𝐶 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 1r ‘ 𝑊 ) ∈ 𝐶 )
25 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) ∈ V )
26 3 21 24 25 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 1r ‘ 𝑊 ) ) = ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) )
27 22 22 rhm1 ⊢ ( 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) → ( 𝐹 ‘ ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
28 5 27 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
29 26 28 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
31 1 4 23 isfxp ⊢ ( 𝜑 → ( ( 1r ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) ) )
32 30 31 mpbird ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) )
33 5 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
34 gaset ⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐶 ∈ V )
35 4 34 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
36 35 4 fxpss ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
37 36 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑧 ∈ 𝐶 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑧 ∈ 𝐶 )
39 38 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
40 36 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
41 40 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑦 ∈ 𝐶 )
42 41 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑦 ∈ 𝐶 )
43 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
44 2 43 43 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) ∧ 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
45 33 39 42 44 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
46 oveq2 ⊢ ( 𝑥 = ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) )
47 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → 𝑊 ∈ Ring )
48 2 43 47 38 41 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ 𝐶 )
49 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) ∈ V )
50 3 46 48 49 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) )
51 50 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) )
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 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 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 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) )
68 45 51 67 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) )
69 68 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) )
70 1 55 48 isfxp ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ) )
71 69 70 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) → ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
72 71 anasss ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∧ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ) ) → ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
73 72 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) )
74 2 22 43 issubrg2 ⊢ ( 𝑊 ∈ Ring → ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) ↔ ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 1r ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) )
75 74 biimpar ⊢ ( ( 𝑊 ∈ Ring ∧ ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 1r ‘ 𝑊 ) ∈ ( 𝐶 FixPts 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) ∀ 𝑦 ∈ ( 𝐶 FixPts 𝐴 ) ( 𝑧 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐶 FixPts 𝐴 ) ) ) → ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) )
76 17 20 32 73 75 syl13anc ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) )