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	⊢ 𝑈 = ( Base ‘ 𝐺 )
	fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
Assertion	fxpgaval	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	⊢ 𝑈 = ( Base ‘ 𝐺 )
2		fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
3		simpr	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐶 = ∅ )
4	3	rabeqdv	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = { 𝑥 ∈ ∅ ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
5		rab0	⊢ { 𝑥 ∈ ∅ ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = ∅
6	4 5	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = ∅ )
7		gaset	⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐶 ∈ V )
8	2 7	syl	⊢ ( 𝜑 → 𝐶 ∈ V )
9	8 2	fxpval	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
11	3	rabeqdv	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = { 𝑥 ∈ ∅ ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
12		rab0	⊢ { 𝑥 ∈ ∅ ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = ∅
13	11 12	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = ∅ )
14	6 10 13	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
15	9	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ ∅ ) → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
16	1	gaf	⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐴 : ( 𝑈 × 𝐶 ) ⟶ 𝐶 )
17	2 16	syl	⊢ ( 𝜑 → 𝐴 : ( 𝑈 × 𝐶 ) ⟶ 𝐶 )
18	17	fdmd	⊢ ( 𝜑 → dom 𝐴 = ( 𝑈 × 𝐶 ) )
19	18	dmeqd	⊢ ( 𝜑 → dom dom 𝐴 = dom ( 𝑈 × 𝐶 ) )
20		dmxp	⊢ ( 𝐶 ≠ ∅ → dom ( 𝑈 × 𝐶 ) = 𝑈 )
21	19 20	sylan9eq	⊢ ( ( 𝜑 ∧ 𝐶 ≠ ∅ ) → dom dom 𝐴 = 𝑈 )
22	21	raleqdv	⊢ ( ( 𝜑 ∧ 𝐶 ≠ ∅ ) → ( ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 ) )
23	22	rabbidv	⊢ ( ( 𝜑 ∧ 𝐶 ≠ ∅ ) → { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
24	15 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝐶 ≠ ∅ ) → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
25	14 24	pm2.61dane	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )