Metamath Proof Explorer

Theorem gasubg

Description: The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypothesis gasubg.1 
|- H = ( G |`s S )
Assertion gasubg 
|- ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) )

Proof

Step Hyp Ref Expression
1 gasubg.1 
 |-  H = ( G |`s S )
2 gaset 
 |-  ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
3 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
4 2 3 anim12ci 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( H e. Grp /\ Y e. _V ) )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
7 6 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
8 simpr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> S e. ( SubGrp ` G ) )
9 5 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
10 8 9 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> S C_ ( Base ` G ) )
11 xpss1 
 |-  ( S C_ ( Base ` G ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
12 10 11 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
13 7 12 fssresd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y )
14 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
15 8 14 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> S = ( Base ` H ) )
16 15 xpeq1d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( S X. Y ) = ( ( Base ` H ) X. Y ) )
17 16 feq2d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y <-> ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y ) )
18 13 17 mpbid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y )
19 8 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> S e. ( SubGrp ` G ) )
20 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
21 20 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
22 19 21 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) e. S )
23 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> x e. Y )
24 ovres 
 |-  ( ( ( 0g ` G ) e. S /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
25 22 23 24 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
26 1 20 subg0 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
27 19 26 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) = ( 0g ` H ) )
28 27 oveq1d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) )
29 20 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
30 29 adantlr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
31 25 28 30 3eqtr3d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x )
32 eqimss2 
 |-  ( S = ( Base ` H ) -> ( Base ` H ) C_ S )
33 15 32 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( Base ` H ) C_ S )
34 33 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( Base ` H ) C_ S )
35 34 sselda 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ y e. ( Base ` H ) ) -> y e. S )
36 34 sselda 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ z e. ( Base ` H ) ) -> z e. S )
37 35 36 anim12dan 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. ( Base ` H ) /\ z e. ( Base ` H ) ) ) -> ( y e. S /\ z e. S ) )
38 simprl 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. S )
39 7 ad2antrr 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
40 9 ad3antlr 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> S C_ ( Base ` G ) )
41 simprr 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. S )
42 40 41 sseldd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. ( Base ` G ) )
43 23 adantr 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> x e. Y )
44 39 42 43 fovcdmd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z .(+) x ) e. Y )
45 ovres 
 |-  ( ( y e. S /\ ( z .(+) x ) e. Y ) -> ( y ( .(+) |` ( S X. Y ) ) ( z .(+) x ) ) = ( y .(+) ( z .(+) x ) ) )
46 38 44 45 syl2anc 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( .(+) |` ( S X. Y ) ) ( z .(+) x ) ) = ( y .(+) ( z .(+) x ) ) )
47 ovres 
 |-  ( ( z e. S /\ x e. Y ) -> ( z ( .(+) |` ( S X. Y ) ) x ) = ( z .(+) x ) )
48 41 43 47 syl2anc 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z ( .(+) |` ( S X. Y ) ) x ) = ( z .(+) x ) )
49 48 oveq2d 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) = ( y ( .(+) |` ( S X. Y ) ) ( z .(+) x ) ) )
50 simplll 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> .(+) e. ( G GrpAct Y ) )
51 40 38 sseldd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. ( Base ` G ) )
52 eqid 
 |-  ( +g ` G ) = ( +g ` G )
53 5 52 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) /\ x e. Y ) ) -> ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
54 50 51 42 43 53 syl13anc 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
55 46 49 54 3eqtr4d 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) = ( ( y ( +g ` G ) z ) .(+) x ) )
56 52 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ y e. S /\ z e. S ) -> ( y ( +g ` G ) z ) e. S )
57 56 3expb 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) e. S )
58 19 57 sylan 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) e. S )
59 ovres 
 |-  ( ( ( y ( +g ` G ) z ) e. S /\ x e. Y ) -> ( ( y ( +g ` G ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( ( y ( +g ` G ) z ) .(+) x ) )
60 58 43 59 syl2anc 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( ( y ( +g ` G ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( ( y ( +g ` G ) z ) .(+) x ) )
61 1 52 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
62 61 ad3antlr 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( +g ` G ) = ( +g ` H ) )
63 62 oveqd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) = ( y ( +g ` H ) z ) )
64 63 oveq1d 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( ( y ( +g ` G ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) )
65 55 60 64 3eqtr2rd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) )
66 37 65 syldan 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. ( Base ` H ) /\ z e. ( Base ` H ) ) ) -> ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) )
67 66 ralrimivva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> A. y e. ( Base ` H ) A. z e. ( Base ` H ) ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) )
68 31 67 jca 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) /\ x e. Y ) -> ( ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x /\ A. y e. ( Base ` H ) A. z e. ( Base ` H ) ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) ) )
69 68 ralrimiva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> A. x e. Y ( ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x /\ A. y e. ( Base ` H ) A. z e. ( Base ` H ) ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) ) )
70 18 69 jca 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x /\ A. y e. ( Base ` H ) A. z e. ( Base ` H ) ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) ) ) )
71 eqid 
 |-  ( Base ` H ) = ( Base ` H )
72 eqid 
 |-  ( +g ` H ) = ( +g ` H )
73 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
74 71 72 73 isga 
 |-  ( ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) <-> ( ( H e. Grp /\ Y e. _V ) /\ ( ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x /\ A. y e. ( Base ` H ) A. z e. ( Base ` H ) ( ( y ( +g ` H ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( y ( .(+) |` ( S X. Y ) ) ( z ( .(+) |` ( S X. Y ) ) x ) ) ) ) ) )
75 4 70 74 sylanbrc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ S e. ( SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) )