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 𝑋 = ( Base ‘ 𝐺 )
gasta.2 𝐻 = { 𝑢𝑋 ∣ ( 𝑢 𝐴 ) = 𝐴 }
orbsta.r = ( 𝐺 ~QG 𝐻 )
Assertion gastacos ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐶 ↔ ( 𝐵 𝐴 ) = ( 𝐶 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 gasta.1 𝑋 = ( Base ‘ 𝐺 )
2 gasta.2 𝐻 = { 𝑢𝑋 ∣ ( 𝑢 𝐴 ) = 𝐴 }
3 orbsta.r = ( 𝐺 ~QG 𝐻 )
4 1 2 gastacl ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
5 4 adantr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgrcl ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 5 6 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐺 ∈ Grp )
8 1 subgss ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻𝑋 )
9 5 8 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐻𝑋 )
10 eqid ( invg𝐺 ) = ( invg𝐺 )
11 eqid ( +g𝐺 ) = ( +g𝐺 )
12 1 10 11 3 eqgval ( ( 𝐺 ∈ Grp ∧ 𝐻𝑋 ) → ( 𝐵 𝐶 ↔ ( 𝐵𝑋𝐶𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) ) )
13 7 9 12 syl2anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐶 ↔ ( 𝐵𝑋𝐶𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) ) )
14 df-3an ( ( 𝐵𝑋𝐶𝑋 ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) ↔ ( ( 𝐵𝑋𝐶𝑋 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) )
15 13 14 bitrdi ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐶 ↔ ( ( 𝐵𝑋𝐶𝑋 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) ) )
16 simpr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵𝑋𝐶𝑋 ) )
17 16 biantrurd ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( 𝐵𝑋𝐶𝑋 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ) ) )
18 simpll ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ∈ ( 𝐺 GrpAct 𝑌 ) )
19 simprl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐵𝑋 )
20 1 10 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝐵𝑋 ) → ( ( invg𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
21 7 19 20 syl2anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( invg𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
22 simprr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐶𝑋 )
23 simplr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → 𝐴𝑌 )
24 1 11 gaass ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ( ( invg𝐺 ) ‘ 𝐵 ) ∈ 𝑋𝐶𝑋𝐴𝑌 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = ( ( ( invg𝐺 ) ‘ 𝐵 ) ( 𝐶 𝐴 ) ) )
25 18 21 22 23 24 syl13anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = ( ( ( invg𝐺 ) ‘ 𝐵 ) ( 𝐶 𝐴 ) ) )
26 25 eqeq1d ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = 𝐴 ↔ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( 𝐶 𝐴 ) ) = 𝐴 ) )
27 1 11 grpcl ( ( 𝐺 ∈ Grp ∧ ( ( invg𝐺 ) ‘ 𝐵 ) ∈ 𝑋𝐶𝑋 ) → ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝑋 )
28 7 21 22 27 syl3anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝑋 )
29 oveq1 ( 𝑢 = ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) → ( 𝑢 𝐴 ) = ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) )
30 29 eqeq1d ( 𝑢 = ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) → ( ( 𝑢 𝐴 ) = 𝐴 ↔ ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = 𝐴 ) )
31 30 2 elrab2 ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝑋 ∧ ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = 𝐴 ) )
32 31 baib ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝑋 → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = 𝐴 ) )
33 28 32 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) 𝐴 ) = 𝐴 ) )
34 1 gaf ( ∈ ( 𝐺 GrpAct 𝑌 ) → : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
35 18 34 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
36 35 22 23 fovrnd ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐶 𝐴 ) ∈ 𝑌 )
37 1 10 gacan ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐵𝑋𝐴𝑌 ∧ ( 𝐶 𝐴 ) ∈ 𝑌 ) ) → ( ( 𝐵 𝐴 ) = ( 𝐶 𝐴 ) ↔ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( 𝐶 𝐴 ) ) = 𝐴 ) )
38 18 19 23 36 37 syl13anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐵 𝐴 ) = ( 𝐶 𝐴 ) ↔ ( ( ( invg𝐺 ) ‘ 𝐵 ) ( 𝐶 𝐴 ) ) = 𝐴 ) )
39 26 33 38 3bitr4d ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( ( ( invg𝐺 ) ‘ 𝐵 ) ( +g𝐺 ) 𝐶 ) ∈ 𝐻 ↔ ( 𝐵 𝐴 ) = ( 𝐶 𝐴 ) ) )
40 15 17 39 3bitr2d ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴𝑌 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐶 ↔ ( 𝐵 𝐴 ) = ( 𝐶 𝐴 ) ) )