Theorem sylow3lem6

Description: Lemma for sylow3 , second part. Using the lemma sylow2a , show that the number of sylow subgroups is equivalent mod P to the number of fixed points under the group action. But K is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ( ( #( P pSyl G ) ) mod P ) = 1 . (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	|- X = ( Base ` G )
	sylow3.g	|- ( ph -> G e. Grp )
	sylow3.xf	|- ( ph -> X e. Fin )
	sylow3.p	|- ( ph -> P e. Prime )
	sylow3lem5.a	|- .+ = ( +g ` G )
	sylow3lem5.d	|- .- = ( -g ` G )
	sylow3lem5.k	|- ( ph -> K e. ( P pSyl G ) )
	sylow3lem5.m	|- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
	sylow3lem6.n	|- N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) }
Assertion	sylow3lem6	|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	|- X = ( Base ` G )
2		sylow3.g	|- ( ph -> G e. Grp )
3		sylow3.xf	|- ( ph -> X e. Fin )
4		sylow3.p	|- ( ph -> P e. Prime )
5		sylow3lem5.a	|- .+ = ( +g ` G )
6		sylow3lem5.d	|- .- = ( -g ` G )
7		sylow3lem5.k	|- ( ph -> K e. ( P pSyl G ) )
8		sylow3lem5.m	|- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
9		sylow3lem6.n	|- N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) }
10		eqid	|- ( Base ` ( G |`s K ) ) = ( Base ` ( G |`s K ) )
11	1 2 3 4 5 6 7 8	sylow3lem5	|- ( ph -> .(+) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )
12		eqid	|- ( G |`s K ) = ( G |`s K )
13	12	slwpgp	|- ( K e. ( P pSyl G ) -> P pGrp ( G |`s K ) )
14	7 13	syl	|- ( ph -> P pGrp ( G |`s K ) )
15		slwsubg	|- ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
16	7 15	syl	|- ( ph -> K e. ( SubGrp ` G ) )
17	12	subgbas	|- ( K e. ( SubGrp ` G ) -> K = ( Base ` ( G |`s K ) ) )
18	16 17	syl	|- ( ph -> K = ( Base ` ( G |`s K ) ) )
19	1	subgss	|- ( K e. ( SubGrp ` G ) -> K C_ X )
20	16 19	syl	|- ( ph -> K C_ X )
21	3 20	ssfid	|- ( ph -> K e. Fin )
22	18 21	eqeltrrd	|- ( ph -> ( Base ` ( G |`s K ) ) e. Fin )
23		pwfi	|- ( X e. Fin <-> ~P X e. Fin )
24	3 23	sylib	|- ( ph -> ~P X e. Fin )
25		slwsubg	|- ( x e. ( P pSyl G ) -> x e. ( SubGrp ` G ) )
26	1	subgss	|- ( x e. ( SubGrp ` G ) -> x C_ X )
27	25 26	syl	|- ( x e. ( P pSyl G ) -> x C_ X )
28	25 27	elpwd	|- ( x e. ( P pSyl G ) -> x e. ~P X )
29	28	ssriv	|- ( P pSyl G ) C_ ~P X
30		ssfi	|- ( ( ~P X e. Fin /\ ( P pSyl G ) C_ ~P X ) -> ( P pSyl G ) e. Fin )
31	24 29 30	sylancl	|- ( ph -> ( P pSyl G ) e. Fin )
32		eqid	|- { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s }
33		eqid	|- { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) } = { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) }
34	10 11 14 22 31 32 33	sylow2a	|- ( ph -> P || ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) )
35		eqcom	|- ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
36	20	adantr	|- ( ( ph /\ s e. ( P pSyl G ) ) -> K C_ X )
37	36	sselda	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. X )
38	37	biantrurd	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
39	35 38	bitrid	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
40		simpr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. K )
41		simplr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( P pSyl G ) )
42		simpr	|- ( ( x = g /\ y = s ) -> y = s )
43		simpl	|- ( ( x = g /\ y = s ) -> x = g )
44	43	oveq1d	|- ( ( x = g /\ y = s ) -> ( x .+ z ) = ( g .+ z ) )
45	44 43	oveq12d	|- ( ( x = g /\ y = s ) -> ( ( x .+ z ) .- x ) = ( ( g .+ z ) .- g ) )
46	42 45	mpteq12dv	|- ( ( x = g /\ y = s ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) ) )
47	46	rneqd	|- ( ( x = g /\ y = s ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
48		vex	|- s e. _V
49	48	mptex	|- ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V
50	49	rnex	|- ran ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V
51	47 8 50	ovmpoa	|- ( ( g e. K /\ s e. ( P pSyl G ) ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
52	40 41 51	syl2anc	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
53	52	eqeq1d	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s ) )
54		slwsubg	|- ( s e. ( P pSyl G ) -> s e. ( SubGrp ` G ) )
55	54	ad2antlr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( SubGrp ` G ) )
56		eqid	|- ( z e. s |-> ( ( g .+ z ) .- g ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) )
57	1 5 6 56 9	conjnmzb	|- ( s e. ( SubGrp ` G ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
58	55 57	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
59	39 53 58	3bitr4d	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> g e. N ) )
60	59	ralbidva	|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. K g e. N ) )
61		dfss3	|- ( K C_ N <-> A. g e. K g e. N )
62	60 61	bitr4di	|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> K C_ N ) )
63	18	adantr	|- ( ( ph /\ s e. ( P pSyl G ) ) -> K = ( Base ` ( G |`s K ) ) )
64	63	raleqdv	|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s ) )
65		eqid	|- ( Base ` ( G |`s N ) ) = ( Base ` ( G |`s N ) )
66	2	ad2antrr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> G e. Grp )
67	9 1 5	nmzsubg	|- ( G e. Grp -> N e. ( SubGrp ` G ) )
68	66 67	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. ( SubGrp ` G ) )
69		eqid	|- ( G |`s N ) = ( G |`s N )
70	69	subgbas	|- ( N e. ( SubGrp ` G ) -> N = ( Base ` ( G |`s N ) ) )
71	68 70	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N = ( Base ` ( G |`s N ) ) )
72	3	ad2antrr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> X e. Fin )
73	1	subgss	|- ( N e. ( SubGrp ` G ) -> N C_ X )
74	68 73	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N C_ X )
75	72 74	ssfid	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. Fin )
76	71 75	eqeltrrd	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( Base ` ( G |`s N ) ) e. Fin )
77	7	ad2antrr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl G ) )
78		simpr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K C_ N )
79	69	subgslw	|- ( ( N e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) )
80	68 77 78 79	syl3anc	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) )
81		simplr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl G ) )
82	54	ad2antlr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( SubGrp ` G ) )
83	9 1 5	ssnmz	|- ( s e. ( SubGrp ` G ) -> s C_ N )
84	82 83	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s C_ N )
85	69	subgslw	|- ( ( N e. ( SubGrp ` G ) /\ s e. ( P pSyl G ) /\ s C_ N ) -> s e. ( P pSyl ( G |`s N ) ) )
86	68 81 84 85	syl3anc	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl ( G |`s N ) ) )
87	1	fvexi	|- X e. _V
88	9 87	rabex2	|- N e. _V
89	69 5	ressplusg	|- ( N e. _V -> .+ = ( +g ` ( G |`s N ) ) )
90	88 89	ax-mp	|- .+ = ( +g ` ( G |`s N ) )
91		eqid	|- ( -g ` ( G |`s N ) ) = ( -g ` ( G |`s N ) )
92	65 76 80 86 90 91	sylow2	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
93	9 1 5 69	nmznsg	|- ( s e. ( SubGrp ` G ) -> s e. ( NrmSGrp ` ( G |`s N ) ) )
94	82 93	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( NrmSGrp ` ( G |`s N ) ) )
95		eqid	|- ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) = ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) )
96	65 90 91 95	conjnsg	|- ( ( s e. ( NrmSGrp ` ( G |`s N ) ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
97	94 96	sylan	|- ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
98		eqeq2	|- ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> ( s = K <-> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) )
99	97 98	syl5ibrcom	|- ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) )
100	99	rexlimdva	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) )
101	92 100	mpd	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s = K )
102		simpr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s = K )
103	16	ad2antrr	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K e. ( SubGrp ` G ) )
104	102 103	eqeltrd	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s e. ( SubGrp ` G ) )
105	104 83	syl	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s C_ N )
106	102 105	eqsstrrd	|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K C_ N )
107	101 106	impbida	|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( K C_ N <-> s = K ) )
108	62 64 107	3bitr3d	|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s <-> s = K ) )
109	108	rabbidva	|- ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | s = K } )
110		rabsn	|- ( K e. ( P pSyl G ) -> { s e. ( P pSyl G ) | s = K } = { K } )
111	7 110	syl	|- ( ph -> { s e. ( P pSyl G ) | s = K } = { K } )
112	109 111	eqtrd	|- ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { K } )
113	112	fveq2d	|- ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = ( # ` { K } ) )
114		hashsng	|- ( K e. ( P pSyl G ) -> ( # ` { K } ) = 1 )
115	7 114	syl	|- ( ph -> ( # ` { K } ) = 1 )
116	113 115	eqtrd	|- ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = 1 )
117	116	oveq2d	|- ( ph -> ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) = ( ( # ` ( P pSyl G ) ) - 1 ) )
118	34 117	breqtrd	|- ( ph -> P || ( ( # ` ( P pSyl G ) ) - 1 ) )
119		prmnn	|- ( P e. Prime -> P e. NN )
120	4 119	syl	|- ( ph -> P e. NN )
121		hashcl	|- ( ( P pSyl G ) e. Fin -> ( # ` ( P pSyl G ) ) e. NN0 )
122	31 121	syl	|- ( ph -> ( # ` ( P pSyl G ) ) e. NN0 )
123	122	nn0zd	|- ( ph -> ( # ` ( P pSyl G ) ) e. ZZ )
124		1zzd	|- ( ph -> 1 e. ZZ )
125		moddvds	|- ( ( P e. NN /\ ( # ` ( P pSyl G ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) )
126	120 123 124 125	syl3anc	|- ( ph -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) )
127	118 126	mpbird	|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) )
128		prmuz2	|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
129		eluz2b2	|- ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) )
130		nnre	|- ( P e. NN -> P e. RR )
131		1mod	|- ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
132	130 131	sylan	|- ( ( P e. NN /\ 1 < P ) -> ( 1 mod P ) = 1 )
133	129 132	sylbi	|- ( P e. ( ZZ>= ` 2 ) -> ( 1 mod P ) = 1 )
134	4 128 133	3syl	|- ( ph -> ( 1 mod P ) = 1 )
135	127 134	eqtrd	|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )