Metamath Proof Explorer

Theorem gastacos

Description: Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses gasta.1 ⊢ X = Base G
gasta.2 ⊢ H = u ∈ X | u ⊕ ˙ A = A
orbsta.r ⊢ ∼ ˙ = G ~ QG H
Assertion gastacos ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∼ ˙ C ↔ B ⊕ ˙ A = C ⊕ ˙ 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 1 2 gastacl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → H ∈ SubGrp ⁡ G
5 4 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → H ∈ SubGrp ⁡ G
6 subgrcl ⊢ H ∈ SubGrp ⁡ G → G ∈ Grp
7 5 6 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → G ∈ Grp
8 1 subgss ⊢ H ∈ SubGrp ⁡ G → H ⊆ X
9 5 8 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → H ⊆ X
10 eqid ⊢ inv g ⁡ G = inv g ⁡ G
11 eqid ⊢ + G = + G
12 1 10 11 3 eqgval ⊢ G ∈ Grp ∧ H ⊆ X → B ∼ ˙ C ↔ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H
13 7 9 12 syl2anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∼ ˙ C ↔ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H
14 df-3an ⊢ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H ↔ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H
15 13 14 bitrdi ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∼ ˙ C ↔ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H
16 simpr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∈ X ∧ C ∈ X
17 16 biantrurd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ∈ H ↔ B ∈ X ∧ C ∈ X ∧ inv g ⁡ G ⁡ B + G C ∈ H
18 simpll ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → ⊕ ˙ ∈ G GrpAct Y
19 simprl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∈ X
20 1 10 grpinvcl ⊢ G ∈ Grp ∧ B ∈ X → inv g ⁡ G ⁡ B ∈ X
21 7 19 20 syl2anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B ∈ X
22 simprr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → C ∈ X
23 simplr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → A ∈ Y
24 1 11 gaass ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ inv g ⁡ G ⁡ B ∈ X ∧ C ∈ X ∧ A ∈ Y → inv g ⁡ G ⁡ B + G C ⊕ ˙ A = inv g ⁡ G ⁡ B ⊕ ˙ C ⊕ ˙ A
25 18 21 22 23 24 syl13anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ⊕ ˙ A = inv g ⁡ G ⁡ B ⊕ ˙ C ⊕ ˙ A
26 25 eqeq1d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ⊕ ˙ A = A ↔ inv g ⁡ G ⁡ B ⊕ ˙ C ⊕ ˙ A = A
27 1 11 grpcl ⊢ G ∈ Grp ∧ inv g ⁡ G ⁡ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ∈ X
28 7 21 22 27 syl3anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ∈ X
29 oveq1 ⊢ u = inv g ⁡ G ⁡ B + G C → u ⊕ ˙ A = inv g ⁡ G ⁡ B + G C ⊕ ˙ A
30 29 eqeq1d ⊢ u = inv g ⁡ G ⁡ B + G C → u ⊕ ˙ A = A ↔ inv g ⁡ G ⁡ B + G C ⊕ ˙ A = A
31 30 2 elrab2 ⊢ inv g ⁡ G ⁡ B + G C ∈ H ↔ inv g ⁡ G ⁡ B + G C ∈ X ∧ inv g ⁡ G ⁡ B + G C ⊕ ˙ A = A
32 31 baib ⊢ inv g ⁡ G ⁡ B + G C ∈ X → inv g ⁡ G ⁡ B + G C ∈ H ↔ inv g ⁡ G ⁡ B + G C ⊕ ˙ A = A
33 28 32 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ∈ H ↔ inv g ⁡ G ⁡ B + G C ⊕ ˙ A = A
34 1 gaf ⊢ ⊕ ˙ ∈ G GrpAct Y → ⊕ ˙ : X × Y ⟶ Y
35 18 34 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → ⊕ ˙ : X × Y ⟶ Y
36 35 22 23 fovrnd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → C ⊕ ˙ A ∈ Y
37 1 10 gacan ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ B ∈ X ∧ A ∈ Y ∧ C ⊕ ˙ A ∈ Y → B ⊕ ˙ A = C ⊕ ˙ A ↔ inv g ⁡ G ⁡ B ⊕ ˙ C ⊕ ˙ A = A
38 18 19 23 36 37 syl13anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ⊕ ˙ A = C ⊕ ˙ A ↔ inv g ⁡ G ⁡ B ⊕ ˙ C ⊕ ˙ A = A
39 26 33 38 3bitr4d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → inv g ⁡ G ⁡ B + G C ∈ H ↔ B ⊕ ˙ A = C ⊕ ˙ A
40 15 17 39 3bitr2d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ B ∈ X ∧ C ∈ X → B ∼ ˙ C ↔ B ⊕ ˙ A = C ⊕ ˙ A