Theorem sylow1lem2 16425

Description: Lemma for sylow1 16429. The function .(+) is a group action on S. (Contributed by Mario Carneiro, 15-Jan-2015.)

Hypotheses

Ref	Expression
sylow1.x	|- X = ( Base ` G )
sylow1.g	|- ( ph -> G e. Grp )
sylow1.f	|- ( ph -> X e. Fin )
sylow1.p	|- ( ph -> P e. Prime )
sylow1.n	|- ( ph -> N e. NN0 )
sylow1.d	|- ( ph -> ( P ^ N ) || ( # ` X ) )
sylow1lem.a	|- .+ = ( +g ` G )
sylow1lem.s	|- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
sylow1lem.m	|- .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )

Assertion

Ref	Expression
sylow1lem2	|- ( ph -> .(+) e. ( G GrpAct S ) )

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

Allowed substitution hints:   ph( s)   .(+) ( s)   S( s)

Proof of Theorem sylow1lem2

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

Step	Hyp	Ref	Expression
1		sylow1.g	. . 3 |- ( ph -> G e. Grp )
2		sylow1lem.s	. . . 4 |- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
3		sylow1.x	. . . . . . 7 |- X = ( Base ` G )
4		fvex 5876	. . . . . . 7 |- ( Base ` G ) e. _V
5	3, 4	eqeltri 2551	. . . . . 6 |- X e. _V
6	5	pwex 4630	. . . . 5 |- ~P X e. _V
7	6	rabex 4598	. . . 4 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } e. _V
8	2, 7	eqeltri 2551	. . 3 |- S e. _V
9	1, 8	jctir 538	. 2 |- ( ph -> ( G e. Grp /\ S e. _V ) )
10	1	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> G e. Grp )
11		simprl 755	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> x e. X )
12		sylow1lem.a	. . . . . . . . . . . . 13 |- .+ = ( +g ` G )
13		eqid 2467	. . . . . . . . . . . . 13 |- ( z e. X |-> ( x .+ z ) ) = ( z e. X |-> ( x .+ z ) )
14	3, 12, 13	grplmulf1o 15922	. . . . . . . . . . . 12 |- ( ( G e. Grp /\ x e. X ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
15	10, 11, 14	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
16		f1of1 5815	. . . . . . . . . . 11 |- ( ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X -> ( z e. X |-> ( x .+ z ) ) : X -1-1-> X )
17	15, 16	syl 16	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-> X )
18		simprr 756	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. S )
19		fveq2 5866	. . . . . . . . . . . . . . 15 |- ( s = y -> ( # ` s ) = ( # ` y ) )
20	19	eqeq1d 2469	. . . . . . . . . . . . . 14 |- ( s = y -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` y ) = ( P ^ N ) ) )
21	20, 2	elrab2 3263	. . . . . . . . . . . . 13 |- ( y e. S <-> ( y e. ~P X /\ ( # ` y ) = ( P ^ N ) ) )
22	18, 21	sylib 196	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( y e. ~P X /\ ( # ` y ) = ( P ^ N ) ) )
23	22	simpld 459	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. ~P X )
24	23	elpwid 4020	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y C_ X )
25		f1ssres 5788	. . . . . . . . . 10 |- ( ( ( z e. X |-> ( x .+ z ) ) : X -1-1-> X /\ y C_ X ) -> ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X )
26	17, 24, 25	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X )
27		resmpt 5323	. . . . . . . . . 10 |- ( y C_ X -> ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) )
28		f1eq1 5776	. . . . . . . . . 10 |- ( ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) -> ( ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X <-> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X ) )
29	24, 27, 28	3syl 20	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X <-> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X ) )
30	26, 29	mpbid 210	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X )
31		f1f 5781	. . . . . . . 8 |- ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y --> X )
32		frn 5737	. . . . . . . 8 |- ( ( z e. y |-> ( x .+ z ) ) : y --> X -> ran ( z e. y |-> ( x .+ z ) ) C_ X )
33	30, 31, 32	3syl 20	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) C_ X )
34	5	elpw2 4611	. . . . . . 7 |- ( ran ( z e. y |-> ( x .+ z ) ) e. ~P X <-> ran ( z e. y |-> ( x .+ z ) ) C_ X )
35	33, 34	sylibr 212	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. ~P X )
36		f1f1orn 5827	. . . . . . . . 9 |- ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y -1-1-onto-> ran ( z e. y |-> ( x .+ z ) ) )
37		vex 3116	. . . . . . . . . 10 |- y e. _V
38	37	f1oen 7536	. . . . . . . . 9 |- ( ( z e. y |-> ( x .+ z ) ) : y -1-1-onto-> ran ( z e. y |-> ( x .+ z ) ) -> y ~~ ran ( z e. y |-> ( x .+ z ) ) )
39	30, 36, 38	3syl 20	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y ~~ ran ( z e. y |-> ( x .+ z ) ) )
40		sylow1.f	. . . . . . . . . . 11 |- ( ph -> X e. Fin )
41	40	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> X e. Fin )
42		ssfi 7740	. . . . . . . . . 10 |- ( ( X e. Fin /\ y C_ X ) -> y e. Fin )
43	41, 24, 42	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. Fin )
44		ssfi 7740	. . . . . . . . . 10 |- ( ( X e. Fin /\ ran ( z e. y |-> ( x .+ z ) ) C_ X ) -> ran ( z e. y |-> ( x .+ z ) ) e. Fin )
45	41, 33, 44	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. Fin )
46		hashen 12388	. . . . . . . . 9 |- ( ( y e. Fin /\ ran ( z e. y |-> ( x .+ z ) ) e. Fin ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) <-> y ~~ ran ( z e. y |-> ( x .+ z ) ) ) )
47	43, 45, 46	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) <-> y ~~ ran ( z e. y |-> ( x .+ z ) ) ) )
48	39, 47	mpbird 232	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) )
49	22	simprd 463	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` y ) = ( P ^ N ) )
50	48, 49	eqtr3d 2510	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) )
51		fveq2 5866	. . . . . . . 8 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( # ` s ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) )
52	51	eqeq1d 2469	. . . . . . 7 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
53	52, 2	elrab2 3263	. . . . . 6 |- ( ran ( z e. y |-> ( x .+ z ) ) e. S <-> ( ran ( z e. y |-> ( x .+ z ) ) e. ~P X /\ ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
54	35, 50, 53	sylanbrc 664	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. S )
55	54	ralrimivva 2885	. . . 4 |- ( ph -> A. x e. X A. y e. S ran ( z e. y |-> ( x .+ z ) ) e. S )
56		sylow1lem.m	. . . . 5 |- .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )
57	56	fmpt2 6851	. . . 4 |- ( A. x e. X A. y e. S ran ( z e. y |-> ( x .+ z ) ) e. S <-> .(+) : ( X X. S ) --> S )
58	55, 57	sylib 196	. . 3 |- ( ph -> .(+) : ( X X. S ) --> S )
59	1	adantr 465	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> G e. Grp )
60		eqid 2467	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
61	3, 60	grpidcl 15888	. . . . . . . 8 |- ( G e. Grp -> ( 0g ` G ) e. X )
62	59, 61	syl 16	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ( 0g ` G ) e. X )
63		simpr 461	. . . . . . 7 |- ( ( ph /\ a e. S ) -> a e. S )
64		simpr 461	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> y = a )
65		simpl 457	. . . . . . . . . . 11 |- ( ( x = ( 0g ` G ) /\ y = a ) -> x = ( 0g ` G ) )
66	65	oveq1d 6299	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( x .+ z ) = ( ( 0g ` G ) .+ z ) )
67	64, 66	mpteq12dv 4525	. . . . . . . . 9 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
68	67	rneqd 5230	. . . . . . . 8 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
69		vex 3116	. . . . . . . . . 10 |- a e. _V
70	69	mptex 6131	. . . . . . . . 9 |- ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
71	70	rnex 6718	. . . . . . . 8 |- ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
72	68, 56, 71	ovmpt2a 6417	. . . . . . 7 |- ( ( ( 0g ` G ) e. X /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
73	62, 63, 72	syl2anc 661	. . . . . 6 |- ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
74		ssrab2 3585	. . . . . . . . . . . . . . 15 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } C_ ~P X
75	2, 74	eqsstri 3534	. . . . . . . . . . . . . 14 |- S C_ ~P X
76	75, 63	sseldi 3502	. . . . . . . . . . . . 13 |- ( ( ph /\ a e. S ) -> a e. ~P X )
77	76	elpwid 4020	. . . . . . . . . . . 12 |- ( ( ph /\ a e. S ) -> a C_ X )
78	77	sselda 3504	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ z e. a ) -> z e. X )
79	3, 12, 60	grplid 15890	. . . . . . . . . . . 12 |- ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
80	59, 79	sylan 471	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
81	78, 80	syldan 470	. . . . . . . . . 10 |- ( ( ( ph /\ a e. S ) /\ z e. a ) -> ( ( 0g ` G ) .+ z ) = z )
82	81	mpteq2dva 4533	. . . . . . . . 9 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( z e. a |-> z ) )
83		mptresid 5328	. . . . . . . . 9 |- ( z e. a |-> z ) = ( _I |` a )
84	82, 83	syl6eq 2524	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( _I |` a ) )
85	84	rneqd 5230	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ran ( _I |` a ) )
86		rnresi 5350	. . . . . . 7 |- ran ( _I |` a ) = a
87	85, 86	syl6eq 2524	. . . . . 6 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = a )
88	73, 87	eqtrd 2508	. . . . 5 |- ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = a )
89		ovex 6309	. . . . . . . . . 10 |- ( c .+ z ) e. _V
90		oveq2 6292	. . . . . . . . . 10 |- ( w = ( c .+ z ) -> ( b .+ w ) = ( b .+ ( c .+ z ) ) )
91	89, 90	abrexco 6144	. . . . . . . . 9 |- { u | E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) } = { u | E. z e. a u = ( b .+ ( c .+ z ) ) }
92		simprr 756	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> c e. X )
93	63	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> a e. S )
94		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> y = a )
95		simpl 457	. . . . . . . . . . . . . . . . 17 |- ( ( x = c /\ y = a ) -> x = c )
96	95	oveq1d 6299	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> ( x .+ z ) = ( c .+ z ) )
97	94, 96	mpteq12dv 4525	. . . . . . . . . . . . . . 15 |- ( ( x = c /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( c .+ z ) ) )
98	97	rneqd 5230	. . . . . . . . . . . . . 14 |- ( ( x = c /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( c .+ z ) ) )
99	69	mptex 6131	. . . . . . . . . . . . . . 15 |- ( z e. a |-> ( c .+ z ) ) e. _V
100	99	rnex 6718	. . . . . . . . . . . . . 14 |- ran ( z e. a |-> ( c .+ z ) ) e. _V
101	98, 56, 100	ovmpt2a 6417	. . . . . . . . . . . . 13 |- ( ( c e. X /\ a e. S ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
102	92, 93, 101	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
103		eqid 2467	. . . . . . . . . . . . 13 |- ( z e. a |-> ( c .+ z ) ) = ( z e. a |-> ( c .+ z ) )
104	103	rnmpt 5248	. . . . . . . . . . . 12 |- ran ( z e. a |-> ( c .+ z ) ) = { v | E. z e. a v = ( c .+ z ) }
105	102, 104	syl6eq 2524	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = { v | E. z e. a v = ( c .+ z ) } )
106	105	rexeqdv 3065	. . . . . . . . . 10 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( E. w e. ( c .(+) a ) u = ( b .+ w ) <-> E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) ) )
107	106	abbidv 2603	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( b .+ w ) } = { u | E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) } )
108	59	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> G e. Grp )
109		simprl 755	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> b e. X )
110	109	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> b e. X )
111	92	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> c e. X )
112	78	adantlr 714	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> z e. X )
113	3, 12	grpass 15874	. . . . . . . . . . . . 13 |- ( ( G e. Grp /\ ( b e. X /\ c e. X /\ z e. X ) ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
114	108, 110, 111, 112, 113	syl13anc 1230	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
115	114	eqeq2d 2481	. . . . . . . . . . 11 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( u = ( ( b .+ c ) .+ z ) <-> u = ( b .+ ( c .+ z ) ) ) )
116	115	rexbidva 2970	. . . . . . . . . 10 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( E. z e. a u = ( ( b .+ c ) .+ z ) <-> E. z e. a u = ( b .+ ( c .+ z ) ) ) )
117	116	abbidv 2603	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. z e. a u = ( ( b .+ c ) .+ z ) } = { u | E. z e. a u = ( b .+ ( c .+ z ) ) } )
118	91, 107, 117	3eqtr4a 2534	. . . . . . . 8 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( b .+ w ) } = { u | E. z e. a u = ( ( b .+ c ) .+ z ) } )
119		eqid 2467	. . . . . . . . 9 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
120	119	rnmpt 5248	. . . . . . . 8 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = { u | E. w e. ( c .(+) a ) u = ( b .+ w ) }
121		eqid 2467	. . . . . . . . 9 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) )
122	121	rnmpt 5248	. . . . . . . 8 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) = { u | E. z e. a u = ( ( b .+ c ) .+ z ) }
123	118, 120, 122	3eqtr4g 2533	. . . . . . 7 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
124	58	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> .(+) : ( X X. S ) --> S )
125	124, 92, 93	fovrnd 6431	. . . . . . . 8 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) e. S )
126		simpr 461	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> y = ( c .(+) a ) )
127		simpl 457	. . . . . . . . . . . . 13 |- ( ( x = b /\ y = ( c .(+) a ) ) -> x = b )
128	127	oveq1d 6299	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( x .+ z ) = ( b .+ z ) )
129	126, 128	mpteq12dv 4525	. . . . . . . . . . 11 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. ( c .(+) a ) |-> ( b .+ z ) ) )
130		oveq2 6292	. . . . . . . . . . . 12 |- ( z = w -> ( b .+ z ) = ( b .+ w ) )
131	130	cbvmptv 4538	. . . . . . . . . . 11 |- ( z e. ( c .(+) a ) |-> ( b .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
132	129, 131	syl6eq 2524	. . . . . . . . . 10 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
133	132	rneqd 5230	. . . . . . . . 9 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
134		ovex 6309	. . . . . . . . . . 11 |- ( c .(+) a ) e. _V
135	134	mptex 6131	. . . . . . . . . 10 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
136	135	rnex 6718	. . . . . . . . 9 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
137	133, 56, 136	ovmpt2a 6417	. . . . . . . 8 |- ( ( b e. X /\ ( c .(+) a ) e. S ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
138	109, 125, 137	syl2anc 661	. . . . . . 7 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
139	1	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> G e. Grp )
140	3, 12	grpcl 15873	. . . . . . . . 9 |- ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .+ c ) e. X )
141	139, 109, 92, 140	syl3anc 1228	. . . . . . . 8 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .+ c ) e. X )
142		simpr 461	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> y = a )
143		simpl 457	. . . . . . . . . . . 12 |- ( ( x = ( b .+ c ) /\ y = a ) -> x = ( b .+ c ) )
144	143	oveq1d 6299	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( x .+ z ) = ( ( b .+ c ) .+ z ) )
145	142, 144	mpteq12dv 4525	. . . . . . . . . 10 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
146	145	rneqd 5230	. . . . . . . . 9 |- ( ( x = ( b .+ c ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
147	69	mptex 6131	. . . . . . . . . 10 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
148	147	rnex 6718	. . . . . . . . 9 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
149	146, 56, 148	ovmpt2a 6417	. . . . . . . 8 |- ( ( ( b .+ c ) e. X /\ a e. S ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
150	141, 93, 149	syl2anc 661	. . . . . . 7 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
151	123, 138, 150	3eqtr4rd 2519	. . . . . 6 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
152	151	ralrimivva 2885	. . . . 5 |- ( ( ph /\ a e. S ) -> A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
153	88, 152	jca 532	. . . 4 |- ( ( ph /\ a e. S ) -> ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
154	153	ralrimiva 2878	. . 3 |- ( ph -> A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
155	58, 154	jca 532	. 2 |- ( ph -> ( .(+) : ( X X. S ) --> S /\ A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) )
156	3, 12, 60	isga 16134	. 2 |- ( .(+) e. ( G GrpAct S ) <-> ( ( G e. Grp /\ S e. _V ) /\ ( .(+) : ( X X. S ) --> S /\ A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) ) )
157	9, 155, 156	sylanbrc 664	1 |- ( ph -> .(+) e. ( G GrpAct S ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   C_ wss 3476   ~Pcpw 4010   class class class wbr 4447   |-> cmpt 4505   _I cid 4790   X. cxp 4997   ran crn 5000   |` cres 5001   -->wf 5584   -1-1->wf1 5585   -1-1-onto->wf1o 5587   ` cfv 5588  (class class class)co 6284   |-> cmpt2 6286   ~~ cen 7513   Fincfn 7516   NN0cn0 10795   ^cexp 12134   #chash 12373   || cdivides 13847   Primecprime 14076   Basecbs 14490   +g cplusg 14555   0gc0g 14695   Grpcgrp 15727   GrpAct cga 16132

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-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569

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 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-er 7311  df-map 7422  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-card 8320  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-n0 10796  df-z 10865  df-uz 11083  df-hash 12374  df-0g 14697  df-mnd 15732  df-grp 15867  df-minusg 15868  df-ga 16133

This theorem is referenced by:  sylow1lem3  16426  sylow1lem5  16428