Metamath Proof Explorer

Theorem sylow3lem5

Description: Lemma for sylow3 , second part. Reduce the group action of sylow3lem1 to a given Sylow subgroup. (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 ) ) )
Assertion sylow3lem5 
|- ( ph -> .(+) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )

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 slwsubg 
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
10 7 9 syl 
 |-  ( ph -> K e. ( SubGrp ` G ) )
11 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
12 10 11 syl 
 |-  ( ph -> K C_ X )
13 ssid 
 |-  ( P pSyl G ) C_ ( P pSyl G )
14 resmpo 
 |-  ( ( K C_ X /\ ( P pSyl G ) C_ ( P pSyl G ) ) -> ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |` ( K X. ( P pSyl G ) ) ) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) )
15 12 13 14 sylancl 
 |-  ( ph -> ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |` ( K X. ( P pSyl G ) ) ) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) )
16 15 8 eqtr4di 
 |-  ( ph -> ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |` ( K X. ( P pSyl G ) ) ) = .(+) )
17 oveq2 
 |-  ( z = c -> ( x .+ z ) = ( x .+ c ) )
18 17 oveq1d 
 |-  ( z = c -> ( ( x .+ z ) .- x ) = ( ( x .+ c ) .- x ) )
19 18 cbvmptv 
 |-  ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( c e. y |-> ( ( x .+ c ) .- x ) )
20 oveq1 
 |-  ( x = a -> ( x .+ c ) = ( a .+ c ) )
21 id 
 |-  ( x = a -> x = a )
22 20 21 oveq12d 
 |-  ( x = a -> ( ( x .+ c ) .- x ) = ( ( a .+ c ) .- a ) )
23 22 mpteq2dv 
 |-  ( x = a -> ( c e. y |-> ( ( x .+ c ) .- x ) ) = ( c e. y |-> ( ( a .+ c ) .- a ) ) )
24 19 23 eqtrid 
 |-  ( x = a -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( c e. y |-> ( ( a .+ c ) .- a ) ) )
25 24 rneqd 
 |-  ( x = a -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( c e. y |-> ( ( a .+ c ) .- a ) ) )
26 mpteq1 
 |-  ( y = b -> ( c e. y |-> ( ( a .+ c ) .- a ) ) = ( c e. b |-> ( ( a .+ c ) .- a ) ) )
27 26 rneqd 
 |-  ( y = b -> ran ( c e. y |-> ( ( a .+ c ) .- a ) ) = ran ( c e. b |-> ( ( a .+ c ) .- a ) ) )
28 25 27 cbvmpov 
 |-  ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) = ( a e. X , b e. ( P pSyl G ) |-> ran ( c e. b |-> ( ( a .+ c ) .- a ) ) )
29 1 2 3 4 5 6 28 sylow3lem1 
 |-  ( ph -> ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) e. ( G GrpAct ( P pSyl G ) ) )
30 eqid 
 |-  ( G |`s K ) = ( G |`s K )
31 30 gasubg 
 |-  ( ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) e. ( G GrpAct ( P pSyl G ) ) /\ K e. ( SubGrp ` G ) ) -> ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |` ( K X. ( P pSyl G ) ) ) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )
32 29 10 31 syl2anc 
 |-  ( ph -> ( ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |` ( K X. ( P pSyl G ) ) ) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )
33 16 32 eqeltrrd 
 |-  ( ph -> .(+) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )