Metamath Proof Explorer

Theorem sylow2blem2

Description: Lemma for sylow2b . Left multiplication in a subgroup H is a group action on the set of all left cosets of K . (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2b.x 
|- X = ( Base ` G )
sylow2b.xf 
|- ( ph -> X e. Fin )
sylow2b.h 
|- ( ph -> H e. ( SubGrp ` G ) )
sylow2b.k 
|- ( ph -> K e. ( SubGrp ` G ) )
sylow2b.a 
|- .+ = ( +g ` G )
sylow2b.r 
|- .~ = ( G ~QG K )
sylow2b.m 
|- .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )
Assertion sylow2blem2 
|- ( ph -> .x. e. ( ( G |`s H ) GrpAct ( X /. .~ ) ) )

Proof

Step Hyp Ref Expression
1 sylow2b.x 
 |-  X = ( Base ` G )
2 sylow2b.xf 
 |-  ( ph -> X e. Fin )
3 sylow2b.h 
 |-  ( ph -> H e. ( SubGrp ` G ) )
4 sylow2b.k 
 |-  ( ph -> K e. ( SubGrp ` G ) )
5 sylow2b.a 
 |-  .+ = ( +g ` G )
6 sylow2b.r 
 |-  .~ = ( G ~QG K )
7 sylow2b.m 
 |-  .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )
8 eqid 
 |-  ( G |`s H ) = ( G |`s H )
9 8 subggrp 
 |-  ( H e. ( SubGrp ` G ) -> ( G |`s H ) e. Grp )
10 3 9 syl 
 |-  ( ph -> ( G |`s H ) e. Grp )
11 pwfi 
 |-  ( X e. Fin <-> ~P X e. Fin )
12 2 11 sylib 
 |-  ( ph -> ~P X e. Fin )
13 1 6 eqger 
 |-  ( K e. ( SubGrp ` G ) -> .~ Er X )
14 4 13 syl 
 |-  ( ph -> .~ Er X )
15 14 qsss 
 |-  ( ph -> ( X /. .~ ) C_ ~P X )
16 12 15 ssexd 
 |-  ( ph -> ( X /. .~ ) e. _V )
17 10 16 jca 
 |-  ( ph -> ( ( G |`s H ) e. Grp /\ ( X /. .~ ) e. _V ) )
18 vex 
 |-  y e. _V
19 18 mptex 
 |-  ( z e. y |-> ( x .+ z ) ) e. _V
20 19 rnex 
 |-  ran ( z e. y |-> ( x .+ z ) ) e. _V
21 7 20 fnmpoi 
 |-  .x. Fn ( H X. ( X /. .~ ) )
22 21 a1i 
 |-  ( ph -> .x. Fn ( H X. ( X /. .~ ) ) )
23 eqid 
 |-  ( X /. .~ ) = ( X /. .~ )
24 oveq2 
 |-  ( [ s ] .~ = v -> ( u .x. [ s ] .~ ) = ( u .x. v ) )
25 24 eleq1d 
 |-  ( [ s ] .~ = v -> ( ( u .x. [ s ] .~ ) e. ( X /. .~ ) <-> ( u .x. v ) e. ( X /. .~ ) ) )
26 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> ( u .x. [ s ] .~ ) = [ ( u .+ s ) ] .~ )
27 6 ovexi 
 |-  .~ e. _V
28 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
29 3 28 syl 
 |-  ( ph -> G e. Grp )
30 29 3ad2ant1 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> G e. Grp )
31 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
32 3 31 syl 
 |-  ( ph -> H C_ X )
33 32 sselda 
 |-  ( ( ph /\ u e. H ) -> u e. X )
34 33 3adant3 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> u e. X )
35 simp3 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> s e. X )
36 1 5 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ s e. X ) -> ( u .+ s ) e. X )
37 30 34 35 36 syl3anc 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> ( u .+ s ) e. X )
38 ecelqsg 
 |-  ( ( .~ e. _V /\ ( u .+ s ) e. X ) -> [ ( u .+ s ) ] .~ e. ( X /. .~ ) )
39 27 37 38 sylancr 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> [ ( u .+ s ) ] .~ e. ( X /. .~ ) )
40 26 39 eqeltrd 
 |-  ( ( ph /\ u e. H /\ s e. X ) -> ( u .x. [ s ] .~ ) e. ( X /. .~ ) )
41 40 3expa 
 |-  ( ( ( ph /\ u e. H ) /\ s e. X ) -> ( u .x. [ s ] .~ ) e. ( X /. .~ ) )
42 23 25 41 ectocld 
 |-  ( ( ( ph /\ u e. H ) /\ v e. ( X /. .~ ) ) -> ( u .x. v ) e. ( X /. .~ ) )
43 42 ralrimiva 
 |-  ( ( ph /\ u e. H ) -> A. v e. ( X /. .~ ) ( u .x. v ) e. ( X /. .~ ) )
44 43 ralrimiva 
 |-  ( ph -> A. u e. H A. v e. ( X /. .~ ) ( u .x. v ) e. ( X /. .~ ) )
45 ffnov 
 |-  ( .x. : ( H X. ( X /. .~ ) ) --> ( X /. .~ ) <-> ( .x. Fn ( H X. ( X /. .~ ) ) /\ A. u e. H A. v e. ( X /. .~ ) ( u .x. v ) e. ( X /. .~ ) ) )
46 22 44 45 sylanbrc 
 |-  ( ph -> .x. : ( H X. ( X /. .~ ) ) --> ( X /. .~ ) )
47 8 subgbas 
 |-  ( H e. ( SubGrp ` G ) -> H = ( Base ` ( G |`s H ) ) )
48 3 47 syl 
 |-  ( ph -> H = ( Base ` ( G |`s H ) ) )
49 48 xpeq1d 
 |-  ( ph -> ( H X. ( X /. .~ ) ) = ( ( Base ` ( G |`s H ) ) X. ( X /. .~ ) ) )
50 49 feq2d 
 |-  ( ph -> ( .x. : ( H X. ( X /. .~ ) ) --> ( X /. .~ ) <-> .x. : ( ( Base ` ( G |`s H ) ) X. ( X /. .~ ) ) --> ( X /. .~ ) ) )
51 46 50 mpbid 
 |-  ( ph -> .x. : ( ( Base ` ( G |`s H ) ) X. ( X /. .~ ) ) --> ( X /. .~ ) )
52 oveq2 
 |-  ( [ s ] .~ = u -> ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) = ( ( 0g ` ( G |`s H ) ) .x. u ) )
53 id 
 |-  ( [ s ] .~ = u -> [ s ] .~ = u )
54 52 53 eqeq12d 
 |-  ( [ s ] .~ = u -> ( ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) = [ s ] .~ <-> ( ( 0g ` ( G |`s H ) ) .x. u ) = u ) )
55 oveq2 
 |-  ( [ s ] .~ = u -> ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) )
56 oveq2 
 |-  ( [ s ] .~ = u -> ( b .x. [ s ] .~ ) = ( b .x. u ) )
57 56 oveq2d 
 |-  ( [ s ] .~ = u -> ( a .x. ( b .x. [ s ] .~ ) ) = ( a .x. ( b .x. u ) ) )
58 55 57 eqeq12d 
 |-  ( [ s ] .~ = u -> ( ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) <-> ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) )
59 58 2ralbidv 
 |-  ( [ s ] .~ = u -> ( A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) <-> A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) )
60 54 59 anbi12d 
 |-  ( [ s ] .~ = u -> ( ( ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) = [ s ] .~ /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) ) <-> ( ( ( 0g ` ( G |`s H ) ) .x. u ) = u /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) ) )
61 simpl 
 |-  ( ( ph /\ s e. X ) -> ph )
62 3 adantr 
 |-  ( ( ph /\ s e. X ) -> H e. ( SubGrp ` G ) )
63 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
64 63 subg0cl 
 |-  ( H e. ( SubGrp ` G ) -> ( 0g ` G ) e. H )
65 62 64 syl 
 |-  ( ( ph /\ s e. X ) -> ( 0g ` G ) e. H )
66 simpr 
 |-  ( ( ph /\ s e. X ) -> s e. X )
67 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ ( 0g ` G ) e. H /\ s e. X ) -> ( ( 0g ` G ) .x. [ s ] .~ ) = [ ( ( 0g ` G ) .+ s ) ] .~ )
68 61 65 66 67 syl3anc 
 |-  ( ( ph /\ s e. X ) -> ( ( 0g ` G ) .x. [ s ] .~ ) = [ ( ( 0g ` G ) .+ s ) ] .~ )
69 8 63 subg0 
 |-  ( H e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` ( G |`s H ) ) )
70 62 69 syl 
 |-  ( ( ph /\ s e. X ) -> ( 0g ` G ) = ( 0g ` ( G |`s H ) ) )
71 70 oveq1d 
 |-  ( ( ph /\ s e. X ) -> ( ( 0g ` G ) .x. [ s ] .~ ) = ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) )
72 1 5 63 grplid 
 |-  ( ( G e. Grp /\ s e. X ) -> ( ( 0g ` G ) .+ s ) = s )
73 29 72 sylan 
 |-  ( ( ph /\ s e. X ) -> ( ( 0g ` G ) .+ s ) = s )
74 73 eceq1d 
 |-  ( ( ph /\ s e. X ) -> [ ( ( 0g ` G ) .+ s ) ] .~ = [ s ] .~ )
75 68 71 74 3eqtr3d 
 |-  ( ( ph /\ s e. X ) -> ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) = [ s ] .~ )
76 62 adantr 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> H e. ( SubGrp ` G ) )
77 76 28 syl 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> G e. Grp )
78 76 31 syl 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> H C_ X )
79 simprl 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> a e. H )
80 78 79 sseldd 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> a e. X )
81 simprr 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> b e. H )
82 78 81 sseldd 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> b e. X )
83 66 adantr 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> s e. X )
84 1 5 grpass 
 |-  ( ( G e. Grp /\ ( a e. X /\ b e. X /\ s e. X ) ) -> ( ( a .+ b ) .+ s ) = ( a .+ ( b .+ s ) ) )
85 77 80 82 83 84 syl13anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( ( a .+ b ) .+ s ) = ( a .+ ( b .+ s ) ) )
86 85 eceq1d 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> [ ( ( a .+ b ) .+ s ) ] .~ = [ ( a .+ ( b .+ s ) ) ] .~ )
87 61 adantr 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ph )
88 1 5 grpcl 
 |-  ( ( G e. Grp /\ b e. X /\ s e. X ) -> ( b .+ s ) e. X )
89 77 82 83 88 syl3anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( b .+ s ) e. X )
90 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ a e. H /\ ( b .+ s ) e. X ) -> ( a .x. [ ( b .+ s ) ] .~ ) = [ ( a .+ ( b .+ s ) ) ] .~ )
91 87 79 89 90 syl3anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( a .x. [ ( b .+ s ) ] .~ ) = [ ( a .+ ( b .+ s ) ) ] .~ )
92 86 91 eqtr4d 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> [ ( ( a .+ b ) .+ s ) ] .~ = ( a .x. [ ( b .+ s ) ] .~ ) )
93 5 subgcl 
 |-  ( ( H e. ( SubGrp ` G ) /\ a e. H /\ b e. H ) -> ( a .+ b ) e. H )
94 76 79 81 93 syl3anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( a .+ b ) e. H )
95 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ ( a .+ b ) e. H /\ s e. X ) -> ( ( a .+ b ) .x. [ s ] .~ ) = [ ( ( a .+ b ) .+ s ) ] .~ )
96 87 94 83 95 syl3anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( ( a .+ b ) .x. [ s ] .~ ) = [ ( ( a .+ b ) .+ s ) ] .~ )
97 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ b e. H /\ s e. X ) -> ( b .x. [ s ] .~ ) = [ ( b .+ s ) ] .~ )
98 87 81 83 97 syl3anc 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( b .x. [ s ] .~ ) = [ ( b .+ s ) ] .~ )
99 98 oveq2d 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( a .x. ( b .x. [ s ] .~ ) ) = ( a .x. [ ( b .+ s ) ] .~ ) )
100 92 96 99 3eqtr4d 
 |-  ( ( ( ph /\ s e. X ) /\ ( a e. H /\ b e. H ) ) -> ( ( a .+ b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) )
101 100 ralrimivva 
 |-  ( ( ph /\ s e. X ) -> A. a e. H A. b e. H ( ( a .+ b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) )
102 62 47 syl 
 |-  ( ( ph /\ s e. X ) -> H = ( Base ` ( G |`s H ) ) )
103 8 5 ressplusg 
 |-  ( H e. ( SubGrp ` G ) -> .+ = ( +g ` ( G |`s H ) ) )
104 3 103 syl 
 |-  ( ph -> .+ = ( +g ` ( G |`s H ) ) )
