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 simpr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → x ∈ X ∧ x ⊕ ˙ A = A
23 22 simpld ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → x ∈ X
24 23 adantrr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x ∈ X
25 simprr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → y ∈ X ∧ y ⊕ ˙ A = A
30 29 simpld ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → y ∈ X
31 eqid ⊢ + G = + G
32 1 31 grpcl ⊢ G ∈ Grp ∧ x ∈ X ∧ y ∈ X → x + G y ∈ X
33 17 24 30 32 syl3anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x + G y ∈ X
34 simplr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → A ∈ Y
35 1 31 gaass ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X ∧ y ∈ X ∧ A ∈ Y → x + G y ⊕ ˙ A = x ⊕ ˙ y ⊕ ˙ A
36 16 24 30 34 35 syl13anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x + G y ⊕ ˙ A = x ⊕ ˙ y ⊕ ˙ A
37 29 simprd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → y ⊕ ˙ A = A
38 37 oveq2d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x ⊕ ˙ y ⊕ ˙ A = x ⊕ ˙ A
39 22 simprd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → x ⊕ ˙ A = A
40 39 adantrr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x ⊕ ˙ A = A
41 36 38 40 3eqtrd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x + G y ⊕ ˙ A = A
42 oveq1 ⊢ u = x + G y → u ⊕ ˙ A = x + G y ⊕ ˙ A
43 42 eqeq1d ⊢ u = x + G y → u ⊕ ˙ A = A ↔ x + G y ⊕ ˙ A = A
44 43 2 elrab2 ⊢ x + G y ∈ H ↔ x + G y ∈ X ∧ x + G y ⊕ ˙ A = A
45 33 41 44 sylanbrc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x + G y ∈ H
46 45 anassrs ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H ∧ y ∈ H → x + G y ∈ H
47 46 ralrimiva ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → ∀ y ∈ H x + G y ∈ H
48 simpll ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → ⊕ ˙ ∈ G GrpAct Y
49 48 5 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → G ∈ Grp
50 eqid ⊢ inv g ⁡ G = inv g ⁡ G
51 1 50 grpinvcl ⊢ G ∈ Grp ∧ x ∈ X → inv g ⁡ G ⁡ x ∈ X
52 49 23 51 syl2anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → inv g ⁡ G ⁡ x ∈ X
53 simplr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → A ∈ Y
54 1 50 gacan ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X ∧ A ∈ Y ∧ A ∈ Y → x ⊕ ˙ A = A ↔ inv g ⁡ G ⁡ x ⊕ ˙ A = A
55 48 23 53 53 54 syl13anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → x ⊕ ˙ A = A ↔ inv g ⁡ G ⁡ x ⊕ ˙ A = A
56 39 55 mpbid ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → inv g ⁡ G ⁡ x ⊕ ˙ A = A
57 oveq1 ⊢ u = inv g ⁡ G ⁡ x → u ⊕ ˙ A = inv g ⁡ G ⁡ x ⊕ ˙ A
58 57 eqeq1d ⊢ u = inv g ⁡ G ⁡ x → u ⊕ ˙ A = A ↔ inv g ⁡ G ⁡ x ⊕ ˙ A = A
59 58 2 elrab2 ⊢ inv g ⁡ G ⁡ x ∈ H ↔ inv g ⁡ G ⁡ x ∈ X ∧ inv g ⁡ G ⁡ x ⊕ ˙ A = A
60 52 56 59 sylanbrc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → inv g ⁡ G ⁡ x ∈ H
61 47 60 jca ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y ∧ x ∈ H → ∀ y ∈ H x + G y ∈ H ∧ inv g ⁡ G ⁡ x ∈ H
62 61 ralrimiva ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → ∀ x ∈ H ∀ y ∈ H x + G y ∈ H ∧ inv g ⁡ G ⁡ x ∈ H
63 1 31 50 issubg2 ⊢ G ∈ Grp → H ∈ SubGrp ⁡ G ↔ H ⊆ X ∧ H ≠ ∅ ∧ ∀ x ∈ H ∀ y ∈ H x + G y ∈ H ∧ inv g ⁡ G ⁡ x ∈ H
64 6 63 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
65 4 15 62 64 mpbir3and ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → H ∈ SubGrp ⁡ G