Metamath Proof Explorer

Theorem fxpsdrg

Description: The fixed points of a group action A on a division ring W is a sub-division-ring. Since sub-division-rings of fields are subfields (see fldsdrgfld ), ( C FixPts A ) might be called the fixed subfield 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 e. C |-> ( p A x ) )
fxpsubm.a 
|- ( ph -> A e. ( G GrpAct C ) )
fxpsubrg.1 
|- ( ( ph /\ p e. B ) -> F e. ( W RingHom W ) )
fxpsdrg.1 
|- ( ph -> W e. DivRing )
Assertion fxpsdrg 
|- ( ph -> ( C FixPts A ) e. ( SubDRing ` 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 fxpsdrg.1 
 |-  ( ph -> W e. DivRing )
7 1 2 3 4 5 fxpsubrg 
 |-  ( ph -> ( C FixPts A ) e. ( SubRing ` W ) )
8 5 adantlr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> F e. ( W RingHom W ) )
9 6 adantr 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> W e. DivRing )
10 9 adantr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> W e. DivRing )
11 gaset 
 |-  ( A e. ( G GrpAct C ) -> C e. _V )
12 4 11 syl 
 |-  ( ph -> C e. _V )
13 12 4 fxpss 
 |-  ( ph -> ( C FixPts A ) C_ C )
14 13 ssdifssd 
 |-  ( ph -> ( ( C FixPts A ) \ { ( 0g ` W ) } ) C_ C )
15 14 sselda 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z e. C )
16 15 adantr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. C )
17 eldifsni 
 |-  ( z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) -> z =/= ( 0g ` W ) )
18 17 adantl 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z =/= ( 0g ` W ) )
19 18 adantr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z =/= ( 0g ` W ) )
20 eqid 
 |-  ( Unit ` W ) = ( Unit ` W )
21 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
22 2 20 21 drngunit 
 |-  ( W e. DivRing -> ( z e. ( Unit ` W ) <-> ( z e. C /\ z =/= ( 0g ` W ) ) ) )
23 22 biimpar 
 |-  ( ( W e. DivRing /\ ( z e. C /\ z =/= ( 0g ` W ) ) ) -> z e. ( Unit ` W ) )
24 10 16 19 23 syl12anc 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( Unit ` W ) )
25 rhmunitinv 
 |-  ( ( F e. ( W RingHom W ) /\ z e. ( Unit ` W ) ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` ( F ` z ) ) )
26 8 24 25 syl2anc 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` ( F ` z ) ) )
27 oveq2 
 |-  ( x = ( ( invr ` W ) ` z ) -> ( p A x ) = ( p A ( ( invr ` W ) ` z ) ) )
28 eqid 
 |-  ( invr ` W ) = ( invr ` W )
29 2 21 28 9 15 18 drnginvrcld 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. C )
30 29 adantr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` z ) e. C )
31 ovexd 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) e. _V )
32 3 27 30 31 fvmptd3 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( p A ( ( invr ` W ) ` z ) ) )
33 oveq2 
 |-  ( x = z -> ( p A x ) = ( p A z ) )
34 ovexd 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) e. _V )
35 3 33 16 34 fvmptd3 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) )
36 4 adantr 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A e. ( G GrpAct C ) )
37 36 adantr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> A e. ( G GrpAct C ) )
38 simplr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) )
39 38 eldifad 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( C FixPts A ) )
40 simpr 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> p e. B )
41 1 37 39 40 fxpgaeq 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) = z )
42 35 41 eqtrd 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = z )
43 42 fveq2d 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` ( F ` z ) ) = ( ( invr ` W ) ` z ) )
44 26 32 43 3eqtr3d 
 |-  ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) )
45 44 ralrimiva 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) )
46 1 36 29 isfxp 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( ( invr ` W ) ` z ) e. ( C FixPts A ) <-> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) )
47 45 46 mpbird 
 |-  ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. ( C FixPts A ) )
48 47 ralrimiva 
 |-  ( ph -> A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) )
49 28 21 issdrg2 
 |-  ( ( C FixPts A ) e. ( SubDRing ` W ) <-> ( W e. DivRing /\ ( C FixPts A ) e. ( SubRing ` W ) /\ A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) )
50 6 7 48 49 syl3anbrc 
 |-  ( ph -> ( C FixPts A ) e. ( SubDRing ` W ) )