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 )