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 ) ] .~ )