Metamath Proof Explorer

Theorem orbstaval

Description: Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses gasta.1 ⊢ X = Base G
gasta.2 ⊢ H = u ∈ X | u ⊕ ˙ A = A
orbsta.r ⊢ ∼ ˙ = G ~ QG H
orbsta.f ⊢ F = ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A
Assertion orbstaval ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X → F ⁡ B ∼ ˙ = B ⊕ ˙ A

Proof

Step Hyp Ref Expression
1 gasta.1 ⊢ X = Base G
2 gasta.2 ⊢ H = u ∈ X | u ⊕ ˙ A = A
3 orbsta.r ⊢ ∼ ˙ = G ~ QG H
4 orbsta.f ⊢ F = ran ⁡ k ∈ X ⟼ k ∼ ˙ k ⊕ ˙ A
5 ovexd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∈ X → k ⊕ ˙ A ∈ V
6 1 2 gastacl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → H ∈ SubGrp ⁡ G
7 1 3 eqger ⊢ H ∈ SubGrp ⁡ G → ∼ ˙ Er X
8 6 7 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → ∼ ˙ Er X
9 1 fvexi ⊢ X ∈ V
10 9 a1i ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → X ∈ V
11 oveq1 ⊢ k = B → k ⊕ ˙ A = B ⊕ ˙ A
12 1 2 3 4 orbstafun ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → Fun ⁡ F
13 4 5 8 10 11 12 qliftval ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X → F ⁡ B ∼ ˙ = B ⊕ ˙ A