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	⊢ 𝑈 = ( Base ‘ 𝐺 )
	fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
	fxpgaeq.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) )
	fxpgaeq.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
Assertion	fxpgaeq	⊢ ( 𝜑 → ( 𝑃 𝐴 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	⊢ 𝑈 = ( Base ‘ 𝐺 )
2		fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
3		fxpgaeq.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) )
4		fxpgaeq.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
5		oveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 𝐴 𝑋 ) = ( 𝑃 𝐴 𝑋 ) )
6	5	eqeq1d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 𝐴 𝑋 ) = 𝑋 ↔ ( 𝑃 𝐴 𝑋 ) = 𝑋 ) )
7	1 2	fxpgaval	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
8	3 7	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
9		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑋 ) )
10		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
11	9 10	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑝 𝐴 𝑥 ) = 𝑥 ↔ ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
12	11	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
13	12	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } ↔ ( 𝑋 ∈ 𝐶 ∧ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
14	8 13	sylib	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ∧ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
15	14	simprd	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 )
16	6 15 4	rspcdva	⊢ ( 𝜑 → ( 𝑃 𝐴 𝑋 ) = 𝑋 )