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={\mathrm{Base}}_G$$
	fxpgaval.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
	fxpgaeq.x	No typesetting found for |- ( ph -> X e. ( C FixPts A ) ) with typecode |-
	fxpgaeq.p	$$⊢\phi \to P\in U$$
Assertion	fxpgaeq	$$⊢\phi \to PAX=X$$

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	$$⊢U={\mathrm{Base}}_G$$
2		fxpgaval.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
3		fxpgaeq.x	Could not format ( ph -> X e. ( C FixPts A ) ) : No typesetting found for |- ( ph -> X e. ( C FixPts A ) ) with typecode |-
4		fxpgaeq.p	$$⊢\phi \to P\in U$$
5		oveq1	$$⊢p=P\to pAX=PAX$$
6	5	eqeq1d	$$⊢p=P\to \left(pAX=X\leftrightarrow PAX=X\right)$$
7	1 2	fxpgaval	Could not format ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) : No typesetting found for |- ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) with typecode |-
8	3 7	eleqtrd	$$⊢\phi \to X\in \left\{x\in C|\forall p\in UpAx=x\right\}$$
9		oveq2	$$⊢x=X\to pAx=pAX$$
10		id	$$⊢x=X\to x=X$$
11	9 10	eqeq12d	$$⊢x=X\to \left(pAx=x\leftrightarrow pAX=X\right)$$
12	11	ralbidv	$$⊢x=X\to \left(\forall p\in UpAx=x\leftrightarrow \forall p\in UpAX=X\right)$$
13	12	elrab	$$⊢X\in \left\{x\in C|\forall p\in UpAx=x\right\}\leftrightarrow \left(X\in C\wedge \forall p\in UpAX=X\right)$$
14	8 13	sylib	$$⊢\phi \to \left(X\in C\wedge \forall p\in UpAX=X\right)$$
15	14	simprd	$$⊢\phi \to \forall p\in UpAX=X$$
16	6 15 4	rspcdva	$$⊢\phi \to PAX=X$$