Metamath Proof Explorer

Theorem orbstafun

Description: Existence and uniqueness for the function of orbsta . (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 orbstafun ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → Fun ⁡ F

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 = h → k ⊕ ˙ A = h ⊕ ˙ A
12 simpr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ∼ ˙ h
13 subgrcl ⊢ H ∈ SubGrp ⁡ G → G ∈ Grp
14 1 subgss ⊢ H ∈ SubGrp ⁡ G → H ⊆ X
15 eqid ⊢ inv g ⁡ G = inv g ⁡ G
16 eqid ⊢ + G = + G
17 1 15 16 3 eqgval ⊢ G ∈ Grp ∧ H ⊆ X → k ∼ ˙ h ↔ k ∈ X ∧ h ∈ X ∧ inv g ⁡ G ⁡ k + G h ∈ H
18 13 14 17 syl2anc ⊢ H ∈ SubGrp ⁡ G → k ∼ ˙ h ↔ k ∈ X ∧ h ∈ X ∧ inv g ⁡ G ⁡ k + G h ∈ H
19 6 18 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → k ∼ ˙ h ↔ k ∈ X ∧ h ∈ X ∧ inv g ⁡ G ⁡ k + G h ∈ H
20 19 biimpa ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ∈ X ∧ h ∈ X ∧ inv g ⁡ G ⁡ k + G h ∈ H
21 20 simp1d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ∈ X
22 20 simp2d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → h ∈ X
23 21 22 jca ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ∈ X ∧ h ∈ X
24 1 2 3 gastacos ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∈ X ∧ h ∈ X → k ∼ ˙ h ↔ k ⊕ ˙ A = h ⊕ ˙ A
25 23 24 syldan ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ∼ ˙ h ↔ k ⊕ ˙ A = h ⊕ ˙ A
26 12 25 mpbid ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ k ∼ ˙ h → k ⊕ ˙ A = h ⊕ ˙ A
27 4 5 8 10 11 26 qliftfund ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → Fun ⁡ F