105 104 oveqdr 
 |-  ( ( ph /\ s e. X ) -> ( a .+ b ) = ( a ( +g ` ( G |`s H ) ) b ) )
106 105 oveq1d 
 |-  ( ( ph /\ s e. X ) -> ( ( a .+ b ) .x. [ s ] .~ ) = ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) )
107 106 eqeq1d 
 |-  ( ( ph /\ s e. X ) -> ( ( ( a .+ b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) <-> ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) ) )
108 102 107 raleqbidv 
 |-  ( ( ph /\ s e. X ) -> ( A. b e. H ( ( a .+ b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) <-> A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) ) )
109 102 108 raleqbidv 
 |-  ( ( ph /\ s e. X ) -> ( A. a e. H A. b e. H ( ( a .+ b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) <-> A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) ) )
110 101 109 mpbid 
 |-  ( ( ph /\ s e. X ) -> A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) )
111 75 110 jca 
 |-  ( ( ph /\ s e. X ) -> ( ( ( 0g ` ( G |`s H ) ) .x. [ s ] .~ ) = [ s ] .~ /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. [ s ] .~ ) = ( a .x. ( b .x. [ s ] .~ ) ) ) )
112 23 60 111 ectocld 
 |-  ( ( ph /\ u e. ( X /. .~ ) ) -> ( ( ( 0g ` ( G |`s H ) ) .x. u ) = u /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) )
113 112 ralrimiva 
 |-  ( ph -> A. u e. ( X /. .~ ) ( ( ( 0g ` ( G |`s H ) ) .x. u ) = u /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) )
114 51 113 jca 
 |-  ( ph -> ( .x. : ( ( Base ` ( G |`s H ) ) X. ( X /. .~ ) ) --> ( X /. .~ ) /\ A. u e. ( X /. .~ ) ( ( ( 0g ` ( G |`s H ) ) .x. u ) = u /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) ) )
115 eqid 
 |-  ( Base ` ( G |`s H ) ) = ( Base ` ( G |`s H ) )
116 eqid 
 |-  ( +g ` ( G |`s H ) ) = ( +g ` ( G |`s H ) )
117 eqid 
 |-  ( 0g ` ( G |`s H ) ) = ( 0g ` ( G |`s H ) )
118 115 116 117 isga 
 |-  ( .x. e. ( ( G |`s H ) GrpAct ( X /. .~ ) ) <-> ( ( ( G |`s H ) e. Grp /\ ( X /. .~ ) e. _V ) /\ ( .x. : ( ( Base ` ( G |`s H ) ) X. ( X /. .~ ) ) --> ( X /. .~ ) /\ A. u e. ( X /. .~ ) ( ( ( 0g ` ( G |`s H ) ) .x. u ) = u /\ A. a e. ( Base ` ( G |`s H ) ) A. b e. ( Base ` ( G |`s H ) ) ( ( a ( +g ` ( G |`s H ) ) b ) .x. u ) = ( a .x. ( b .x. u ) ) ) ) ) )
119 17 114 118 sylanbrc 
 |-  ( ph -> .x. e. ( ( G |`s H ) GrpAct ( X /. .~ ) ) )