Theorem sylow1lem2 16091

Description: Lemma for sylow1 16095. 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 5698	. . . . . . 7 |- ( Base ` G ) e. _V
5	3, 4	eqeltri 2511	. . . . . 6 |- X e. _V
6	5	pwex 4472	. . . . 5 |- ~P X e. _V
7	6	rabex 4440	. . . 4 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } e. _V
8	2, 7	eqeltri 2511	. . 3 |- S e. _V
9	1, 8	jctir 535	. 2 |- ( ph -> ( G e. Grp /\ S e. _V ) )
10	1	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> G e. Grp )
11		simprl 750	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> x e. X )
12		sylow1lem.a	. . . . . . . . . . . . 13 |- .+ = ( +g ` G )
13		eqid 2441	. . . . . . . . . . . . 13 |- ( z e. X |-> ( x .+ z ) ) = ( z e. X |-> ( x .+ z ) )
14	3, 12, 13	grplmulf1o 15593	. . . . . . . . . . . 12 |- ( ( G e. Grp /\ x e. X ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
15	10, 11, 14	syl2anc 656	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
16		f1of1 5637	. . . . . . . . . . 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 751	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. S )
19		fveq2 5688	. . . . . . . . . . . . . . 15 |- ( s = y -> ( # ` s ) = ( # ` y ) )
20	19	eqeq1d 2449	. . . . . . . . . . . . . 14 |- ( s = y -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` y ) = ( P ^ N ) ) )
21	20, 2	elrab2 3116	. . . . . . . . . . . . 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 456	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. ~P X )
24	23	elpwid 3867	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y C_ X )
25		f1ssres 5610	. . . . . . . . . 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 656	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X )
27		resmpt 5153	. . . . . . . . . 10 |- ( y C_ X -> ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) )
28		f1eq1 5598	. . . . . . . . . 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 5603	. . . . . . . 8 |- ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y --> X )
32		frn 5562	. . . . . . . 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 4453	. . . . . . 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 5649	. . . . . . . . 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 2973	. . . . . . . . . 10 |- y e. _V
38	37	f1oen 7326	. . . . . . . . 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 462	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> X e. Fin )
42		ssfi 7529	. . . . . . . . . 10 |- ( ( X e. Fin /\ y C_ X ) -> y e. Fin )
43	41, 24, 42	syl2anc 656	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. Fin )
44		ssfi 7529	. . . . . . . . . 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 656	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. Fin )
46		hashen 12114	. . . . . . . . 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 656	. . . . . . . 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 460	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` y ) = ( P ^ N ) )
50	48, 49	eqtr3d 2475	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) )
51		fveq2 5688	. . . . . . . 8 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( # ` s ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) )
52	51	eqeq1d 2449	. . . . . . 7 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
53	52, 2	elrab2 3116	. . . . . 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 659	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. S )
55	54	ralrimivva 2806	. . . 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 6640	. . . 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 462	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> G e. Grp )
60		eqid 2441	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
61	3, 60	grpidcl 15559	. . . . . . . 8 |- ( G e. Grp -> ( 0g ` G ) e. X )
62	59, 61	syl 16	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ( 0g ` G ) e. X )
63		simpr 458	. . . . . . 7 |- ( ( ph /\ a e. S ) -> a e. S )
64		simpr 458	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> y = a )
65		simpl 454	. . . . . . . . . . 11 |- ( ( x = ( 0g ` G ) /\ y = a ) -> x = ( 0g ` G ) )
66	65	oveq1d 6105	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( x .+ z ) = ( ( 0g ` G ) .+ z ) )
67	64, 66	mpteq12dv 4367	. . . . . . . . 9 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
68	67	rneqd 5063	. . . . . . . 8 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
69		vex 2973	. . . . . . . . . 10 |- a e. _V
70	69	mptex 5945	. . . . . . . . 9 |- ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
71	70	rnex 6511	. . . . . . . 8 |- ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
72	68, 56, 71	ovmpt2a 6220	. . . . . . 7 |- ( ( ( 0g ` G ) e. X /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
73	62, 63, 72	syl2anc 656	. . . . . 6 |- ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
74		ssrab2 3434	. . . . . . . . . . . . . . 15 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } C_ ~P X
75	2, 74	eqsstri 3383	. . . . . . . . . . . . . 14 |- S C_ ~P X
76	75, 63	sseldi 3351	. . . . . . . . . . . . 13 |- ( ( ph /\ a e. S ) -> a e. ~P X )
77	76	elpwid 3867	. . . . . . . . . . . 12 |- ( ( ph /\ a e. S ) -> a C_ X )
78	77	sselda 3353	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ z e. a ) -> z e. X )
79	3, 12, 60	grplid 15561	. . . . . . . . . . . 12 |- ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
80	59, 79	sylan 468	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
81	78, 80	syldan 467	. . . . . . . . . 10 |- ( ( ( ph /\ a e. S ) /\ z e. a ) -> ( ( 0g ` G ) .+ z ) = z )
82	81	mpteq2dva 4375	. . . . . . . . 9 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( z e. a |-> z ) )
83		mptresid 5157	. . . . . . . . 9 |- ( z e. a |-> z ) = ( _I |` a )
84	82, 83	syl6eq 2489	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( _I |` a ) )
85	84	rneqd 5063	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ran ( _I |` a ) )
86		rnresi 5179	. . . . . . 7 |- ran ( _I |` a ) = a
87	85, 86	syl6eq 2489	. . . . . 6 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = a )
88	73, 87	eqtrd 2473	. . . . 5 |- ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = a )
89		ovex 6115	. . . . . . . . . 10 |- ( c .+ z ) e. _V
90		oveq2 6098	. . . . . . . . . 10 |- ( w = ( c .+ z ) -> ( b .+ w ) = ( b .+ ( c .+ z ) ) )
91	89, 90	abrexco 5958	. . . . . . . . 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 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> c e. X )
93	63	adantr 462	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> a e. S )
94		simpr 458	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> y = a )
95		simpl 454	. . . . . . . . . . . . . . . . 17 |- ( ( x = c /\ y = a ) -> x = c )
96	95	oveq1d 6105	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> ( x .+ z ) = ( c .+ z ) )
97	94, 96	mpteq12dv 4367	. . . . . . . . . . . . . . 15 |- ( ( x = c /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( c .+ z ) ) )
98	97	rneqd 5063	. . . . . . . . . . . . . 14 |- ( ( x = c /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( c .+ z ) ) )
99	69	mptex 5945	. . . . . . . . . . . . . . 15 |- ( z e. a |-> ( c .+ z ) ) e. _V
100	99	rnex 6511	. . . . . . . . . . . . . 14 |- ran ( z e. a |-> ( c .+ z ) ) e. _V
101	98, 56, 100	ovmpt2a 6220	. . . . . . . . . . . . 13 |- ( ( c e. X /\ a e. S ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
102	92, 93, 101	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
103		eqid 2441	. . . . . . . . . . . . 13 |- ( z e. a |-> ( c .+ z ) ) = ( z e. a |-> ( c .+ z ) )
104	103	rnmpt 5081	. . . . . . . . . . . 12 |- ran ( z e. a |-> ( c .+ z ) ) = { v | E. z e. a v = ( c .+ z ) }
105	102, 104	syl6eq 2489	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = { v | E. z e. a v = ( c .+ z ) } )
106	105	rexeqdv 2922	. . . . . . . . . 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 2555	. . . . . . . . 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 720	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> G e. Grp )
109		simprl 750	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> b e. X )
110	109	adantr 462	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> b e. X )
111	92	adantr 462	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> c e. X )
112	78	adantlr 709	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> z e. X )
113	3, 12	grpass 15545	. . . . . . . . . . . . 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 1215	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
115	114	eqeq2d 2452	. . . . . . . . . . 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 2730	. . . . . . . . . 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 2555	. . . . . . . . 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 2499	. . . . . . . 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 2441	. . . . . . . . 9 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
120	119	rnmpt 5081	. . . . . . . 8 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = { u | E. w e. ( c .(+) a ) u = ( b .+ w ) }
121		eqid 2441	. . . . . . . . 9 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) )
122	121	rnmpt 5081	. . . . . . . 8 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) = { u | E. z e. a u = ( ( b .+ c ) .+ z ) }
123	118, 120, 122	3eqtr4g 2498	. . . . . . 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 720	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> .(+) : ( X X. S ) --> S )
125	124, 92, 93	fovrnd 6234	. . . . . . . 8 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) e. S )
126		simpr 458	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> y = ( c .(+) a ) )
127		simpl 454	. . . . . . . . . . . . 13 |- ( ( x = b /\ y = ( c .(+) a ) ) -> x = b )
128	127	oveq1d 6105	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( x .+ z ) = ( b .+ z ) )
129	126, 128	mpteq12dv 4367	. . . . . . . . . . 11 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. ( c .(+) a ) |-> ( b .+ z ) ) )
130		oveq2 6098	. . . . . . . . . . . 12 |- ( z = w -> ( b .+ z ) = ( b .+ w ) )
131	130	cbvmptv 4380	. . . . . . . . . . 11 |- ( z e. ( c .(+) a ) |-> ( b .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
132	129, 131	syl6eq 2489	. . . . . . . . . 10 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
133	132	rneqd 5063	. . . . . . . . 9 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
134		ovex 6115	. . . . . . . . . . 11 |- ( c .(+) a ) e. _V
135	134	mptex 5945	. . . . . . . . . 10 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
136	135	rnex 6511	. . . . . . . . 9 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
137	133, 56, 136	ovmpt2a 6220	. . . . . . . 8 |- ( ( b e. X /\ ( c .(+) a ) e. S ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
138	109, 125, 137	syl2anc 656	. . . . . . 7 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
139	1	ad2antrr 720	. . . . . . . . 9 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> G e. Grp )
140	3, 12	grpcl 15544	. . . . . . . . 9 |- ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .+ c ) e. X )
141	139, 109, 92, 140	syl3anc 1213	. . . . . . . 8 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .+ c ) e. X )
142		simpr 458	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> y = a )
143		simpl 454	. . . . . . . . . . . 12 |- ( ( x = ( b .+ c ) /\ y = a ) -> x = ( b .+ c ) )
144	143	oveq1d 6105	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( x .+ z ) = ( ( b .+ c ) .+ z ) )
145	142, 144	mpteq12dv 4367	. . . . . . . . . 10 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
146	145	rneqd 5063	. . . . . . . . 9 |- ( ( x = ( b .+ c ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
147	69	mptex 5945	. . . . . . . . . 10 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
148	147	rnex 6511	. . . . . . . . 9 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
149	146, 56, 148	ovmpt2a 6220	. . . . . . . 8 |- ( ( ( b .+ c ) e. X /\ a e. S ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
150	141, 93, 149	syl2anc 656	. . . . . . 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 2484	. . . . . 6 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
152	151	ralrimivva 2806	. . . . 5 |- ( ( ph /\ a e. S ) -> A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
153	88, 152	jca 529	. . . 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 2797	. . 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 529	. 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 15802	. 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 659	1 |- ( ph -> .(+) e. ( G GrpAct S ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1364   e. wcel 1761   {cab 2427   A.wral 2713   E.wrex 2714   {crab 2717   _Vcvv 2970   C_ wss 3325   ~Pcpw 3857   class class class wbr 4289   e. cmpt 4347   _I cid 4627   X. cxp 4834   ran crn 4837   |` cres 4838   -->wf 5411   -1-1->wf1 5412   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   e. cmpt2 6092   ~~ cen 7303   Fincfn 7306   NN0cn0 10575   ^cexp 11861   #chash 12099   || cdivides 13531   Primecprime 13759   Basecbs 14170   +g cplusg 14234   0gc0g 14374   Grpcgrp 15406   GrpAct cga 15800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-er 7097  df-map 7212  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-n0 10576  df-z 10643  df-uz 10858  df-hash 12100  df-0g 14376  df-mnd 15411  df-grp 15538  df-minusg 15539  df-ga 15801

This theorem is referenced by:  sylow1lem3  16092  sylow1lem5  16094