This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sylow2alem1

Description: Lemma for sylow2a . An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2a.x 
|- X = ( Base ` G )
sylow2a.m 
|- ( ph -> .(+) e. ( G GrpAct Y ) )
sylow2a.p 
|- ( ph -> P pGrp G )
sylow2a.f 
|- ( ph -> X e. Fin )
sylow2a.y 
|- ( ph -> Y e. Fin )
sylow2a.z 
|- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
sylow2a.r 
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion sylow2alem1 
|- ( ( ph /\ A e. Z ) -> [ A ] .~ = { A } )

Proof

Step Hyp Ref Expression
1 sylow2a.x 
 |-  X = ( Base ` G )
2 sylow2a.m 
 |-  ( ph -> .(+) e. ( G GrpAct Y ) )
3 sylow2a.p 
 |-  ( ph -> P pGrp G )
4 sylow2a.f 
 |-  ( ph -> X e. Fin )
5 sylow2a.y 
 |-  ( ph -> Y e. Fin )
6 sylow2a.z 
 |-  Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
7 sylow2a.r 
 |-  .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
8 vex 
 |-  w e. _V
9 simpr 
 |-  ( ( ph /\ A e. Z ) -> A e. Z )
10 elecg 
 |-  ( ( w e. _V /\ A e. Z ) -> ( w e. [ A ] .~ <-> A .~ w ) )
11 8 9 10 sylancr 
 |-  ( ( ph /\ A e. Z ) -> ( w e. [ A ] .~ <-> A .~ w ) )
12 7 gaorb 
 |-  ( A .~ w <-> ( A e. Y /\ w e. Y /\ E. k e. X ( k .(+) A ) = w ) )
13 12 simp3bi 
 |-  ( A .~ w -> E. k e. X ( k .(+) A ) = w )
14 oveq2 
 |-  ( u = A -> ( h .(+) u ) = ( h .(+) A ) )
15 id 
 |-  ( u = A -> u = A )
16 14 15 eqeq12d 
 |-  ( u = A -> ( ( h .(+) u ) = u <-> ( h .(+) A ) = A ) )
17 16 ralbidv 
 |-  ( u = A -> ( A. h e. X ( h .(+) u ) = u <-> A. h e. X ( h .(+) A ) = A ) )
18 17 6 elrab2 
 |-  ( A e. Z <-> ( A e. Y /\ A. h e. X ( h .(+) A ) = A ) )
19 9 18 sylib 
 |-  ( ( ph /\ A e. Z ) -> ( A e. Y /\ A. h e. X ( h .(+) A ) = A ) )
20 19 simprd 
 |-  ( ( ph /\ A e. Z ) -> A. h e. X ( h .(+) A ) = A )
21 oveq1 
 |-  ( h = k -> ( h .(+) A ) = ( k .(+) A ) )
22 21 eqeq1d 
 |-  ( h = k -> ( ( h .(+) A ) = A <-> ( k .(+) A ) = A ) )
23 22 rspccva 
 |-  ( ( A. h e. X ( h .(+) A ) = A /\ k e. X ) -> ( k .(+) A ) = A )
24 20 23 sylan 
 |-  ( ( ( ph /\ A e. Z ) /\ k e. X ) -> ( k .(+) A ) = A )
25 eqeq1 
 |-  ( ( k .(+) A ) = w -> ( ( k .(+) A ) = A <-> w = A ) )
26 24 25 syl5ibcom 
 |-  ( ( ( ph /\ A e. Z ) /\ k e. X ) -> ( ( k .(+) A ) = w -> w = A ) )
27 26 rexlimdva 
 |-  ( ( ph /\ A e. Z ) -> ( E. k e. X ( k .(+) A ) = w -> w = A ) )
28 13 27 syl5 
 |-  ( ( ph /\ A e. Z ) -> ( A .~ w -> w = A ) )
29 11 28 sylbid 
 |-  ( ( ph /\ A e. Z ) -> ( w e. [ A ] .~ -> w = A ) )
30 velsn 
 |-  ( w e. { A } <-> w = A )
31 29 30 imbitrrdi 
 |-  ( ( ph /\ A e. Z ) -> ( w e. [ A ] .~ -> w e. { A } ) )
32 31 ssrdv 
 |-  ( ( ph /\ A e. Z ) -> [ A ] .~ C_ { A } )
33 7 1 gaorber 
 |-  ( .(+) e. ( G GrpAct Y ) -> .~ Er Y )
34 2 33 syl 
 |-  ( ph -> .~ Er Y )
35 34 adantr 
 |-  ( ( ph /\ A e. Z ) -> .~ Er Y )
36 19 simpld 
 |-  ( ( ph /\ A e. Z ) -> A e. Y )
37 35 36 erref 
 |-  ( ( ph /\ A e. Z ) -> A .~ A )
38 elecg 
 |-  ( ( A e. Z /\ A e. Z ) -> ( A e. [ A ] .~ <-> A .~ A ) )
39 9 38 sylancom 
 |-  ( ( ph /\ A e. Z ) -> ( A e. [ A ] .~ <-> A .~ A ) )
40 37 39 mpbird 
 |-  ( ( ph /\ A e. Z ) -> A e. [ A ] .~ )
41 40 snssd 
 |-  ( ( ph /\ A e. Z ) -> { A } C_ [ A ] .~ )
42 32 41 eqssd 
 |-  ( ( ph /\ A e. Z ) -> [ A ] .~ = { A } )