Theorem sylow1lem2 16098

Description: Lemma for sylow1 16102. 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 5701	. . . . . . 7 |- ( Base ` G ) e. _V
5	3, 4	eqeltri 2513	. . . . . 6 |- X e. _V
6	5	pwex 4475	. . . . 5 |- ~P X e. _V
7	6	rabex 4443	. . . 4 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } e. _V
8	2, 7	eqeltri 2513	. . 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 2443	. . . . . . . . . . . . 13 |- ( z e. X |-> ( x .+ z ) ) = ( z e. X |-> ( x .+ z ) )
14	3, 12, 13	grplmulf1o 15600	. . . . . . . . . . . 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 5640	. . . . . . . . . . 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 5691	. . . . . . . . . . . . . . 15 |- ( s = y -> ( # ` s ) = ( # ` y ) )
20	19	eqeq1d 2451	. . . . . . . . . . . . . 14 |- ( s = y -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` y ) = ( P ^ N ) ) )
21	20, 2	elrab2 3119	. . . . . . . . . . . . 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 3870	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> y C_ X )
25		f1ssres 5613	. . . . . . . . . 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 5156	. . . . . . . . . 10 |- ( y C_ X -> ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) )
28		f1eq1 5601	. . . . . . . . . 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 5606	. . . . . . . 8 |- ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y --> X )
32		frn 5565	. . . . . . . 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 4456	. . . . . . 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 5652	. . . . . . . . 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 2975	. . . . . . . . . 10 |- y e. _V
38	37	f1oen 7330	. . . . . . . . 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 7533	. . . . . . . . . 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 7533	. . . . . . . . . 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 12118	. . . . . . . . 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 2477	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) )
51		fveq2 5691	. . . . . . . 8 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( # ` s ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) )
52	51	eqeq1d 2451	. . . . . . 7 |- ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
53	52, 2	elrab2 3119	. . . . . 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 2808	. . . 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 6641	. . . 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 2443	. . . . . . . . 9 |- ( 0g ` G ) = ( 0g ` G )
61	3, 60	grpidcl 15566	. . . . . . . 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 6106	. . . . . . . . . 10 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( x .+ z ) = ( ( 0g ` G ) .+ z ) )
67	64, 66	mpteq12dv 4370	. . . . . . . . 9 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
68	67	rneqd 5067	. . . . . . . 8 |- ( ( x = ( 0g ` G ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
69		vex 2975	. . . . . . . . . 10 |- a e. _V
70	69	mptex 5948	. . . . . . . . 9 |- ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
71	70	rnex 6512	. . . . . . . 8 |- ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
72	68, 56, 71	ovmpt2a 6221	. . . . . . 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 3437	. . . . . . . . . . . . . . 15 |- { s e. ~P X | ( # ` s ) = ( P ^ N ) } C_ ~P X
75	2, 74	eqsstri 3386	. . . . . . . . . . . . . 14 |- S C_ ~P X
76	75, 63	sseldi 3354	. . . . . . . . . . . . 13 |- ( ( ph /\ a e. S ) -> a e. ~P X )
77	76	elpwid 3870	. . . . . . . . . . . 12 |- ( ( ph /\ a e. S ) -> a C_ X )
78	77	sselda 3356	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ z e. a ) -> z e. X )
79	3, 12, 60	grplid 15568	. . . . . . . . . . . 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 4378	. . . . . . . . 9 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( z e. a |-> z ) )
83		mptresid 5160	. . . . . . . . 9 |- ( z e. a |-> z ) = ( _I |` a )
84	82, 83	syl6eq 2491	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( _I |` a ) )
85	84	rneqd 5067	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ran ( _I |` a ) )
86		rnresi 5182	. . . . . . 7 |- ran ( _I |` a ) = a
87	85, 86	syl6eq 2491	. . . . . 6 |- ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = a )
88	73, 87	eqtrd 2475	. . . . 5 |- ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = a )
89		ovex 6116	. . . . . . . . . 10 |- ( c .+ z ) e. _V
90		oveq2 6099	. . . . . . . . . 10 |- ( w = ( c .+ z ) -> ( b .+ w ) = ( b .+ ( c .+ z ) ) )
91	89, 90	abrexco 5961	. . . . . . . . 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 6106	. . . . . . . . . . . . . . . 16 |- ( ( x = c /\ y = a ) -> ( x .+ z ) = ( c .+ z ) )
97	94, 96	mpteq12dv 4370	. . . . . . . . . . . . . . 15 |- ( ( x = c /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( c .+ z ) ) )
98	97	rneqd 5067	. . . . . . . . . . . . . 14 |- ( ( x = c /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( c .+ z ) ) )
99	69	mptex 5948	. . . . . . . . . . . . . . 15 |- ( z e. a |-> ( c .+ z ) ) e. _V
100	99	rnex 6512	. . . . . . . . . . . . . 14 |- ran ( z e. a |-> ( c .+ z ) ) e. _V
101	98, 56, 100	ovmpt2a 6221	. . . . . . . . . . . . 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 2443	. . . . . . . . . . . . 13 |- ( z e. a |-> ( c .+ z ) ) = ( z e. a |-> ( c .+ z ) )
104	103	rnmpt 5085	. . . . . . . . . . . 12 |- ran ( z e. a |-> ( c .+ z ) ) = { v | E. z e. a v = ( c .+ z ) }
105	102, 104	syl6eq 2491	. . . . . . . . . . 11 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = { v | E. z e. a v = ( c .+ z ) } )
106	105	rexeqdv 2924	. . . . . . . . . 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 2557	. . . . . . . . 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 15552	. . . . . . . . . . . . 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 1220	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
115	114	eqeq2d 2454	. . . . . . . . . . 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 2732	. . . . . . . . . 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 2557	. . . . . . . . 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 2501	. . . . . . . 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 2443	. . . . . . . . 9 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
120	119	rnmpt 5085	. . . . . . . 8 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = { u | E. w e. ( c .(+) a ) u = ( b .+ w ) }
121		eqid 2443	. . . . . . . . 9 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) )
122	121	rnmpt 5085	. . . . . . . 8 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) = { u | E. z e. a u = ( ( b .+ c ) .+ z ) }
123	118, 120, 122	3eqtr4g 2500	. . . . . . 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 6235	. . . . . . . 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 6106	. . . . . . . . . . . 12 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( x .+ z ) = ( b .+ z ) )
129	126, 128	mpteq12dv 4370	. . . . . . . . . . 11 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. ( c .(+) a ) |-> ( b .+ z ) ) )
130		oveq2 6099	. . . . . . . . . . . 12 |- ( z = w -> ( b .+ z ) = ( b .+ w ) )
131	130	cbvmptv 4383	. . . . . . . . . . 11 |- ( z e. ( c .(+) a ) |-> ( b .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
132	129, 131	syl6eq 2491	. . . . . . . . . 10 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
133	132	rneqd 5067	. . . . . . . . 9 |- ( ( x = b /\ y = ( c .(+) a ) ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
134		ovex 6116	. . . . . . . . . . 11 |- ( c .(+) a ) e. _V
135	134	mptex 5948	. . . . . . . . . 10 |- ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
136	135	rnex 6512	. . . . . . . . 9 |- ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
137	133, 56, 136	ovmpt2a 6221	. . . . . . . 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 15551	. . . . . . . . 9 |- ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .+ c ) e. X )
141	139, 109, 92, 140	syl3anc 1218	. . . . . . . 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 6106	. . . . . . . . . . 11 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( x .+ z ) = ( ( b .+ c ) .+ z ) )
145	142, 144	mpteq12dv 4370	. . . . . . . . . 10 |- ( ( x = ( b .+ c ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
146	145	rneqd 5067	. . . . . . . . 9 |- ( ( x = ( b .+ c ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
147	69	mptex 5948	. . . . . . . . . 10 |- ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
148	147	rnex 6512	. . . . . . . . 9 |- ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
149	146, 56, 148	ovmpt2a 6221	. . . . . . . 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 2486	. . . . . 6 |- ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
152	151	ralrimivva 2808	. . . . 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 2799	. . 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 15809	. 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 1369   e. wcel 1756   {cab 2429   A.wral 2715   E.wrex 2716   {crab 2719   _Vcvv 2972   C_ wss 3328   ~Pcpw 3860   class class class wbr 4292   e. cmpt 4350   _I cid 4631   X. cxp 4838   ran crn 4841   |` cres 4842   -->wf 5414   -1-1->wf1 5415   -1-1-onto->wf1o 5417   ` cfv 5418  (class class class)co 6091   e. cmpt2 6093   ~~ cen 7307   Fincfn 7310   NN0cn0 10579   ^cexp 11865   #chash 12103   || cdivides 13535   Primecprime 13763   Basecbs 14174   +g cplusg 14238   0gc0g 14378   Grpcgrp 15410   GrpAct cga 15807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-er 7101  df-map 7216  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-card 8109  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-nn 10323  df-n0 10580  df-z 10647  df-uz 10862  df-hash 12104  df-0g 14380  df-mnd 15415  df-grp 15545  df-minusg 15546  df-ga 15808

This theorem is referenced by:  sylow1lem3  16099  sylow1lem5  16101