Theorem gasubg 16943

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 16934	. . 3 |- ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
2		gasubg.1	. . . 4 |- H = ( G ↾s S )
3	2	subggrp 16807	. . 3 |- ( S e. (SubGrp ` G ) -> H e. Grp )
4	1, 3	anim12ci 569	. 2 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( H e. Grp /\ Y e. _V ) )
5		eqid 2422	. . . . . . 7 |- ( Base ` G ) = ( Base ` G )
6	5	gaf 16936	. . . . . 6 |- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
7	6	adantr 466	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> .(+) : ( ( Base ` G ) X. Y ) --> Y )
8		simpr 462	. . . . . . 7 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S e. (SubGrp ` G ) )
9	5	subgss 16805	. . . . . . 7 |- ( S e. (SubGrp ` G ) -> S C_ ( Base ` G ) )
10	8, 9	syl 17	. . . . . 6 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S C_ ( Base ` G ) )
11		xpss1 4958	. . . . . 6 |- ( S C_ ( Base ` G ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
12	10, 11	syl 17	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( S X. Y ) C_ ( ( Base ` G ) X. Y ) )
13	7, 12	fssresd 5763	. . . 4 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( S X. Y ) --> Y )
14	2	subgbas 16808	. . . . . . 7 |- ( S e. (SubGrp ` G ) -> S = ( Base ` H ) )
15	8, 14	syl 17	. . . . . 6 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> S = ( Base ` H ) )
16	15	xpeq1d 4872	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( S X. Y ) = ( ( Base ` H ) X. Y ) )
17	16	feq2d 5729	. . . 4 |- ( ( .(+) 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 213	. . 3 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) : ( ( Base ` H ) X. Y ) --> Y )
19	8	adantr 466	. . . . . . . 8 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> S e. (SubGrp ` G ) )
20		eqid 2422	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
21	20	subg0cl 16812	. . . . . . . 8 |- ( S e. (SubGrp ` G ) -> ( 0g ` G ) e. S )
22	19, 21	syl 17	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) e. S )
23		simpr 462	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> x e. Y )
24		ovres 6446	. . . . . . 7 |- ( ( ( 0g ` G ) e. S /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
25	22, 23, 24	syl2anc 665	. . . . . 6 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) ( .(+) |` ( S X. Y ) ) x ) = ( ( 0g ` G ) .(+) x ) )
26	2, 20	subg0 16810	. . . . . . . 8 |- ( S e. (SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
27	19, 26	syl 17	. . . . . . 7 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( 0g ` G ) = ( 0g ` H ) )
28	27	oveq1d 6316	. . . . . 6 |- ( ( ( .(+) 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 16935	. . . . . . 7 |- ( ( .(+) e. ( G GrpAct Y ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
30	29	adantlr 719	. . . . . 6 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` G ) .(+) x ) = x )
31	25, 28, 30	3eqtr3d 2471	. . . . 5 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x )
32		eqimss2 3517	. . . . . . . . . . 11 |- ( S = ( Base ` H ) -> ( Base ` H ) C_ S )
33	15, 32	syl 17	. . . . . . . . . 10 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( Base ` H ) C_ S )
34	33	adantr 466	. . . . . . . . 9 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( Base ` H ) C_ S )
35	34	sselda 3464	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ y e. ( Base ` H ) ) -> y e. S )
36	34	sselda 3464	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ z e. ( Base ` H ) ) -> z e. S )
37	35, 36	anim12dan 845	. . . . . . 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 ) )
38		simprl 762	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. S )
39	7	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( ( .(+) 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 735	. . . . . . . . . . . 12 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> S C_ ( Base ` G ) )
41		simprr 764	. . . . . . . . . . . 12 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. S )
42	40, 41	sseldd 3465	. . . . . . . . . . 11 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> z e. ( Base ` G ) )
43	23	adantr 466	. . . . . . . . . . 11 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> x e. Y )
44	39, 42, 43	fovrnd 6451	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z .(+) x ) e. Y )
45		ovres 6446	. . . . . . . . . 10 |- ( ( y e. S /\ ( z .(+) x ) e. Y ) -> ( y ( .(+) |` ( S X. Y ) ) ( z .(+) x ) ) = ( y .(+) ( z .(+) x ) ) )
46	38, 44, 45	syl2anc 665	. . . . . . . . 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 ) ) )
47		ovres 6446	. . . . . . . . . . 11 |- ( ( z e. S /\ x e. Y ) -> ( z ( .(+) |` ( S X. Y ) ) x ) = ( z .(+) x ) )
48	41, 43, 47	syl2anc 665	. . . . . . . . . 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 ) )
49	48	oveq2d 6317	. . . . . . . . 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 ) ) )
50		simplll 766	. . . . . . . . . 10 |- ( ( ( ( .(+) 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 3465	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. ( Base ` G ) )
52		eqid 2422	. . . . . . . . . . 11 |- ( +g ` G ) = ( +g ` G )
53	5, 52	gaass 16938	. . . . . . . . . 10 |- ( ( .(+) 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 1266	. . . . . . . . 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 ) ) )
55	46, 49, 54	3eqtr4d 2473	. . . . . . . 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 ) )
56	52	subgcl 16814	. . . . . . . . . . 11 |- ( ( S e. (SubGrp ` G ) /\ y e. S /\ z e. S ) -> ( y ( +g ` G ) z ) e. S )
57	56	3expb 1206	. . . . . . . . . 10 |- ( ( S e. (SubGrp ` G ) /\ ( y e. S /\ z e. S ) ) -> ( y ( +g ` G ) z ) e. S )
58	19, 57	sylan 473	. . . . . . . . 9 |- ( ( ( ( .(+) 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 6446	. . . . . . . . 9 |- ( ( ( 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 665	. . . . . . . 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 ) )
61	2, 52	ressplusg 15226	. . . . . . . . . . 11 |- ( S e. (SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
62	61	ad3antlr 735	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( +g ` G ) = ( +g ` H ) )
63	62	oveqd 6318	. . . . . . . . 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 ) )
64	63	oveq1d 6316	. . . . . . . 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 ) )
65	55, 60, 64	3eqtr2rd 2470	. . . . . . 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 ) ) )
66	37, 65	syldan 472	. . . . . 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 ) ) )
67	66	ralrimivva 2846	. . . . 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 ) ) )
68	31, 67	jca 534	. . . 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 ) ) ) )
69	68	ralrimiva 2839	. . 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 ) ) ) )
70	18, 69	jca 534	. 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 ) ) ) ) )
71		eqid 2422	. . 3 |- ( Base ` H ) = ( Base ` H )
72		eqid 2422	. . 3 |- ( +g ` H ) = ( +g ` H )
73		eqid 2422	. . 3 |- ( 0g ` H ) = ( 0g ` H )
74	71, 72, 73	isga 16932	. 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 ) ) ) ) ) )
75	4, 70, 74	sylanbrc 668	1 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   _Vcvv 3081   C_ wss 3436   X. cxp 4847   |` cres 4851   -->wf 5593   ` cfv 5597  (class class class)co 6301   Basecbs 15108   ↾_s cress 15109   +g cplusg 15177   0gc0g 15325   Grpcgrp 16656  SubGrpcsubg 16798   GrpAct cga 16930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-map 7478  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-ress 15115  df-plusg 15190  df-0g 15327  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-grp 16660  df-subg 16801  df-ga 16931

This theorem is referenced by:  sylow3lem5  17270