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 fovcdmd ⊢ ( ( ( ⊕ ∈ ( 𝐺 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 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∼ 𝐶 ↔ ( 𝐵 ⊕ 𝐴 ) = ( 𝐶 ⊕ 𝐴 ) ) )