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

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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gasta.2 ⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
orbsta.r ⊢ ∼ = ( 𝐺 ~QG 𝐻 )
orbsta.f ⊢ 𝐹 = ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ )
Assertion orbstaval ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ [ 𝐵 ] ∼ ) = ( 𝐵 ⊕ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 gasta.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gasta.2 ⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
3 orbsta.r ⊢ ∼ = ( 𝐺 ~QG 𝐻 )
4 orbsta.f ⊢ 𝐹 = ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ )
5 ovexd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ⊕ 𝐴 ) ∈ V )
6 1 2 gastacl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
7 1 3 eqger ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
8 6 7 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ∼ Er 𝑋 )
9 1 fvexi ⊢ 𝑋 ∈ V
10 9 a1i ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝑋 ∈ V )
11 oveq1 ⊢ ( 𝑘 = 𝐵 → ( 𝑘 ⊕ 𝐴 ) = ( 𝐵 ⊕ 𝐴 ) )
12 1 2 3 4 orbstafun ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → Fun 𝐹 )
13 4 5 8 10 11 12 qliftval ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ [ 𝐵 ] ∼ ) = ( 𝐵 ⊕ 𝐴 ) )