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 e. X | ( u .(+) A ) = A }
Assertion gastacl 
|- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 gasta.1 
 |-  X = ( Base ` G )
2 gasta.2 
 |-  H = { u e. X | ( u .(+) A ) = A }
3 2 ssrab3 
 |-  H C_ X
4 3 a1i 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H C_ X )
5 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
6 5 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> G e. Grp )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 7 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
9 6 8 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( 0g ` G ) e. X )
10 7 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( ( 0g ` G ) .(+) A ) = A )
11 oveq1 
 |-  ( u = ( 0g ` G ) -> ( u .(+) A ) = ( ( 0g ` G ) .(+) A ) )
12 11 eqeq1d 
 |-  ( u = ( 0g ` G ) -> ( ( u .(+) A ) = A <-> ( ( 0g ` G ) .(+) A ) = A ) )
13 12 2 elrab2 
 |-  ( ( 0g ` G ) e. H <-> ( ( 0g ` G ) e. X /\ ( ( 0g ` G ) .(+) A ) = A ) )
14 9 10 13 sylanbrc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( 0g ` G ) e. H )
15 14 ne0d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H =/= (/) )
16 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> .(+) e. ( G GrpAct Y ) )
17 16 5 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> G e. Grp )
18 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> x e. 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 e. H <-> ( x e. X /\ ( x .(+) A ) = A ) )
22 18 21 sylib 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( x e. X /\ ( x .(+) A ) = A ) )
23 22 simpld 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> x e. X )
24 23 adantrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> x e. X )
25 simprr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> y e. 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 e. H <-> ( y e. X /\ ( y .(+) A ) = A ) )
29 25 28 sylib 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( y e. X /\ ( y .(+) A ) = A ) )
30 29 simpld 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> y e. X )
31 eqid 
 |-  ( +g ` G ) = ( +g ` G )
32 1 31 grpcl 
 |-  ( ( G e. Grp /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) y ) e. X )
33 17 24 30 32 syl3anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x ( +g ` G ) y ) e. X )
34 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> A e. Y )
35 1 31 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( x e. X /\ y e. X /\ A e. Y ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = ( x .(+) ( y .(+) A ) ) )
36 16 24 30 34 35 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = ( x .(+) ( y .(+) A ) ) )
37 29 simprd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( y .(+) A ) = A )
38 37 oveq2d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x .(+) ( y .(+) A ) ) = ( x .(+) A ) )
39 22 simprd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( x .(+) A ) = A )
40 39 adantrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x .(+) A ) = A )
41 36 38 40 3eqtrd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = A )
42 oveq1 
 |-  ( u = ( x ( +g ` G ) y ) -> ( u .(+) A ) = ( ( x ( +g ` G ) y ) .(+) A ) )
43 42 eqeq1d 
 |-  ( u = ( x ( +g ` G ) y ) -> ( ( u .(+) A ) = A <-> ( ( x ( +g ` G ) y ) .(+) A ) = A ) )
44 43 2 elrab2 
 |-  ( ( x ( +g ` G ) y ) e. H <-> ( ( x ( +g ` G ) y ) e. X /\ ( ( x ( +g ` G ) y ) .(+) A ) = A ) )
45 33 41 44 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x ( +g ` G ) y ) e. H )
46 45 anassrs 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) /\ y e. H ) -> ( x ( +g ` G ) y ) e. H )
47 46 ralrimiva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> A. y e. H ( x ( +g ` G ) y ) e. H )
48 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> .(+) e. ( G GrpAct Y ) )
49 48 5 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> G e. Grp )
50 eqid 
 |-  ( invg ` G ) = ( invg ` G )
51 1 50 grpinvcl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( invg ` G ) ` x ) e. X )
52 49 23 51 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( invg ` G ) ` x ) e. X )
53 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> A e. Y )
54 1 50 gacan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( x e. X /\ A e. Y /\ A e. Y ) ) -> ( ( x .(+) A ) = A <-> ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
55 48 23 53 53 54 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( x .(+) A ) = A <-> ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
56 39 55 mpbid 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. 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 ) e. H <-> ( ( ( invg ` G ) ` x ) e. X /\ ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
60 52 56 59 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( invg ` G ) ` x ) e. H )
61 47 60 jca 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( A. y e. H ( x ( +g ` G ) y ) e. H /\ ( ( invg ` G ) ` x ) e. H ) )
62 61 ralrimiva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> A. x e. H ( A. y e. H ( x ( +g ` G ) y ) e. H /\ ( ( invg ` G ) ` x ) e. H ) )
63 1 31 50 issubg2 
 |-  ( G e. Grp -> ( H e. ( SubGrp ` G ) <-> ( H C_ X /\ H =/= (/) /\ A. x e. H ( A. y e. H ( x ( +g ` G ) y ) e. H /\ ( ( invg ` G ) ` x ) e. H ) ) ) )
64 6 63 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( H e. ( SubGrp ` G ) <-> ( H C_ X /\ H =/= (/) /\ A. x e. H ( A. y e. H ( x ( +g ` G ) y ) e. H /\ ( ( invg ` G ) ` x ) e. H ) ) ) )
65 4 15 62 64 mpbir3and 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )