Metamath Proof Explorer

Theorem cayleylem2

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cayleylem1.x 
|- X = ( Base ` G )
cayleylem1.p 
|- .+ = ( +g ` G )
cayleylem1.u 
|- .0. = ( 0g ` G )
cayleylem1.h 
|- H = ( SymGrp ` X )
cayleylem1.s 
|- S = ( Base ` H )
cayleylem1.f 
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
Assertion cayleylem2 
|- ( G e. Grp -> F : X -1-1-> S )

Proof

Step Hyp Ref Expression
1 cayleylem1.x 
 |-  X = ( Base ` G )
2 cayleylem1.p 
 |-  .+ = ( +g ` G )
3 cayleylem1.u 
 |-  .0. = ( 0g ` G )
4 cayleylem1.h 
 |-  H = ( SymGrp ` X )
5 cayleylem1.s 
 |-  S = ( Base ` H )
6 cayleylem1.f 
 |-  F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
7 fveq1 
 |-  ( ( F ` x ) = ( 0g ` H ) -> ( ( F ` x ) ` .0. ) = ( ( 0g ` H ) ` .0. ) )
8 simpr 
 |-  ( ( G e. Grp /\ x e. X ) -> x e. X )
9 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
10 9 adantr 
 |-  ( ( G e. Grp /\ x e. X ) -> .0. e. X )
11 6 1 grplactval 
 |-  ( ( x e. X /\ .0. e. X ) -> ( ( F ` x ) ` .0. ) = ( x .+ .0. ) )
12 8 10 11 syl2anc 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) ` .0. ) = ( x .+ .0. ) )
13 1 2 3 grprid 
 |-  ( ( G e. Grp /\ x e. X ) -> ( x .+ .0. ) = x )
14 12 13 eqtrd 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) ` .0. ) = x )
15 1 fvexi 
 |-  X e. _V
16 4 symgid 
 |-  ( X e. _V -> ( _I |` X ) = ( 0g ` H ) )
17 15 16 ax-mp 
 |-  ( _I |` X ) = ( 0g ` H )
18 17 fveq1i 
 |-  ( ( _I |` X ) ` .0. ) = ( ( 0g ` H ) ` .0. )
19 fvresi 
 |-  ( .0. e. X -> ( ( _I |` X ) ` .0. ) = .0. )
20 10 19 syl 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( _I |` X ) ` .0. ) = .0. )
21 18 20 eqtr3id 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( 0g ` H ) ` .0. ) = .0. )
22 14 21 eqeq12d 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( ( F ` x ) ` .0. ) = ( ( 0g ` H ) ` .0. ) <-> x = .0. ) )
23 7 22 imbitrid 
 |-  ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) )
24 23 ralrimiva 
 |-  ( G e. Grp -> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) )
25 1 2 3 4 5 6 cayleylem1 
 |-  ( G e. Grp -> F e. ( G GrpHom H ) )
26 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
27 1 5 3 26 ghmf1 
 |-  ( F e. ( G GrpHom H ) -> ( F : X -1-1-> S <-> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) ) )
28 25 27 syl 
 |-  ( G e. Grp -> ( F : X -1-1-> S <-> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) ) )
29 24 28 mpbird 
 |-  ( G e. Grp -> F : X -1-1-> S )