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=BaseG
gasta.2 ⊢H=u∈X|u⊕˙A=A
orbsta.r ⊢∼˙=G~QGH
Assertion gastacos ⊢⊕˙∈GGrpActY∧A∈Y∧B∈X∧C∈X→B∼˙C↔B⊕˙A=C⊕˙A

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