This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 oveq1 
 |-  ( u = x -> ( u .(+) A ) = ( x .(+) A ) )
19 18 eqeq1d 
 |-  ( u = x -> ( ( u .(+) A ) = A <-> ( x .(+) A ) = A ) )
20 19 2 elrab2 
 |-  ( x e. H <-> ( x e. X /\ ( x .(+) A ) = A ) )
21 20 bilani 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( x e. X /\ ( x .(+) A ) = A ) )
22 21 simpld 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> x e. X )
23 22 adantrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> x e. X )
24 simprr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> y e. 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 e. H <-> ( y e. X /\ ( y .(+) A ) = A ) )
28 24 27 sylib 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( y e. X /\ ( y .(+) A ) = A ) )
29 28 simpld 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> y e. X )
30 eqid 
 |-  ( +g ` G ) = ( +g ` G )
31 1 30 grpcl 
 |-  ( ( G e. Grp /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) y ) e. X )
32 17 23 29 31 syl3anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x ( +g ` G ) y ) e. X )
33 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> A e. Y )
34 1 30 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( x e. X /\ y e. X /\ A e. Y ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = ( x .(+) ( y .(+) A ) ) )
35 16 23 29 33 34 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = ( x .(+) ( y .(+) A ) ) )
36 28 simprd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( y .(+) A ) = A )
37 36 oveq2d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x .(+) ( y .(+) A ) ) = ( x .(+) A ) )
38 21 simprd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( x .(+) A ) = A )
39 38 adantrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x .(+) A ) = A )
40 35 37 39 3eqtrd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( ( x ( +g ` G ) y ) .(+) A ) = A )
41 oveq1 
 |-  ( u = ( x ( +g ` G ) y ) -> ( u .(+) A ) = ( ( x ( +g ` G ) y ) .(+) A ) )
42 41 eqeq1d 
 |-  ( u = ( x ( +g ` G ) y ) -> ( ( u .(+) A ) = A <-> ( ( x ( +g ` G ) y ) .(+) A ) = A ) )
43 42 2 elrab2 
 |-  ( ( x ( +g ` G ) y ) e. H <-> ( ( x ( +g ` G ) y ) e. X /\ ( ( x ( +g ` G ) y ) .(+) A ) = A ) )
44 32 40 43 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( x e. H /\ y e. H ) ) -> ( x ( +g ` G ) y ) e. H )
45 44 anassrs 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) /\ y e. H ) -> ( x ( +g ` G ) y ) e. H )
46 45 ralrimiva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> A. y e. H ( x ( +g ` G ) y ) e. H )
47 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> .(+) e. ( G GrpAct Y ) )
48 47 5 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> G e. Grp )
49 eqid 
 |-  ( invg ` G ) = ( invg ` G )
50 1 49 grpinvcl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( invg ` G ) ` x ) e. X )
51 48 22 50 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( invg ` G ) ` x ) e. X )
52 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> A e. Y )
53 1 49 gacan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( x e. X /\ A e. Y /\ A e. Y ) ) -> ( ( x .(+) A ) = A <-> ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
54 47 22 52 52 53 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( x .(+) A ) = A <-> ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
55 38 54 mpbid 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( ( invg ` G ) ` x ) .(+) A ) = A )
56 oveq1 
 |-  ( u = ( ( invg ` G ) ` x ) -> ( u .(+) A ) = ( ( ( invg ` G ) ` x ) .(+) A ) )
57 56 eqeq1d 
 |-  ( u = ( ( invg ` G ) ` x ) -> ( ( u .(+) A ) = A <-> ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
58 57 2 elrab2 
 |-  ( ( ( invg ` G ) ` x ) e. H <-> ( ( ( invg ` G ) ` x ) e. X /\ ( ( ( invg ` G ) ` x ) .(+) A ) = A ) )
59 51 55 58 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ x e. H ) -> ( ( invg ` G ) ` x ) e. H )
60 46 59 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 ) )
61 60 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 ) )
62 1 30 49 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 ) ) ) )
63 6 62 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 ) ) ) )
64 4 15 61 63 mpbir3and 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )