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 
|- B = ( Base ` G )
fxpsubm.c 
|- C = ( Base ` W )
fxpsubm.f 
|- F = ( x e. C |-> ( p A x ) )
fxpsubm.a 
|- ( ph -> A e. ( G GrpAct C ) )
fxpsubrg.1 
|- ( ( ph /\ p e. B ) -> F e. ( W RingHom W ) )
Assertion fxpsubrg 
|- ( ph -> ( C FixPts A ) e. ( SubRing ` W ) )

Proof

Step Hyp Ref Expression
1 fxpsubm.b 
 |-  B = ( Base ` G )
2 fxpsubm.c 
 |-  C = ( Base ` W )
3 fxpsubm.f 
 |-  F = ( x e. C |-> ( p A x ) )
4 fxpsubm.a 
 |-  ( ph -> A e. ( G GrpAct C ) )
5 fxpsubrg.1 
 |-  ( ( ph /\ p e. B ) -> F e. ( W RingHom W ) )
6 oveq1 
 |-  ( p = ( 0g ` G ) -> ( p A x ) = ( ( 0g ` G ) A x ) )
7 6 mpteq2dv 
 |-  ( p = ( 0g ` G ) -> ( x e. C |-> ( p A x ) ) = ( x e. C |-> ( ( 0g ` G ) A x ) ) )
8 3 7 eqtrid 
 |-  ( p = ( 0g ` G ) -> F = ( x e. C |-> ( ( 0g ` G ) A x ) ) )
9 8 eleq1d 
 |-  ( p = ( 0g ` G ) -> ( F e. ( W RingHom W ) <-> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W RingHom W ) ) )
10 5 ralrimiva 
 |-  ( ph -> A. p e. B F e. ( W RingHom W ) )
11 gagrp 
 |-  ( A e. ( G GrpAct C ) -> G e. Grp )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 1 12 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
14 4 11 13 3syl 
 |-  ( ph -> ( 0g ` G ) e. B )
15 9 10 14 rspcdva 
 |-  ( ph -> ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W RingHom W ) )
16 rhmrcl1 
 |-  ( ( x e. C |-> ( ( 0g ` G ) A x ) ) e. ( W RingHom W ) -> W e. Ring )
17 15 16 syl 
 |-  ( ph -> W e. Ring )
18 rhmghm 
 |-  ( F e. ( W RingHom W ) -> F e. ( W GrpHom W ) )
19 5 18 syl 
 |-  ( ( ph /\ p e. B ) -> F e. ( W GrpHom W ) )
20 1 2 3 4 19 fxpsubg 
 |-  ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) )
21 oveq2 
 |-  ( x = ( 1r ` W ) -> ( p A x ) = ( p A ( 1r ` W ) ) )
22 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
23 2 22 17 ringidcld 
 |-  ( ph -> ( 1r ` W ) e. C )
24 23 adantr 
 |-  ( ( ph /\ p e. B ) -> ( 1r ` W ) e. C )
25 ovexd 
 |-  ( ( ph /\ p e. B ) -> ( p A ( 1r ` W ) ) e. _V )
26 3 21 24 25 fvmptd3 
 |-  ( ( ph /\ p e. B ) -> ( F ` ( 1r ` W ) ) = ( p A ( 1r ` W ) ) )
27 22 22 rhm1 
 |-  ( F e. ( W RingHom W ) -> ( F ` ( 1r ` W ) ) = ( 1r ` W ) )
28 5 27 syl 
 |-  ( ( ph /\ p e. B ) -> ( F ` ( 1r ` W ) ) = ( 1r ` W ) )
29 26 28 eqtr3d 
 |-  ( ( ph /\ p e. B ) -> ( p A ( 1r ` W ) ) = ( 1r ` W ) )
30 29 ralrimiva 
 |-  ( ph -> A. p e. B ( p A ( 1r ` W ) ) = ( 1r ` W ) )
31 1 4 23 isfxp 
 |-  ( ph -> ( ( 1r ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 1r ` W ) ) = ( 1r ` W ) ) )
32 30 31 mpbird 
 |-  ( ph -> ( 1r ` W ) e. ( C FixPts A ) )
33 5 ad4ant14 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W RingHom W ) )
34 gaset 
 |-  ( A e. ( G GrpAct C ) -> C e. _V )
35 4 34 syl 
 |-  ( ph -> C e. _V )
36 35 4 fxpss 
 |-  ( ph -> ( C FixPts A ) C_ C )
37 36 sselda 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C )
38 37 adantr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C )
39 38 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C )
40 36 adantr 
 |-  ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C )
41 40 sselda 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C )
42 41 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C )
43 eqid 
 |-  ( .r ` W ) = ( .r ` W )
44 2 43 43 rhmmul 
 |-  ( ( F e. ( W RingHom W ) /\ z e. C /\ y e. C ) -> ( F ` ( z ( .r ` W ) y ) ) = ( ( F ` z ) ( .r ` W ) ( F ` y ) ) )
45 33 39 42 44 syl3anc 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( ( F ` z ) ( .r ` W ) ( F ` y ) ) )
46 oveq2 
 |-  ( x = ( z ( .r ` W ) y ) -> ( p A x ) = ( p A ( z ( .r ` W ) y ) ) )
47 17 ad2antrr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Ring )
48 2 43 47 38 41 ringcld 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. C )
49 ovexd 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( p A ( z ( .r ` W ) y ) ) e. _V )
50 3 46 48 49 fvmptd3 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) )
51 50 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) )
52 oveq2 
 |-  ( x = z -> ( p A x ) = ( p A z ) )
53 ovexd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V )
54 3 52 39 53 fvmptd3 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) )
55 4 ad2antrr 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) )
56 55 adantr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) )
57 simpllr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) )
58 simpr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B )
59 1 56 57 58 fxpgaeq 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z )
60 54 59 eqtrd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z )
61 oveq2 
 |-  ( x = y -> ( p A x ) = ( p A y ) )
62 ovexd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V )
63 3 61 42 62 fvmptd3 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) )
64 simplr 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) )
65 1 56 64 58 fxpgaeq 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y )
66 63 65 eqtrd 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y )
67 60 66 oveq12d 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( .r ` W ) ( F ` y ) ) = ( z ( .r ` W ) y ) )
68 45 51 67 3eqtr3d 
 |-  ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) )
69 68 ralrimiva 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) )
70 1 55 48 isfxp 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( ( z ( .r ` W ) y ) e. ( C FixPts A ) <-> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) )
71 69 70 mpbird 
 |-  ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) )
72 71 anasss 
 |-  ( ( ph /\ ( z e. ( C FixPts A ) /\ y e. ( C FixPts A ) ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) )
73 72 ralrimivva 
 |-  ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) )
74 2 22 43 issubrg2 
 |-  ( W e. Ring -> ( ( C FixPts A ) e. ( SubRing ` W ) <-> ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) )
75 74 biimpar 
 |-  ( ( W e. Ring /\ ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) -> ( C FixPts A ) e. ( SubRing ` W ) )
76 17 20 32 73 75 syl13anc 
 |-  ( ph -> ( C FixPts A ) e. ( SubRing ` W ) )