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

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 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → 𝑘 ∼ ℎ )
13 subgrcl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
15 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
16 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
17 1 15 16 3 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ⊆ 𝑋 ) → ( 𝑘 ∼ ℎ ↔ ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑘 ) ( +g ‘ 𝐺 ) ℎ ) ∈ 𝐻 ) ) )
18 13 14 17 syl2anc ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑘 ∼ ℎ ↔ ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑘 ) ( +g ‘ 𝐺 ) ℎ ) ∈ 𝐻 ) ) )
19 6 18 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑘 ∼ ℎ ↔ ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑘 ) ( +g ‘ 𝐺 ) ℎ ) ∈ 𝐻 ) ) )
20 19 biimpa ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑘 ) ( +g ‘ 𝐺 ) ℎ ) ∈ 𝐻 ) )
21 20 simp1d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → 𝑘 ∈ 𝑋 )
22 20 simp2d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → ℎ ∈ 𝑋 )
23 21 22 jca ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ) )
24 1 2 3 gastacos ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ) ) → ( 𝑘 ∼ ℎ ↔ ( 𝑘 ⊕ 𝐴 ) = ( ℎ ⊕ 𝐴 ) ) )
25 23 24 syldan ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → ( 𝑘 ∼ ℎ ↔ ( 𝑘 ⊕ 𝐴 ) = ( ℎ ⊕ 𝐴 ) ) )
26 12 25 mpbid ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∼ ℎ ) → ( 𝑘 ⊕ 𝐴 ) = ( ℎ ⊕ 𝐴 ) )
27 4 5 8 10 11 26 qliftfund ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → Fun 𝐹 )