Theorem gasubg 15819

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

Hypothesis

Ref	Expression
gasubg.1	|- H = ( G ↾s S )

Assertion

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

Proof of Theorem gasubg

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gaset 15810	. . 3 |- ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
2		gasubg.1	. . . 4 |- H = ( G ↾s S )
3	2	subggrp 15683	. . 3 |- ( S e. (SubGrp ` G ) -> H e. Grp )
4	1, 3	anim12ci 567	. 2 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( H e. Grp /\ Y e. _V ) )
5		eqid 2442	. . . . . . 7 |- ( Base ` G ) = ( Base ` G )
6	5	gaf 15812	. . . . . 6 |- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
7	6	adantr 465	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
8		simpr 461	. . . . . . 7 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S e. (SubGrp ` G ) )
9	5	subgss 15681	. . . . . . 7 |- ( S e. (SubGrp ` G ) -> S C_ ( Base ` G ) )
10	8, 9	syl 16	. . . . . 6 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S C_ ( Base ` G ) )
11		xpss1 4947	. . . . . 6 |- ( S C_ ( Base ` G ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
12	10, 11	syl 16	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
13		fssres 5577	. . . . 5 |- ( ( .(+) : ( ( Base ` G ) X. Y ) --> Y /\ ( S X. Y ) C_ ( ( Base ` G ) X. Y ) ) -> ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y )
14	7, 12, 13	syl2anc 661	. . . 4 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y )
15	2	subgbas 15684	. . . . . . 7 |- ( S e. (SubGrp ` G ) -> S = ( Base ` H ) )
16	8, 15	syl 16	. . . . . 6 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S = ( Base ` H ) )
17	16	xpeq1d 4862	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( S X. Y ) = ( ( Base ` H ) X. Y ) )
18	17	feq2d 5546	. . . 4 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y <-> ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y ) )
19	14, 18	mpbid 210	. . 3 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y )
20	8	adantr 465	. . . . . . . 8 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> S e. (SubGrp ` G ) )
21		eqid 2442	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
22	21	subg0cl 15688	. . . . . . . 8 |- ( S e. (SubGrp ` G ) -> ( 0g ` G ) e. S )
23	20, 22	syl 16	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) e. S )
24		simpr 461	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> x e. Y )
25		ovres 6229	. . . . . . 7 |- ( ( ( 0g ` G ) e. S /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
26	23, 24, 25	syl2anc 661	. . . . . 6 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
27	2, 21	subg0 15686	. . . . . . . 8 |- ( S e. (SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
28	20, 27	syl 16	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) = ( 0g ` H ) )
29	28	oveq1d 6105	. . . . . 6 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) )
30	21	gagrpid 15811	. . . . . . 7 |- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
31	30	adantlr 714	. . . . . 6 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
32	26, 29, 31	3eqtr3d 2482	. . . . 5 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x )
33		eqimss2 3408	. . . . . . . . . . 11 |- ( S = ( Base ` H ) -> ( Base ` H ) C_ S )
34	16, 33	syl 16	. . . . . . . . . 10 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( Base ` H ) C_ S )
35	34	adantr 465	. . . . . . . . 9 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( Base ` H ) C_ S )
36	35	sselda 3355	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ y e. ( Base ` H ) ) -> y e. S )
37	35	sselda 3355	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ z e. ( Base ` H ) ) -> z e. S )
38	36, 37	anim12dan 833	. . . . . . 7 |- ( ( ( ( .(+) 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 ) )
39		simprl 755	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. S )
40	7	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
41	9	ad3antlr 730	. . . . . . . . . . . 12 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> S C_ ( Base ` G ) )
42		simprr 756	. . . . . . . . . . . 12 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. S )
43	41, 42	sseldd 3356	. . . . . . . . . . 11 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. ( Base ` G ) )
44	24	adantr 465	. . . . . . . . . . 11 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> x e. Y )
45	40, 43, 44	fovrnd 6234	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z .(+) x ) e. Y )
46		ovres 6229	. . . . . . . . . 10 |- ( ( y e. S /\ ( z .(+) x ) e. Y ) -> ( y ( .(+) |` ( S X. Y ) ) ( z .(+) x ) ) = ( y .(+) ( z .(+) x ) ) )
47	39, 45, 46	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( .(+) 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 ) ) )
48		ovres 6229	. . . . . . . . . . 11 |- ( ( z e. S /\ x e. Y ) -> ( z ( .(+) |` ( S X. Y ) ) x ) = ( z .(+) x ) )
49	42, 44, 48	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z ( .(+) |` ( S X. Y ) ) x ) = ( z .(+) x ) )
50	49	oveq2d 6106	. . . . . . . . 9 |- ( ( ( ( .(+) 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 ) ) )
51		simplll 757	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> .(+) e. ( G GrpAct Y ) )
52	41, 39	sseldd 3356	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. ( Base ` G ) )
53		eqid 2442	. . . . . . . . . . 11 |- ( +g ` G ) = ( +g ` G )
54	5, 53	gaass 15814	. . . . . . . . . 10 |- ( ( .(+) e. ( G GrpAct Y ) /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) /\ x e. Y ) ) -> ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
55	51, 52, 43, 44, 54	syl13anc 1220	. . . . . . . . 9 |- ( ( ( ( .(+) 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 ) ) )
56	47, 50, 55	3eqtr4d 2484	. . . . . . . 8 |- ( ( ( ( .(+) 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 ) )
57	53	subgcl 15690	. . . . . . . . . . 11 |- ( ( S e. (SubGrp ` G ) /\ y e. S /\ z e. S ) -> ( y ( +g ` G ) z ) e. S )
58	57	3expb 1188	. . . . . . . . . 10 |- ( ( S e. (SubGrp ` G ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) e. S )
59	20, 58	sylan 471	. . . . . . . . 9 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) e. S )
60		ovres 6229	. . . . . . . . 9 |- ( ( ( y ( +g ` G ) z ) e. S /\ x e. Y ) -> ( ( y ( +g ` G ) z ) ( .(+) |` ( S X. Y ) ) x ) = ( ( y ( +g ` G ) z ) .(+) x ) )
61	59, 44, 60	syl2anc 661	. . . . . . . 8 |- ( ( ( ( .(+) 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 ) )
62	2, 53	ressplusg 14279	. . . . . . . . . . 11 |- ( S e. (SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
63	62	ad3antlr 730	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( +g ` G ) = ( +g ` H ) )
64	63	oveqd 6107	. . . . . . . . 9 |- ( ( ( ( .(+) 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 ) )
65	64	oveq1d 6105	. . . . . . . 8 |- ( ( ( ( .(+) 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 ) )
66	56, 61, 65	3eqtr2rd 2481	. . . . . . 7 |- ( ( ( ( .(+) 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 ) ) )
67	38, 66	syldan 470	. . . . . 6 |- ( ( ( ( .(+) 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 ) ) )
68	67	ralrimivva 2807	. . . . 5 |- ( ( ( .(+) 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 ) ) )
69	32, 68	jca 532	. . . 4 |- ( ( ( .(+) 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 ) ) ) )
70	69	ralrimiva 2798	. . 3 |- ( ( .(+) 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 ) ) ) )
71	19, 70	jca 532	. 2 |- ( ( .(+) 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 ) ) ) ) )
72		eqid 2442	. . 3 |- ( Base ` H ) = ( Base ` H )
73		eqid 2442	. . 3 |- ( +g ` H ) = ( +g ` H )
74		eqid 2442	. . 3 |- ( 0g ` H ) = ( 0g ` H )
75	72, 73, 74	isga 15808	. 2 |- ( ( .(+) |` ( 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 ) ) ) ) ) )
76	4, 71, 75	sylanbrc 664	1 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2714   _Vcvv 2971   C_ wss 3327   X. cxp 4837   |` cres 4841   -->wf 5413   ` cfv 5417  (class class class)co 6090   Basecbs 14173   ↾_s cress 14174   +g cplusg 14237   0gc0g 14377   Grpcgrp 15409  SubGrpcsubg 15674   GrpAct cga 15806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371  ax-cnex 9337  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-addrcl 9342  ax-mulcl 9343  ax-mulrcl 9344  ax-mulcom 9345  ax-addass 9346  ax-mulass 9347  ax-distr 9348  ax-i2m1 9349  ax-1ne0 9350  ax-1rid 9351  ax-rnegex 9352  ax-rrecex 9353  ax-cnre 9354  ax-pre-lttri 9355  ax-pre-lttrn 9356  ax-pre-ltadd 9357  ax-pre-mulgt0 9358

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-iun 4172  df-br 4292  df-opab 4350  df-mpt 4351  df-tr 4385  df-eprel 4631  df-id 4635  df-po 4640  df-so 4641  df-fr 4678  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-riota 6051  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-recs 6831  df-rdg 6865  df-er 7100  df-map 7215  df-en 7310  df-dom 7311  df-sdom 7312  df-pnf 9419  df-mnf 9420  df-xr 9421  df-ltxr 9422  df-le 9423  df-sub 9596  df-neg 9597  df-nn 10322  df-2 10379  df-ndx 14176  df-slot 14177  df-base 14178  df-sets 14179  df-ress 14180  df-plusg 14250  df-0g 14379  df-mnd 15414  df-grp 15544  df-subg 15677  df-ga 15807

This theorem is referenced by:  sylow3lem5  16129