Metamath Proof Explorer

Theorem orbsta2

Description: Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses orbsta2.x ⊢ X = Base G
orbsta2.h ⊢ H = u ∈ X | u ⊕ ˙ A = A
orbsta2.r ⊢ ∼ ˙ = G ~ QG H
orbsta2.o ⊢ O = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
Assertion orbsta2 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X = A O ⁢ H

Proof

Step Hyp Ref Expression
1 orbsta2.x ⊢ X = Base G
2 orbsta2.h ⊢ H = u ∈ X | u ⊕ ˙ A = A
3 orbsta2.r ⊢ ∼ ˙ = G ~ QG H
4 orbsta2.o ⊢ O = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
5 1 2 gastacl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → H ∈ SubGrp ⁡ G
6 5 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → H ∈ SubGrp ⁡ G
7 simpr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X ∈ Fin
8 1 3 6 7 lagsubg2 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X = X / ∼ ˙ ⁢ H
9 pwfi ⊢ X ∈ Fin ↔ 𝒫 X ∈ Fin
10 9 bilani ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → 𝒫 X ∈ Fin
11 1 3 eqger ⊢ H ∈ SubGrp ⁡ G → ∼ ˙ Er X
12 6 11 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → ∼ ˙ Er X
13 12 qsss ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X / ∼ ˙ ⊆ 𝒫 X
14 10 13 ssfid ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X / ∼ ˙ ∈ Fin
15 eqid ⊢ ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A = ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A
16 1 2 3 15 4 orbsta ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A : X / ∼ ˙ ⟶ 1-1 onto A O
17 16 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A : X / ∼ ˙ ⟶ 1-1 onto A O
18 14 17 hasheqf1od ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X / ∼ ˙ = A O
19 18 oveq1d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X / ∼ ˙ ⁢ H = A O ⁢ H
20 8 19 eqtrd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ X ∈ Fin → X = A O ⁢ H