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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gasta.2 ⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
Assertion gastacl ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

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