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

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		simpr	$$⊢\left(\phi \wedge C=\varnothing \right)\to C=\varnothing$$
4	3	rabeqdv	$$⊢\left(\phi \wedge C=\varnothing \right)\to \left\{x\in C|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}=\left\{x\in \varnothing |\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}$$
5		rab0	$$⊢\left\{x\in \varnothing |\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}=\varnothing$$
6	4 5	eqtrdi	$$⊢\left(\phi \wedge C=\varnothing \right)\to \left\{x\in C|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}=\varnothing$$
7		gaset	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to C\in \mathrm{V}$$
8	2 7	syl	$$⊢\phi \to C\in \mathrm{V}$$
9	8 2	fxpval	Could not format ( ph -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) : No typesetting found for |- ( ph -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) with typecode |-
10	9	adantr	Could not format ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) : No typesetting found for |- ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) with typecode |-
11	3	rabeqdv	$$⊢\left(\phi \wedge C=\varnothing \right)\to \left\{x\in C|\forall p\in UpAx=x\right\}=\left\{x\in \varnothing |\forall p\in UpAx=x\right\}$$
12		rab0	$$⊢\left\{x\in \varnothing |\forall p\in UpAx=x\right\}=\varnothing$$
13	11 12	eqtrdi	$$⊢\left(\phi \wedge C=\varnothing \right)\to \left\{x\in C|\forall p\in UpAx=x\right\}=\varnothing$$
14	6 10 13	3eqtr4d	Could not format ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) : No typesetting found for |- ( ( ph /\ C = (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) with typecode |-
15	9	adantr	Could not format ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) : No typesetting found for |- ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. dom dom A ( p A x ) = x } ) with typecode |-
16	1	gaf	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to A:U\times C⟶C$$
17	2 16	syl	$$⊢\phi \to A:U\times C⟶C$$
18	17	fdmd	$$⊢\phi \to \mathrm{dom}A=U\times C$$
19	18	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}A=\mathrm{dom}\left(U\times C\right)$$
20		dmxp	$$⊢C\ne \varnothing \to \mathrm{dom}\left(U\times C\right)=U$$
21	19 20	sylan9eq	$$⊢\left(\phi \wedge C\ne \varnothing \right)\to \mathrm{dom}\mathrm{dom}A=U$$
22	21	raleqdv	$$⊢\left(\phi \wedge C\ne \varnothing \right)\to \left(\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\leftrightarrow \forall p\in UpAx=x\right)$$
23	22	rabbidv	$$⊢\left(\phi \wedge C\ne \varnothing \right)\to \left\{x\in C|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}=\left\{x\in C|\forall p\in UpAx=x\right\}$$
24	15 23	eqtrd	Could not format ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) : No typesetting found for |- ( ( ph /\ C =/= (/) ) -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) with typecode |-
25	14 24	pm2.61dane	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 |-