Metamath Proof Explorer

Theorem sylow2blem1

Description: Lemma for sylow2b . Evaluate the group action on a left coset. (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 sylow2blem1 
|- ( ( ph /\ B e. H /\ C e. X ) -> ( B .x. [ C ] .~ ) = [ ( B .+ C ) ] .~ )

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 simp2 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> B e. H )
9 6 ovexi 
 |-  .~ e. _V
10 simp3 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> C e. X )
11 ecelqsg 
 |-  ( ( .~ e. _V /\ C e. X ) -> [ C ] .~ e. ( X /. .~ ) )
12 9 10 11 sylancr 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ C ] .~ e. ( X /. .~ ) )
13 simpr 
 |-  ( ( x = B /\ y = [ C ] .~ ) -> y = [ C ] .~ )
14 simpl 
 |-  ( ( x = B /\ y = [ C ] .~ ) -> x = B )
15 14 oveq1d 
 |-  ( ( x = B /\ y = [ C ] .~ ) -> ( x .+ z ) = ( B .+ z ) )
16 13 15 mpteq12dv 
 |-  ( ( x = B /\ y = [ C ] .~ ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. [ C ] .~ |-> ( B .+ z ) ) )
17 16 rneqd 
 |-  ( ( x = B /\ y = [ C ] .~ ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
18 ecexg 
 |-  ( .~ e. _V -> [ C ] .~ e. _V )
19 9 18 ax-mp 
 |-  [ C ] .~ e. _V
20 19 mptex 
 |-  ( z e. [ C ] .~ |-> ( B .+ z ) ) e. _V
21 20 rnex 
 |-  ran ( z e. [ C ] .~ |-> ( B .+ z ) ) e. _V
22 17 7 21 ovmpoa 
 |-  ( ( B e. H /\ [ C ] .~ e. ( X /. .~ ) ) -> ( B .x. [ C ] .~ ) = ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
23 8 12 22 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( B .x. [ C ] .~ ) = ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
24 1 6 eqger 
 |-  ( K e. ( SubGrp ` G ) -> .~ Er X )
25 4 24 syl 
 |-  ( ph -> .~ Er X )
26 25 ecss 
 |-  ( ph -> [ ( B .+ C ) ] .~ C_ X )
27 2 26 ssfid 
 |-  ( ph -> [ ( B .+ C ) ] .~ e. Fin )
28 27 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ ( B .+ C ) ] .~ e. Fin )
29 vex 
 |-  z e. _V
30 elecg 
 |-  ( ( z e. _V /\ C e. X ) -> ( z e. [ C ] .~ <-> C .~ z ) )
31 29 10 30 sylancr 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. [ C ] .~ <-> C .~ z ) )
32 31 biimpa 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ z e. [ C ] .~ ) -> C .~ z )
33 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
34 3 33 syl 
 |-  ( ph -> G e. Grp )
35 34 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> G e. Grp )
36 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
37 3 36 syl 
 |-  ( ph -> H C_ X )
38 37 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> H C_ X )
39 38 8 sseldd 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> B e. X )
40 1 5 grpcl 
 |-  ( ( G e. Grp /\ B e. X /\ C e. X ) -> ( B .+ C ) e. X )
41 35 39 10 40 syl3anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( B .+ C ) e. X )
42 41 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( B .+ C ) e. X )
43 35 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> G e. Grp )
44 39 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> B e. X )
45 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
46 4 45 syl 
 |-  ( ph -> K C_ X )
47 eqid 
 |-  ( invg ` G ) = ( invg ` G )
48 1 47 5 6 eqgval 
 |-  ( ( G e. Grp /\ K C_ X ) -> ( C .~ z <-> ( C e. X /\ z e. X /\ ( ( ( invg ` G ) ` C ) .+ z ) e. K ) ) )
49 34 46 48 syl2anc 
 |-  ( ph -> ( C .~ z <-> ( C e. X /\ z e. X /\ ( ( ( invg ` G ) ` C ) .+ z ) e. K ) ) )
50 49 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( C .~ z <-> ( C e. X /\ z e. X /\ ( ( ( invg ` G ) ` C ) .+ z ) e. K ) ) )
51 50 biimpa 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( C e. X /\ z e. X /\ ( ( ( invg ` G ) ` C ) .+ z ) e. K ) )
52 51 simp2d 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> z e. X )
53 1 5 grpcl 
 |-  ( ( G e. Grp /\ B e. X /\ z e. X ) -> ( B .+ z ) e. X )
54 43 44 52 53 syl3anc 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( B .+ z ) e. X )
55 1 47 grpinvcl 
 |-  ( ( G e. Grp /\ ( B .+ C ) e. X ) -> ( ( invg ` G ) ` ( B .+ C ) ) e. X )
56 35 41 55 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( invg ` G ) ` ( B .+ C ) ) e. X )
57 56 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( invg ` G ) ` ( B .+ C ) ) e. X )
58 1 5 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` ( B .+ C ) ) e. X /\ B e. X /\ z e. X ) ) -> ( ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) .+ z ) = ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) )
59 43 57 44 52 58 syl13anc 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) .+ z ) = ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) )
60 1 5 47 grpinvadd 
 |-  ( ( G e. Grp /\ B e. X /\ C e. X ) -> ( ( invg ` G ) ` ( B .+ C ) ) = ( ( ( invg ` G ) ` C ) .+ ( ( invg ` G ) ` B ) ) )
61 35 39 10 60 syl3anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( invg ` G ) ` ( B .+ C ) ) = ( ( ( invg ` G ) ` C ) .+ ( ( invg ` G ) ` B ) ) )
62 1 47 grpinvcl 
 |-  ( ( G e. Grp /\ C e. X ) -> ( ( invg ` G ) ` C ) e. X )
63 35 10 62 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( invg ` G ) ` C ) e. X )
64 eqid 
 |-  ( -g ` G ) = ( -g ` G )
65 1 5 47 64 grpsubval 
 |-  ( ( ( ( invg ` G ) ` C ) e. X /\ B e. X ) -> ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) = ( ( ( invg ` G ) ` C ) .+ ( ( invg ` G ) ` B ) ) )
66 63 39 65 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) = ( ( ( invg ` G ) ` C ) .+ ( ( invg ` G ) ` B ) ) )
67 61 66 eqtr4d 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( invg ` G ) ` ( B .+ C ) ) = ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) )
68 67 oveq1d 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) = ( ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) .+ B ) )
69 1 5 64 grpnpcan 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` C ) e. X /\ B e. X ) -> ( ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) .+ B ) = ( ( invg ` G ) ` C ) )
70 35 63 39 69 syl3anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( ( invg ` G ) ` C ) ( -g ` G ) B ) .+ B ) = ( ( invg ` G ) ` C ) )
71 68 70 eqtrd 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) = ( ( invg ` G ) ` C ) )
72 71 oveq1d 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) .+ z ) = ( ( ( invg ` G ) ` C ) .+ z ) )
73 72 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( ( ( invg ` G ) ` ( B .+ C ) ) .+ B ) .+ z ) = ( ( ( invg ` G ) ` C ) .+ z ) )
74 59 73 eqtr3d 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) = ( ( ( invg ` G ) ` C ) .+ z ) )
75 51 simp3d 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( ( invg ` G ) ` C ) .+ z ) e. K )
76 74 75 eqeltrd 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) e. K )
77 1 47 5 6 eqgval 
 |-  ( ( G e. Grp /\ K C_ X ) -> ( ( B .+ C ) .~ ( B .+ z ) <-> ( ( B .+ C ) e. X /\ ( B .+ z ) e. X /\ ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) e. K ) ) )
78 34 46 77 syl2anc 
 |-  ( ph -> ( ( B .+ C ) .~ ( B .+ z ) <-> ( ( B .+ C ) e. X /\ ( B .+ z ) e. X /\ ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) e. K ) ) )
79 78 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( B .+ C ) .~ ( B .+ z ) <-> ( ( B .+ C ) e. X /\ ( B .+ z ) e. X /\ ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) e. K ) ) )
80 79 adantr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( ( B .+ C ) .~ ( B .+ z ) <-> ( ( B .+ C ) e. X /\ ( B .+ z ) e. X /\ ( ( ( invg ` G ) ` ( B .+ C ) ) .+ ( B .+ z ) ) e. K ) ) )
81 42 54 76 80 mpbir3and 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( B .+ C ) .~ ( B .+ z ) )
82 ovex 
 |-  ( B .+ z ) e. _V
83 ovex 
 |-  ( B .+ C ) e. _V
84 82 83 elec 
 |-  ( ( B .+ z ) e. [ ( B .+ C ) ] .~ <-> ( B .+ C ) .~ ( B .+ z ) )
85 81 84 sylibr 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ C .~ z ) -> ( B .+ z ) e. [ ( B .+ C ) ] .~ )
86 32 85 syldan 
 |-  ( ( ( ph /\ B e. H /\ C e. X ) /\ z e. [ C ] .~ ) -> ( B .+ z ) e. [ ( B .+ C ) ] .~ )
87 86 fmpttd 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ --> [ ( B .+ C ) ] .~ )
88 87 frnd 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) C_ [ ( B .+ C ) ] .~ )
89 eqid 
 |-  ( z e. X |-> ( B .+ z ) ) = ( z e. X |-> ( B .+ z ) )
