Theorem sylow3lem1 17272

Description: Lemma for sylow3 17278, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)

Hypotheses

Ref	Expression
sylow3.x	|- X = ( Base ` G )
sylow3.g	|- ( ph -> G e. Grp )
sylow3.xf	|- ( ph -> X e. Fin )
sylow3.p	|- ( ph -> P e. Prime )
sylow3lem1.a	|- .+ = ( +g ` G )
sylow3lem1.d	|- .- = ( -g ` G )
sylow3lem1.m	|- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )

Assertion

Ref	Expression
sylow3lem1	|- ( ph -> .(+) e. ( G GrpAct ( P pSyl G ) ) )

Distinct variable groups:   x, y, z, .-   x, .(+) , y, z   x, X, y, z   x, G, y, z   ph, x, y, z   x, .+ , y, z   x, P, y, z

Proof of Theorem sylow3lem1

Dummy variables a b c u v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow3.g	. . 3 |- ( ph -> G e. Grp )
2		ovex 6316	. . 3 |- ( P pSyl G ) e. _V
3	1, 2	jctir 541	. 2 |- ( ph -> ( G e. Grp /\ ( P pSyl G ) e. _V ) )
4		sylow3.xf	. . . . . . . . . . 11 |- ( ph -> X e. Fin )
5		sylow3.p	. . . . . . . . . . 11 |- ( ph -> P e. Prime )
6		sylow3.x	. . . . . . . . . . . 12 |- X = ( Base ` G )
7	6	fislw 17270	. . . . . . . . . . 11 |- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( y e. ( P pSyl G ) <-> ( y e. (SubGrp ` G ) /\ ( # ` y ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
8	1, 4, 5, 7	syl3anc 1267	. . . . . . . . . 10 |- ( ph -> ( y e. ( P pSyl G ) <-> ( y e. (SubGrp ` G ) /\ ( # ` y ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
9	8	biimpa 487	. . . . . . . . 9 |- ( ( ph /\ y e. ( P pSyl G ) ) -> ( y e. (SubGrp ` G ) /\ ( # ` y ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
10	9	adantrl 721	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( y e. (SubGrp ` G ) /\ ( # ` y ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
11	10	simpld 461	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> y e. (SubGrp ` G ) )
12		simprl 763	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> x e. X )
13		sylow3lem1.a	. . . . . . . 8 |- .+ = ( +g ` G )
14		sylow3lem1.d	. . . . . . . 8 |- .- = ( -g ` G )
15		eqid 2450	. . . . . . . 8 |- ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. y |-> ( ( x .+ z ) .- x ) )
16	6, 13, 14, 15	conjsubg 16907	. . . . . . 7 |- ( ( y e. (SubGrp ` G ) /\ x e. X ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) )
17	11, 12, 16	syl2anc 666	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) )
18	6, 13, 14, 15	conjsubgen 16908	. . . . . . . . 9 |- ( ( y e. (SubGrp ` G ) /\ x e. X ) -> y ~~ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
19	11, 12, 18	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> y ~~ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
20	4	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> X e. Fin )
21	6	subgss 16811	. . . . . . . . . . 11 |- ( y e. (SubGrp ` G ) -> y C_ X )
22	11, 21	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> y C_ X )
23		ssfi 7789	. . . . . . . . . 10 |- ( ( X e. Fin /\ y C_ X ) -> y e. Fin )
24	20, 22, 23	syl2anc 666	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> y e. Fin )
25	6	subgss 16811	. . . . . . . . . . 11 |- ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) C_ X )
26	17, 25	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) C_ X )
27		ssfi 7789	. . . . . . . . . 10 |- ( ( X e. Fin /\ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) C_ X ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. Fin )
28	20, 26, 27	syl2anc 666	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. Fin )
29		hashen 12527	. . . . . . . . 9 |- ( ( y e. Fin /\ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. Fin ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) <-> y ~~ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) )
30	24, 28, 29	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) <-> y ~~ ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) )
31	19, 30	mpbird 236	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( # ` y ) = ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) )
32	10	simprd 465	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( # ` y ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
33	31, 32	eqtr3d 2486	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
34	6	fislw 17270	. . . . . . . 8 |- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) <-> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) /\ ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
35	1, 4, 5, 34	syl3anc 1267	. . . . . . 7 |- ( ph -> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) <-> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) /\ ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
36	35	adantr 467	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) <-> ( ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. (SubGrp ` G ) /\ ( # ` ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
37	17, 33, 36	mpbir2and 932	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. ( P pSyl G ) ) ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) )
38	37	ralrimivva 2808	. . . 4 |- ( ph -> A. x e. X A. y e. ( P pSyl G ) ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) )
39		sylow3lem1.m	. . . . 5 |- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
40	39	fmpt2 6857	. . . 4 |- ( A. x e. X A. y e. ( P pSyl G ) ran ( z e. y |-> ( ( x .+ z ) .- x ) ) e. ( P pSyl G ) <-> .(+) : ( X X. ( P pSyl G ) ) --> ( P pSyl G ) )
41	38, 40	sylib 200	. . 3 |- ( ph -> .(+) : ( X X. ( P pSyl G ) ) --> ( P pSyl G ) )
42	1	adantr 467	. . . . . . . 8 |- ( ( ph /\ a e. ( P pSyl G ) ) -> G e. Grp )
43		eqid 2450	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
44	6, 43	grpidcl 16687	. . . . . . . 8 |- ( G e. Grp -> ( 0g ` G ) e. X )
45	42, 44	syl 17	. . . . . . 7 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( 0g ` G ) e. X )
46		simpr 463	. . . . . . 7 |- ( ( ph /\ a e. ( P pSyl G ) ) -> a e. ( P pSyl G ) )
47		simpr 463	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> y = a )
48		simpl 459	. . . . . . . . . . . 12 |- ( ( x = ( 0g ` G ) /\ y = a ) -> x = ( 0g ` G ) )
49	48	oveq1d 6303	. . . . . . . . . . 11 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( x .+ z ) = ( ( 0g ` G ) .+ z ) )
50	49, 48	oveq12d 6306	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( ( x .+ z ) .- x ) = ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) )
51	47, 50	mpteq12dv 4480	. . . . . . . . 9 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) )
52	51	rneqd 5061	. . . . . . . 8 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) )
53		vex 3047	. . . . . . . . . 10 |- a e. _V
54	53	mptex 6134	. . . . . . . . 9 |- ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) e. _V
55	54	rnex 6724	. . . . . . . 8 |- ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) e. _V
56	52, 39, 55	ovmpt2a 6424	. . . . . . 7 |- ( ( ( 0g ` G ) e. X /\ a e. ( P pSyl G ) ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) )
57	45, 46, 56	syl2anc 666	. . . . . 6 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) )
58	1	ad2antrr 731	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> G e. Grp )
59		slwsubg 17255	. . . . . . . . . . . . . . . 16 |- ( a e. ( P pSyl G ) -> a e. (SubGrp ` G ) )
60	59	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ a e. ( P pSyl G ) ) -> a e. (SubGrp ` G ) )
61	6	subgss 16811	. . . . . . . . . . . . . . 15 |- ( a e. (SubGrp ` G ) -> a C_ X )
62	60, 61	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ a e. ( P pSyl G ) ) -> a C_ X )
63	62	sselda 3431	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> z e. X )
64	6, 13, 43	grplid 16689	. . . . . . . . . . . . 13 |- ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
65	58, 63, 64	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> ( ( 0g ` G ) .+ z ) = z )
66	65	oveq1d 6303	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) = ( z .- ( 0g ` G ) ) )
67	6, 43, 14	grpsubid1 16732	. . . . . . . . . . . 12 |- ( ( G e. Grp /\ z e. X ) -> ( z .- ( 0g ` G ) ) = z )
68	58, 63, 67	syl2anc 666	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> ( z .- ( 0g ` G ) ) = z )
69	66, 68	eqtrd 2484	. . . . . . . . . 10 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ z e. a ) -> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) = z )
70	69	mpteq2dva 4488	. . . . . . . . 9 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) = ( z e. a |-> z ) )
71		mptresid 5158	. . . . . . . . 9 |- ( z e. a |-> z ) = ( _I |` a )
72	70, 71	syl6eq 2500	. . . . . . . 8 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) = ( _I |` a ) )
73	72	rneqd 5061	. . . . . . 7 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) = ran ( _I |` a ) )
74		rnresi 5180	. . . . . . 7 |- ran ( _I |` a ) = a
75	73, 74	syl6eq 2500	. . . . . 6 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ran ( z e. a |-> ( ( ( 0g ` G ) .+ z ) .- ( 0g ` G ) ) ) = a )
76	57, 75	eqtrd 2484	. . . . 5 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( ( 0g ` G ) .(+) a ) = a )
77		ovex 6316	. . . . . . . . . 10 |- ( ( c .+ z ) .- c ) e. _V
78		oveq2 6296	. . . . . . . . . . 11 |- ( w = ( ( c .+ z ) .- c ) -> ( b .+ w ) = ( b .+ ( ( c .+ z ) .- c ) ) )
79	78	oveq1d 6303	. . . . . . . . . 10 |- ( w = ( ( c .+ z ) .- c ) -> ( ( b .+ w ) .- b ) = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) )
80	77, 79	abrexco 6147	. . . . . . . . 9 |- { u | E. w e. { v | E. z e. a v = ( ( c .+ z ) .- c ) } u = ( ( b .+ w ) .- b ) } = { u | E. z e. a u = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) }
81		simprr 765	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> c e. X )
82		simplr 761	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> a e. ( P pSyl G ) )
83		simpr 463	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> y = a )
84		simpl 459	. . . . . . . . . . . . . . . . . 18 |- ( ( x = c /\ y = a ) -> x = c )
85	84	oveq1d 6303	. . . . . . . . . . . . . . . . 17 |- ( ( x = c /\ y = a ) -> ( x .+ z ) = ( c .+ z ) )
86	85, 84	oveq12d 6306	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> ( ( x .+ z ) .- x ) = ( ( c .+ z ) .- c ) )
87	83, 86	mpteq12dv 4480	. . . . . . . . . . . . . . 15 |- ( ( x = c /\ y = a ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. a |-> ( ( c .+ z ) .- c ) ) )
88	87	rneqd 5061	. . . . . . . . . . . . . 14 |- ( ( x = c /\ y = a ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. a |-> ( ( c .+ z ) .- c ) ) )
89	53	mptex 6134	. . . . . . . . . . . . . . 15 |- ( z e. a |-> ( ( c .+ z ) .- c ) ) e. _V
90	89	rnex 6724	. . . . . . . . . . . . . 14 |- ran ( z e. a |-> ( ( c .+ z ) .- c ) ) e. _V
91	88, 39, 90	ovmpt2a 6424	. . . . . . . . . . . . 13 |- ( ( c e. X /\ a e. ( P pSyl G ) ) -> ( c .(+) a ) = ran ( z e. a |-> ( ( c .+ z ) .- c ) ) )
92	81, 82, 91	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = ran ( z e. a |-> ( ( c .+ z ) .- c ) ) )
93		eqid 2450	. . . . . . . . . . . . 13 |- ( z e. a |-> ( ( c .+ z ) .- c ) ) = ( z e. a |-> ( ( c .+ z ) .- c ) )
94	93	rnmpt 5079	. . . . . . . . . . . 12 |- ran ( z e. a |-> ( ( c .+ z ) .- c ) ) = { v | E. z e. a v = ( ( c .+ z ) .- c ) }
95	92, 94	syl6eq 2500	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = { v | E. z e. a v = ( ( c .+ z ) .- c ) } )
96	95	rexeqdv 2993	. . . . . . . . . 10 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( E. w e. ( c .(+) a ) u = ( ( b .+ w ) .- b ) <-> E. w e. { v | E. z e. a v = ( ( c .+ z ) .- c ) } u = ( ( b .+ w ) .- b ) ) )
97	96	abbidv 2568	. . . . . . . . 9 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( ( b .+ w ) .- b ) } = { u | E. w e. { v | E. z e. a v = ( ( c .+ z ) .- c ) } u = ( ( b .+ w ) .- b ) } )
98	42	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> G e. Grp )
99	98	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> G e. Grp )
100		simprl 763	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> b e. X )
101	6, 13	grpcl 16672	. . . . . . . . . . . . . . . . 17 |- ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .+ c ) e. X )
102	98, 100, 81, 101	syl3anc 1267	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( b .+ c ) e. X )
103	102	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( b .+ c ) e. X )
104	63	adantlr 720	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> z e. X )
105	6, 13	grpcl 16672	. . . . . . . . . . . . . . 15 |- ( ( G e. Grp /\ ( b .+ c ) e. X /\ z e. X ) -> ( ( b .+ c ) .+ z ) e. X )
106	99, 103, 104, 105	syl3anc 1267	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) e. X )
107	81	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> c e. X )
108	100	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> b e. X )
109	6, 13, 14	grpsubsub4 16740	. . . . . . . . . . . . . 14 |- ( ( G e. Grp /\ ( ( ( b .+ c ) .+ z ) e. X /\ c e. X /\ b e. X ) ) -> ( ( ( ( b .+ c ) .+ z ) .- c ) .- b ) = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) )
110	99, 106, 107, 108, 109	syl13anc 1269	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( ( ( b .+ c ) .+ z ) .- c ) .- b ) = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) )
111	6, 13	grpass 16673	. . . . . . . . . . . . . . . . 17 |- ( ( G e. Grp /\ ( b e. X /\ c e. X /\ z e. X ) ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
112	99, 108, 107, 104, 111	syl13anc 1269	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
113	112	oveq1d 6303	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( ( b .+ c ) .+ z ) .- c ) = ( ( b .+ ( c .+ z ) ) .- c ) )
114	6, 13	grpcl 16672	. . . . . . . . . . . . . . . . 17 |- ( ( G e. Grp /\ c e. X /\ z e. X ) -> ( c .+ z ) e. X )
115	99, 107, 104, 114	syl3anc 1267	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( c .+ z ) e. X )
116	6, 13, 14	grpaddsubass 16737	. . . . . . . . . . . . . . . 16 |- ( ( G e. Grp /\ ( b e. X /\ ( c .+ z ) e. X /\ c e. X ) ) -> ( ( b .+ ( c .+ z ) ) .- c ) = ( b .+ ( ( c .+ z ) .- c ) ) )
117	99, 108, 115, 107, 116	syl13anc 1269	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ ( c .+ z ) ) .- c ) = ( b .+ ( ( c .+ z ) .- c ) ) )
118	113, 117	eqtrd 2484	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( ( b .+ c ) .+ z ) .- c ) = ( b .+ ( ( c .+ z ) .- c ) ) )
119	118	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( ( ( b .+ c ) .+ z ) .- c ) .- b ) = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) )
120	110, 119	eqtr3d 2486	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) )
121	120	eqeq2d 2460	. . . . . . . . . . 11 |- ( ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( u = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) <-> u = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) ) )
122	121	rexbidva 2897	. . . . . . . . . 10 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( E. z e. a u = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) <-> E. z e. a u = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) ) )
123	122	abbidv 2568	. . . . . . . . 9 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> { u | E. z e. a u = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) } = { u | E. z e. a u = ( ( b .+ ( ( c .+ z ) .- c ) ) .- b ) } )
124	80, 97, 123	3eqtr4a 2510	. . . . . . . 8 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( ( b .+ w ) .- b ) } = { u | E. z e. a u = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) } )
125		eqid 2450	. . . . . . . . 9 |- ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) = ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) )
126	125	rnmpt 5079	. . . . . . . 8 |- ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) = { u | E. w e. ( c .(+) a ) u = ( ( b .+ w ) .- b ) }
127		eqid 2450	. . . . . . . . 9 |- ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) = ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) )
128	127	rnmpt 5079	. . . . . . . 8 |- ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) = { u | E. z e. a u = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) }
129	124, 126, 128	3eqtr4g 2509	. . . . . . 7 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) = ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) )
130	41	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> .(+) : ( X X. ( P pSyl G ) ) --> ( P pSyl G ) )
131	130, 81, 82	fovrnd 6438	. . . . . . . 8 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) e. ( P pSyl G ) )
132		simpr 463	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> y = ( c .(+) a ) )
133		simpl 459	. . . . . . . . . . . . . 14 |- ( ( x = b /\ y = ( c .(+) a ) ) -> x = b )
134	133	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( x .+ z ) = ( b .+ z ) )
135	134, 133	oveq12d 6306	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( ( x .+ z ) .- x ) = ( ( b .+ z ) .- b ) )
136	132, 135	mpteq12dv 4480	. . . . . . . . . . 11 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. ( c .(+) a ) |-> ( ( b .+ z ) .- b ) ) )
137		oveq2 6296	. . . . . . . . . . . . 13 |- ( z = w -> ( b .+ z ) = ( b .+ w ) )
138	137	oveq1d 6303	. . . . . . . . . . . 12 |- ( z = w -> ( ( b .+ z ) .- b ) = ( ( b .+ w ) .- b ) )
139	138	cbvmptv 4494	. . . . . . . . . . 11 |- ( z e. ( c .(+) a ) |-> ( ( b .+ z ) .- b ) ) = ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) )
140	136, 139	syl6eq 2500	. . . . . . . . . 10 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) )
141	140	rneqd 5061	. . . . . . . . 9 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) )
142		ovex 6316	. . . . . . . . . . 11 |- ( c .(+) a ) e. _V
143	142	mptex 6134	. . . . . . . . . 10 |- ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) e. _V
144	143	rnex 6724	. . . . . . . . 9 |- ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) e. _V
145	141, 39, 144	ovmpt2a 6424	. . . . . . . 8 |- ( ( b e. X /\ ( c .(+) a ) e. ( P pSyl G ) ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) )
146	100, 131, 145	syl2anc 666	. . . . . . 7 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( ( b .+ w ) .- b ) ) )
147		simpr 463	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> y = a )
148		simpl 459	. . . . . . . . . . . . 13 |- ( ( x = ( b .+ c ) /\ y = a ) -> x = ( b .+ c ) )
149	148	oveq1d 6303	. . . . . . . . . . . 12 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( x .+ z ) = ( ( b .+ c ) .+ z ) )
150	149, 148	oveq12d 6306	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( ( x .+ z ) .- x ) = ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) )
151	147, 150	mpteq12dv 4480	. . . . . . . . . 10 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) )
152	151	rneqd 5061	. . . . . . . . 9 |- ( ( x = ( b .+ c ) /\ y = a ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) )
153	53	mptex 6134	. . . . . . . . . 10 |- ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) e. _V
154	153	rnex 6724	. . . . . . . . 9 |- ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) e. _V
155	152, 39, 154	ovmpt2a 6424	. . . . . . . 8 |- ( ( ( b .+ c ) e. X /\ a e. ( P pSyl G ) ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) )
156	102, 82, 155	syl2anc 666	. . . . . . 7 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( ( b .+ c ) .+ z ) .- ( b .+ c ) ) ) )
157	129, 146, 156	3eqtr4rd 2495	. . . . . 6 |- ( ( ( ph /\ a e. ( P pSyl G ) ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
158	157	ralrimivva 2808	. . . . 5 |- ( ( ph /\ a e. ( P pSyl G ) ) -> A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
159	76, 158	jca 535	. . . 4 |- ( ( ph /\ a e. ( P pSyl G ) ) -> ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
160	159	ralrimiva 2801	. . 3 |- ( ph -> A. a e. ( P pSyl G ) ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
161	41, 160	jca 535	. 2 |- ( ph -> ( .(+) : ( X X. ( P pSyl G ) ) --> ( P pSyl G ) /\ A. a e. ( P pSyl G ) ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) )
162	6, 13, 43	isga 16938	. 2 |- ( .(+) e. ( G GrpAct ( P pSyl G ) ) <-> ( ( G e. Grp /\ ( P pSyl G ) e. _V ) /\ ( .(+) : ( X X. ( P pSyl G ) ) --> ( P pSyl G ) /\ A. a e. ( P pSyl G ) ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) ) )
163	3, 161, 162	sylanbrc 669	1 |- ( ph -> .(+) e. ( G GrpAct ( P pSyl G ) ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   {cab 2436   A.wral 2736   E.wrex 2737   _Vcvv 3044   C_ wss 3403   class class class wbr 4401   |-> cmpt 4460   _I cid 4743   X. cxp 4831   ran crn 4834   |` cres 4835   -->wf 5577   ` cfv 5581  (class class class)co 6288   |-> cmpt2 6290   ~~ cen 7563   Fincfn 7566   ^cexp 12269   #chash 12512   Primecprime 14615   pCnt cpc 14779   Basecbs 15114   +g cplusg 15183   0gc0g 15331   Grpcgrp 16662   -gcsg 16664  SubGrpcsubg 16804   GrpAct cga 16936   pSyl cslw 17164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-disj 4373  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-omul 7184  df-er 7360  df-ec 7362  df-qs 7366  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-acn 8373  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-q 11262  df-rp 11300  df-fz 11782  df-fzo 11913  df-fl 12025  df-mod 12094  df-seq 12211  df-exp 12270  df-fac 12457  df-bc 12485  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-sum 13746  df-dvds 14299  df-gcd 14462  df-prm 14616  df-pc 14780  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-0g 15333  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-submnd 16576  df-grp 16666  df-minusg 16667  df-sbg 16668  df-mulg 16669  df-subg 16807  df-eqg 16809  df-ghm 16874  df-ga 16937  df-od 17165  df-pgp 17169  df-slw 17171

This theorem is referenced by:  sylow3lem3  17274  sylow3lem5  17276