This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Base G
fxpgaval.a ⊢ φ → A ∈ G GrpAct C
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 = Base G
2 fxpgaval.a ⊢ φ → A ∈ G GrpAct C
3 simpr ⊢ φ ∧ C = ∅ → C = ∅
4 3 rabeqdv ⊢ φ ∧ C = ∅ → x ∈ C | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x = x ∈ ∅ | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
5 rab0 ⊢ x ∈ ∅ | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x = ∅
6 4 5 eqtrdi ⊢ φ ∧ C = ∅ → x ∈ C | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x = ∅
7 gaset ⊢ A ∈ G GrpAct C → C ∈ V
8 2 7 syl ⊢ φ → C ∈ 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 ⊢ φ ∧ C = ∅ → x ∈ C | ∀ p ∈ U p A x = x = x ∈ ∅ | ∀ p ∈ U p A x = x
12 rab0 ⊢ x ∈ ∅ | ∀ p ∈ U p A x = x = ∅
13 11 12 eqtrdi ⊢ φ ∧ C = ∅ → x ∈ C | ∀ p ∈ U p A x = x = ∅
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 ∈ G GrpAct C → A : U × C ⟶ C
17 2 16 syl ⊢ φ → A : U × C ⟶ C
18 17 fdmd ⊢ φ → dom ⁡ A = U × C
19 18 dmeqd ⊢ φ → dom ⁡ dom ⁡ A = dom ⁡ U × C
20 dmxp ⊢ C ≠ ∅ → dom ⁡ U × C = U
21 19 20 sylan9eq ⊢ φ ∧ C ≠ ∅ → dom ⁡ dom ⁡ A = U
22 21 raleqdv ⊢ φ ∧ C ≠ ∅ → ∀ p ∈ dom ⁡ dom ⁡ A p A x = x ↔ ∀ p ∈ U p A x = x
23 22 rabbidv ⊢ φ ∧ C ≠ ∅ → x ∈ C | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x = x ∈ C | ∀ p ∈ U p A x = x
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 |-