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 = Base G
gasta.2 ⊢ H = u ∈ X | u ⊕ ˙ A = A
Assertion gastacl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → H ∈ SubGrp ⁡ G

Proof

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