Metamath Proof Explorer

Theorem fxpgaval

Description: Value of the set of fixed points for a group action A (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses fxpgaval.s 
|- U = ( Base ` G )
fxpgaval.a 
|- ( ph -> A e. ( G GrpAct C ) )
Assertion fxpgaval 
|- ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )

Proof

Step Hyp Ref Expression
1 fxpgaval.s 
 |-  U = ( Base ` G )
2 fxpgaval.a 
 |-  ( ph -> A e. ( G GrpAct C ) )
3 simpr 
 |-  ( ( ph /\ C = (/) ) -> C = (/) )
4 3 rabeqdv 
 |-  ( ( ph /\ C = (/) ) -> { x e. C | A. p e. dom dom A ( p A x ) = x } = { x e. (/) | A. p e. dom dom A ( p A x ) = x } )
5 rab0 
 |-  { x e. (/) | A. p e. dom dom A ( p A x ) = x } = (/)
6 4 5 eqtrdi 
 |-  ( ( ph /\ C = (/) ) -> { x e. C | A. p e. dom dom A ( p A x ) = x } = (/) )
7 gaset 
 |-  ( A e. ( G GrpAct C ) -> C e. _V )
8 2 7 syl 
 |-  ( ph -> C e. _V )
9 8 2 fxpval 
 |-  ( ph -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } )
10 9 adantr 
 |-  ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } )
11 3 rabeqdv 
 |-  ( ( ph /\ C = (/) ) -> { x e. C | A. p e. U ( p A x ) = x } = { x e. (/) | A. p e. U ( p A x ) = x } )
12 rab0 
 |-  { x e. (/) | A. p e. U ( p A x ) = x } = (/)
13 11 12 eqtrdi 
 |-  ( ( ph /\ C = (/) ) -> { x e. C | A. p e. U ( p A x ) = x } = (/) )
14 6 10 13 3eqtr4d 
 |-  ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )
15 9 adantr 
 |-  ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } )
16 1 gaf 
 |-  ( A e. ( G GrpAct C ) -> A : ( U X. C ) --> C )
17 2 16 syl 
 |-  ( ph -> A : ( U X. C ) --> C )
18 17 fdmd 
 |-  ( ph -> dom A = ( U X. C ) )
19 18 dmeqd 
 |-  ( ph -> dom dom A = dom ( U X. C ) )
20 dmxp 
 |-  ( C =/= (/) -> dom ( U X. C ) = U )
21 19 20 sylan9eq 
 |-  ( ( ph /\ C =/= (/) ) -> dom dom A = U )
22 21 raleqdv 
 |-  ( ( ph /\ C =/= (/) ) -> ( A. p e. dom dom A ( p A x ) = x <-> A. p e. U ( p A x ) = x ) )
23 22 rabbidv 
 |-  ( ( ph /\ C =/= (/) ) -> { x e. C | A. p e. dom dom A ( p A x ) = x } = { x e. C | A. p e. U ( p A x ) = x } )
24 15 23 eqtrd 
 |-  ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )
25 14 24 pm2.61dane 
 |-  ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )