Theorem gasubg 16212

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 16203	. . 3 |- ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
2		gasubg.1	. . . 4 |- H = ( G ↾s S )
3	2	subggrp 16076	. . 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 2467	. . . . . . 7 |- ( Base ` G ) = ( Base ` G )
6	5	gaf 16205	. . . . . 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 16074	. . . . . . 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 5117	. . . . . 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 5757	. . . . 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 16077	. . . . . . 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 5028	. . . . 5 |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( S X. Y ) = ( ( Base ` H ) X. Y ) )
18	17	feq2d 5724	. . . 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 2467	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
22	21	subg0cl 16081	. . . . . . . 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 6437	. . . . . . 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 16079	. . . . . . . 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 6310	. . . . . 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 16204	. . . . . . 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 2516	. . . . 5 |- ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) -> ( ( 0g ` H ) ( .(+) |` ( S X. Y ) ) x ) = x )
33		eqimss2 3562	. . . . . . . . . . 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 3509	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ y e. ( Base ` H ) ) -> y e. S )
37	35	sselda 3509	. . . . . . . 8 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ z e. ( Base ` H ) ) -> z e. S )
38	36, 37	anim12dan 835	. . . . . . 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 3510	. . . . . . . . . . 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 6442	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> ( z .(+) x ) e. Y )
46		ovres 6437	. . . . . . . . . 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 6437	. . . . . . . . . . 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 6311	. . . . . . . . 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 3510	. . . . . . . . . 10 |- ( ( ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) /\ x e. Y ) /\ ( y e. S /\ z e. S ) ) -> y e. ( Base ` G ) )
53		eqid 2467	. . . . . . . . . . 11 |- ( +g ` G ) = ( +g ` G )
54	5, 53	gaass 16207	. . . . . . . . . 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 1230	. . . . . . . . 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 2518	. . . . . . . 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 16083	. . . . . . . . . . 11 |- ( ( S e. (SubGrp ` G ) /\ y e. S /\ z e. S ) -> ( y ( +g ` G ) z ) e. S )
58	57	3expb 1197	. . . . . . . . . 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 6437	. . . . . . . . 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 14614	. . . . . . . . . . 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 6312	. . . . . . . . 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 6310	. . . . . . . 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 2515	. . . . . . 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 2888	. . . . 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 2881	. . 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 2467	. . 3 |- ( Base ` H ) = ( Base ` H )
73		eqid 2467	. . 3 |- ( +g ` H ) = ( +g ` H )
74		eqid 2467	. . 3 |- ( 0g ` H ) = ( 0g ` H )
75	72, 73, 74	isga 16201	. 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 1379   e. wcel 1767   A.wral 2817   _Vcvv 3118   C_ wss 3481   X. cxp 5003   |` cres 5007   -->wf 5590   ` cfv 5594  (class class class)co 6295   Basecbs 14507   ↾_s cress 14508   +g cplusg 14572   0gc0g 14712   Grpcgrp 15925  SubGrpcsubg 16067   GrpAct cga 16199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-recs 7054  df-rdg 7088  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-0g 14714  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-grp 15929  df-subg 16070  df-ga 16200

This theorem is referenced by:  sylow3lem5  16524