Metamath Proof Explorer

Theorem fxpgaeq

Description: A fixed point X is invariant under 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 ) )
fxpgaeq.x 
|- ( ph -> X e. ( C FixPts A ) )
fxpgaeq.p 
|- ( ph -> P e. U )
Assertion fxpgaeq 
|- ( ph -> ( 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 fxpgaeq.x 
 |-  ( ph -> X e. ( C FixPts A ) )
4 fxpgaeq.p 
 |-  ( ph -> P e. U )
5 oveq1 
 |-  ( p = P -> ( p A X ) = ( P A X ) )
6 5 eqeq1d 
 |-  ( p = P -> ( ( p A X ) = X <-> ( P A X ) = X ) )
7 1 2 fxpgaval 
 |-  ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )
8 3 7 eleqtrd 
 |-  ( ph -> X e. { x e. C | A. p e. U ( p A x ) = x } )
9 oveq2 
 |-  ( x = X -> ( p A x ) = ( p A X ) )
10 id 
 |-  ( x = X -> x = X )
11 9 10 eqeq12d 
 |-  ( x = X -> ( ( p A x ) = x <-> ( p A X ) = X ) )
12 11 ralbidv 
 |-  ( x = X -> ( A. p e. U ( p A x ) = x <-> A. p e. U ( p A X ) = X ) )
13 12 elrab 
 |-  ( X e. { x e. C | A. p e. U ( p A x ) = x } <-> ( X e. C /\ A. p e. U ( p A X ) = X ) )
14 8 13 sylib 
 |-  ( ph -> ( X e. C /\ A. p e. U ( p A X ) = X ) )
15 14 simprd 
 |-  ( ph -> A. p e. U ( p A X ) = X )
16 6 15 4 rspcdva 
 |-  ( ph -> ( P A X ) = X )