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 ⊢ 𝑈 = ( 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 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )