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=BaseG
gasta.2 ⊢H=u∈X|u⊕˙A=A
orbsta.r ⊢∼˙=G~QGH
orbsta.f ⊢F=ran⁡k∈X⟼k∼˙k⊕˙A
Assertion orbstafun ⊢⊕˙∈GGrpActY∧A∈Y→Fun⁡F

Proof

Step Hyp Ref Expression
1 gasta.1 ⊢X=BaseG
2 gasta.2 ⊢H=u∈X|u⊕˙A=A
3 orbsta.r ⊢∼˙=G~QGH
4 orbsta.f ⊢F=ran⁡k∈X⟼k∼˙k⊕˙A
5 ovexd ⊢⊕˙∈GGrpActY∧A∈Y∧k∈X→k⊕˙A∈V
6 1 2 gastacl ⊢⊕˙∈GGrpActY∧A∈Y→H∈SubGrp⁡G
7 1 3 eqger ⊢H∈SubGrp⁡G→∼˙ErX
8 6 7 syl ⊢⊕˙∈GGrpActY∧A∈Y→∼˙ErX
9 1 fvexi ⊢X∈V
10 9 a1i ⊢⊕˙∈GGrpActY∧A∈Y→X∈V
11 oveq1 ⊢k=h→k⊕˙A=h⊕˙A
12 simpr ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k∼˙h
13 subgrcl ⊢H∈SubGrp⁡G→G∈Grp
14 1 subgss ⊢H∈SubGrp⁡G→H⊆X
15 eqid ⊢invg⁡G=invg⁡G
16 eqid ⊢+G=+G
17 1 15 16 3 eqgval ⊢G∈Grp∧H⊆X→k∼˙h↔k∈X∧h∈X∧invg⁡G⁡k+Gh∈H
18 13 14 17 syl2anc ⊢H∈SubGrp⁡G→k∼˙h↔k∈X∧h∈X∧invg⁡G⁡k+Gh∈H
19 6 18 syl ⊢⊕˙∈GGrpActY∧A∈Y→k∼˙h↔k∈X∧h∈X∧invg⁡G⁡k+Gh∈H
20 19 biimpa ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k∈X∧h∈X∧invg⁡G⁡k+Gh∈H
21 20 simp1d ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k∈X
22 20 simp2d ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→h∈X
23 21 22 jca ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k∈X∧h∈X
24 1 2 3 gastacos ⊢⊕˙∈GGrpActY∧A∈Y∧k∈X∧h∈X→k∼˙h↔k⊕˙A=h⊕˙A
25 23 24 syldan ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k∼˙h↔k⊕˙A=h⊕˙A
26 12 25 mpbid ⊢⊕˙∈GGrpActY∧A∈Y∧k∼˙h→k⊕˙A=h⊕˙A
27 4 5 8 10 11 26 qliftfund ⊢⊕˙∈GGrpActY∧A∈Y→Fun⁡F