Metamath Proof Explorer

Theorem gastacl

Description: The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses gasta.1 ⊢X=BaseG
gasta.2 ⊢H=u∈X|u⊕˙A=A
Assertion gastacl ⊢⊕˙∈GGrpActY∧A∈Y→H∈SubGrp⁡G

Proof

Step Hyp Ref Expression
1 gasta.1 ⊢X=BaseG
2 gasta.2 ⊢H=u∈X|u⊕˙A=A
3 2 ssrab3 ⊢H⊆X
4 3 a1i ⊢⊕˙∈GGrpActY∧A∈Y→H⊆X
5 gagrp ⊢⊕˙∈GGrpActY→G∈Grp
6 5 adantr ⊢⊕˙∈GGrpActY∧A∈Y→G∈Grp
7 eqid ⊢0G=0G
8 1 7 grpidcl ⊢G∈Grp→0G∈X
9 6 8 syl ⊢⊕˙∈GGrpActY∧A∈Y→0G∈X
10 7 gagrpid ⊢⊕˙∈GGrpActY∧A∈Y→0G⊕˙A=A
11 oveq1 ⊢u=0G→u⊕˙A=0G⊕˙A
12 11 eqeq1d ⊢u=0G→u⊕˙A=A↔0G⊕˙A=A
13 12 2 elrab2 ⊢0G∈H↔0G∈X∧0G⊕˙A=A
14 9 10 13 sylanbrc ⊢⊕˙∈GGrpActY∧A∈Y→0G∈H
15 14 ne0d ⊢⊕˙∈GGrpActY∧A∈Y→H≠∅
16 simpll ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→⊕˙∈GGrpActY
17 16 5 syl ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→G∈Grp
18 simpr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→x∈H
19 oveq1 ⊢u=x→u⊕˙A=x⊕˙A
20 19 eqeq1d ⊢u=x→u⊕˙A=A↔x⊕˙A=A
21 20 2 elrab2 ⊢x∈H↔x∈X∧x⊕˙A=A
22 18 21 sylib ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→x∈X∧x⊕˙A=A
23 22 simpld ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→x∈X
24 23 adantrr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x∈X
25 simprr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→y∈H
26 oveq1 ⊢u=y→u⊕˙A=y⊕˙A
27 26 eqeq1d ⊢u=y→u⊕˙A=A↔y⊕˙A=A
28 27 2 elrab2 ⊢y∈H↔y∈X∧y⊕˙A=A
29 25 28 sylib ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→y∈X∧y⊕˙A=A
30 29 simpld ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→y∈X
31 eqid ⊢+G=+G
32 1 31 grpcl ⊢G∈Grp∧x∈X∧y∈X→x+Gy∈X
33 17 24 30 32 syl3anc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x+Gy∈X
34 simplr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→A∈Y
35 1 31 gaass ⊢⊕˙∈GGrpActY∧x∈X∧y∈X∧A∈Y→x+Gy⊕˙A=x⊕˙y⊕˙A
36 16 24 30 34 35 syl13anc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x+Gy⊕˙A=x⊕˙y⊕˙A
37 29 simprd ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→y⊕˙A=A
38 37 oveq2d ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x⊕˙y⊕˙A=x⊕˙A
39 22 simprd ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→x⊕˙A=A
40 39 adantrr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x⊕˙A=A
41 36 38 40 3eqtrd ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x+Gy⊕˙A=A
42 oveq1 ⊢u=x+Gy→u⊕˙A=x+Gy⊕˙A
43 42 eqeq1d ⊢u=x+Gy→u⊕˙A=A↔x+Gy⊕˙A=A
44 43 2 elrab2 ⊢x+Gy∈H↔x+Gy∈X∧x+Gy⊕˙A=A
45 33 41 44 sylanbrc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x+Gy∈H
46 45 anassrs ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H∧y∈H→x+Gy∈H
47 46 ralrimiva ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→∀y∈Hx+Gy∈H
48 simpll ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→⊕˙∈GGrpActY
49 48 5 syl ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→G∈Grp
50 eqid ⊢invg⁡G=invg⁡G
51 1 50 grpinvcl ⊢G∈Grp∧x∈X→invg⁡G⁡x∈X
52 49 23 51 syl2anc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→invg⁡G⁡x∈X
53 simplr ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→A∈Y
54 1 50 gacan ⊢⊕˙∈GGrpActY∧x∈X∧A∈Y∧A∈Y→x⊕˙A=A↔invg⁡G⁡x⊕˙A=A
55 48 23 53 53 54 syl13anc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→x⊕˙A=A↔invg⁡G⁡x⊕˙A=A
56 39 55 mpbid ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→invg⁡G⁡x⊕˙A=A
57 oveq1 ⊢u=invg⁡G⁡x→u⊕˙A=invg⁡G⁡x⊕˙A
58 57 eqeq1d ⊢u=invg⁡G⁡x→u⊕˙A=A↔invg⁡G⁡x⊕˙A=A
59 58 2 elrab2 ⊢invg⁡G⁡x∈H↔invg⁡G⁡x∈X∧invg⁡G⁡x⊕˙A=A
60 52 56 59 sylanbrc ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→invg⁡G⁡x∈H
61 47 60 jca ⊢⊕˙∈GGrpActY∧A∈Y∧x∈H→∀y∈Hx+Gy∈H∧invg⁡G⁡x∈H
62 61 ralrimiva ⊢⊕˙∈GGrpActY∧A∈Y→∀x∈H∀y∈Hx+Gy∈H∧invg⁡G⁡x∈H
63 1 31 50 issubg2 ⊢G∈Grp→H∈SubGrp⁡G↔H⊆X∧H≠∅∧∀x∈H∀y∈Hx+Gy∈H∧invg⁡G⁡x∈H
64 6 63 syl ⊢⊕˙∈GGrpActY∧A∈Y→H∈SubGrp⁡G↔H⊆X∧H≠∅∧∀x∈H∀y∈Hx+Gy∈H∧invg⁡G⁡x∈H
65 4 15 62 64 mpbir3and ⊢⊕˙∈GGrpActY∧A∈Y→H∈SubGrp⁡G