Metamath Proof Explorer

Theorem symgfixelsi

Description: The restriction of a permutation fixing an element to the set with this element removed is an element of the restricted symmetric group. (Contributed by AV, 4-Jan-2019)

Ref Expression
Hypotheses symgfixf.p 
|- P = ( Base ` ( SymGrp ` N ) )
symgfixf.q 
|- Q = { q e. P | ( q ` K ) = K }
symgfixf.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgfixf.d 
|- D = ( N \ { K } )
Assertion symgfixelsi 
|- ( ( K e. N /\ F e. Q ) -> ( F |` D ) e. S )

Proof

Step Hyp Ref Expression
1 symgfixf.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 symgfixf.q 
 |-  Q = { q e. P | ( q ` K ) = K }
3 symgfixf.s 
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
4 symgfixf.d 
 |-  D = ( N \ { K } )
5 1 2 symgfixelq 
 |-  ( F e. Q -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )
6 f1of1 
 |-  ( F : N -1-1-onto-> N -> F : N -1-1-> N )
7 6 ad2antrl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> F : N -1-1-> N )
8 difssd 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( N \ { K } ) C_ N )
9 f1ores 
 |-  ( ( F : N -1-1-> N /\ ( N \ { K } ) C_ N ) -> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) )
10 7 8 9 syl2anc 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) )
11 4 reseq2i 
 |-  ( F |` D ) = ( F |` ( N \ { K } ) )
12 11 a1i 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` D ) = ( F |` ( N \ { K } ) ) )
13 4 a1i 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> D = ( N \ { K } ) )
14 f1ofo 
 |-  ( F : N -1-1-onto-> N -> F : N -onto-> N )
15 foima 
 |-  ( F : N -onto-> N -> ( F " N ) = N )
16 15 eqcomd 
 |-  ( F : N -onto-> N -> N = ( F " N ) )
17 14 16 syl 
 |-  ( F : N -1-1-onto-> N -> N = ( F " N ) )
18 17 ad2antrl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> N = ( F " N ) )
19 sneq 
 |-  ( K = ( F ` K ) -> { K } = { ( F ` K ) } )
20 19 eqcoms 
 |-  ( ( F ` K ) = K -> { K } = { ( F ` K ) } )
21 20 ad2antll 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { K } = { ( F ` K ) } )
22 f1ofn 
 |-  ( F : N -1-1-onto-> N -> F Fn N )
23 22 ad2antrl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> F Fn N )
24 simpl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> K e. N )
25 fnsnfv 
 |-  ( ( F Fn N /\ K e. N ) -> { ( F ` K ) } = ( F " { K } ) )
26 23 24 25 syl2anc 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { ( F ` K ) } = ( F " { K } ) )
27 21 26 eqtrd 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { K } = ( F " { K } ) )
28 18 27 difeq12d 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( N \ { K } ) = ( ( F " N ) \ ( F " { K } ) ) )
29 dff1o2 
 |-  ( F : N -1-1-onto-> N <-> ( F Fn N /\ Fun `' F /\ ran F = N ) )
30 29 simp2bi 
 |-  ( F : N -1-1-onto-> N -> Fun `' F )
31 30 ad2antrl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> Fun `' F )
32 imadif 
 |-  ( Fun `' F -> ( F " ( N \ { K } ) ) = ( ( F " N ) \ ( F " { K } ) ) )
33 31 32 syl 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F " ( N \ { K } ) ) = ( ( F " N ) \ ( F " { K } ) ) )
34 28 13 33 3eqtr4d 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> D = ( F " ( N \ { K } ) ) )
35 12 13 34 f1oeq123d 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( ( F |` D ) : D -1-1-onto-> D <-> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) ) )
36 10 35 mpbird 
 |-  ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` D ) : D -1-1-onto-> D )
37 36 ancoms 
 |-  ( ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) /\ K e. N ) -> ( F |` D ) : D -1-1-onto-> D )
38 1 2 3 4 symgfixels 
 |-  ( F e. Q -> ( ( F |` D ) e. S <-> ( F |` D ) : D -1-1-onto-> D ) )
39 37 38 syl5ibr 
 |-  ( F e. Q -> ( ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) /\ K e. N ) -> ( F |` D ) e. S ) )
40 39 expd 
 |-  ( F e. Q -> ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) -> ( K e. N -> ( F |` D ) e. S ) ) )
41 5 40 sylbid 
 |-  ( F e. Q -> ( F e. Q -> ( K e. N -> ( F |` D ) e. S ) ) )
42 41 pm2.43i 
 |-  ( F e. Q -> ( K e. N -> ( F |` D ) e. S ) )
43 42 impcom 
 |-  ( ( K e. N /\ F e. Q ) -> ( F |` D ) e. S )