90 1 5 89 grplmulf1o 
 |-  ( ( G e. Grp /\ B e. X ) -> ( z e. X |-> ( B .+ z ) ) : X -1-1-onto-> X )
91 35 39 90 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. X |-> ( B .+ z ) ) : X -1-1-onto-> X )
92 f1of1 
 |-  ( ( z e. X |-> ( B .+ z ) ) : X -1-1-onto-> X -> ( z e. X |-> ( B .+ z ) ) : X -1-1-> X )
93 91 92 syl 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. X |-> ( B .+ z ) ) : X -1-1-> X )
94 25 ecss 
 |-  ( ph -> [ C ] .~ C_ X )
95 94 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ C ] .~ C_ X )
96 f1ssres 
 |-  ( ( ( z e. X |-> ( B .+ z ) ) : X -1-1-> X /\ [ C ] .~ C_ X ) -> ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) : [ C ] .~ -1-1-> X )
97 93 95 96 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) : [ C ] .~ -1-1-> X )
98 resmpt 
 |-  ( [ C ] .~ C_ X -> ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) = ( z e. [ C ] .~ |-> ( B .+ z ) ) )
99 f1eq1 
 |-  ( ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) = ( z e. [ C ] .~ |-> ( B .+ z ) ) -> ( ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) : [ C ] .~ -1-1-> X <-> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-> X ) )
100 95 98 99 3syl 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( ( ( z e. X |-> ( B .+ z ) ) |` [ C ] .~ ) : [ C ] .~ -1-1-> X <-> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-> X ) )
101 97 100 mpbid 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-> X )
102 f1f1orn 
 |-  ( ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-> X -> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-onto-> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
103 101 102 syl 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-onto-> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
104 19 f1oen 
 |-  ( ( z e. [ C ] .~ |-> ( B .+ z ) ) : [ C ] .~ -1-1-onto-> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) -> [ C ] .~ ~~ ran ( z e. [ C ] .~ |-> ( B .+ z ) ) )
105 ensym 
 |-  ( [ C ] .~ ~~ ran ( z e. [ C ] .~ |-> ( B .+ z ) ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ C ] .~ )
106 103 104 105 3syl 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ C ] .~ )
107 4 3ad2ant1 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> K e. ( SubGrp ` G ) )
108 1 6 eqgen 
 |-  ( ( K e. ( SubGrp ` G ) /\ [ C ] .~ e. ( X /. .~ ) ) -> K ~~ [ C ] .~ )
109 107 12 108 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> K ~~ [ C ] .~ )
110 ensym 
 |-  ( K ~~ [ C ] .~ -> [ C ] .~ ~~ K )
111 109 110 syl 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ C ] .~ ~~ K )
112 ecelqsg 
 |-  ( ( .~ e. _V /\ ( B .+ C ) e. X ) -> [ ( B .+ C ) ] .~ e. ( X /. .~ ) )
113 9 41 112 sylancr 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ ( B .+ C ) ] .~ e. ( X /. .~ ) )
114 1 6 eqgen 
 |-  ( ( K e. ( SubGrp ` G ) /\ [ ( B .+ C ) ] .~ e. ( X /. .~ ) ) -> K ~~ [ ( B .+ C ) ] .~ )
115 107 113 114 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> K ~~ [ ( B .+ C ) ] .~ )
116 entr 
 |-  ( ( [ C ] .~ ~~ K /\ K ~~ [ ( B .+ C ) ] .~ ) -> [ C ] .~ ~~ [ ( B .+ C ) ] .~ )
117 111 115 116 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> [ C ] .~ ~~ [ ( B .+ C ) ] .~ )
118 entr 
 |-  ( ( ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ C ] .~ /\ [ C ] .~ ~~ [ ( B .+ C ) ] .~ ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ ( B .+ C ) ] .~ )
119 106 117 118 syl2anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ ( B .+ C ) ] .~ )
120 fisseneq 
 |-  ( ( [ ( B .+ C ) ] .~ e. Fin /\ ran ( z e. [ C ] .~ |-> ( B .+ z ) ) C_ [ ( B .+ C ) ] .~ /\ ran ( z e. [ C ] .~ |-> ( B .+ z ) ) ~~ [ ( B .+ C ) ] .~ ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) = [ ( B .+ C ) ] .~ )
121 28 88 119 120 syl3anc 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ran ( z e. [ C ] .~ |-> ( B .+ z ) ) = [ ( B .+ C ) ] .~ )
122 23 121 eqtrd 
 |-  ( ( ph /\ B e. H /\ C e. X ) -> ( B .x. [ C ] .~ ) = [ ( B .+ C ) ] .~ )