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 oveq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ⊕ 𝐴 ) = ( 𝑥 ⊕ 𝐴 ) )
19 18 eqeq1d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ⊕ 𝐴 ) = 𝐴 ↔ ( 𝑥 ⊕ 𝐴 ) = 𝐴 ) )
20 19 2 elrab2 ⊢ ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ⊕ 𝐴 ) = 𝐴 ) )
21 20 bilani ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ⊕ 𝐴 ) = 𝐴 ) )
22 21 simpld ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ 𝑋 )
23 22 adantrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → 𝑥 ∈ 𝑋 )
24 simprr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → 𝑦 ∈ 𝐻 )
25 oveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 ⊕ 𝐴 ) = ( 𝑦 ⊕ 𝐴 ) )
26 25 eqeq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 ⊕ 𝐴 ) = 𝐴 ↔ ( 𝑦 ⊕ 𝐴 ) = 𝐴 ) )
27 26 2 elrab2 ⊢ ( 𝑦 ∈ 𝐻 ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ⊕ 𝐴 ) = 𝐴 ) )
28 24 27 sylib ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ⊕ 𝐴 ) = 𝐴 ) )
29 28 simpld ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → 𝑦 ∈ 𝑋 )
30 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
31 1 30 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
32 17 23 29 31 syl3anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
33 simplr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → 𝐴 ∈ 𝑌 )
34 1 30 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) = ( 𝑥 ⊕ ( 𝑦 ⊕ 𝐴 ) ) )
35 16 23 29 33 34 syl13anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) = ( 𝑥 ⊕ ( 𝑦 ⊕ 𝐴 ) ) )
36 28 simprd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑦 ⊕ 𝐴 ) = 𝐴 )
37 36 oveq2d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ⊕ ( 𝑦 ⊕ 𝐴 ) ) = ( 𝑥 ⊕ 𝐴 ) )
38 21 simprd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( 𝑥 ⊕ 𝐴 ) = 𝐴 )
39 38 adantrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ⊕ 𝐴 ) = 𝐴 )
40 35 37 39 3eqtrd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) = 𝐴 )
41 oveq1 ⊢ ( 𝑢 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( 𝑢 ⊕ 𝐴 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) )
42 41 eqeq1d ⊢ ( 𝑢 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( ( 𝑢 ⊕ 𝐴 ) = 𝐴 ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) = 𝐴 ) )
43 42 2 elrab2 ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 ∧ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ⊕ 𝐴 ) = 𝐴 ) )
44 32 40 43 sylanbrc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 )
45 44 anassrs ⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 )
46 45 ralrimiva ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 )
47 simpll ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
48 47 5 syl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → 𝐺 ∈ Grp )
49 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
50 1 49 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑋 )
51 48 22 50 syl2anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑋 )
52 simplr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → 𝐴 ∈ 𝑌 )
53 1 49 gacan ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ∧ 𝐴 ∈ 𝑌 ) ) → ( ( 𝑥 ⊕ 𝐴 ) = 𝐴 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) = 𝐴 ) )
54 47 22 52 52 53 syl13anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑥 ⊕ 𝐴 ) = 𝐴 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) = 𝐴 ) )
55 38 54 mpbid ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) = 𝐴 )
56 oveq1 ⊢ ( 𝑢 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑢 ⊕ 𝐴 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) )
57 56 eqeq1d ⊢ ( 𝑢 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( 𝑢 ⊕ 𝐴 ) = 𝐴 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) = 𝐴 ) )
58 57 2 elrab2 ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ⊕ 𝐴 ) = 𝐴 ) )
59 51 55 58 sylanbrc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 )
60 46 59 jca ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝐻 ) → ( ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) )
61 60 ralrimiva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝐻 ( ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) )
62 1 30 49 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐻 ⊆ 𝑋 ∧ 𝐻 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐻 ( ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) ) ) )
63 6 62 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐻 ⊆ 𝑋 ∧ 𝐻 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐻 ( ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐻 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) ) ) )
64 4 15 61 63 mpbir3and ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )