Metamath Proof Explorer

Theorem symgfixf1

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a 1-1 function. (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.h 
|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
Assertion symgfixf1 
|- ( K e. N -> H : Q -1-1-> 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.h 
 |-  H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
5 1 2 3 4 symgfixf 
 |-  ( K e. N -> H : Q --> S )
6 4 fvtresfn 
 |-  ( g e. Q -> ( H ` g ) = ( g |` ( N \ { K } ) ) )
7 4 fvtresfn 
 |-  ( p e. Q -> ( H ` p ) = ( p |` ( N \ { K } ) ) )
8 6 7 eqeqan12d 
 |-  ( ( g e. Q /\ p e. Q ) -> ( ( H ` g ) = ( H ` p ) <-> ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) ) )
9 8 adantl 
 |-  ( ( K e. N /\ ( g e. Q /\ p e. Q ) ) -> ( ( H ` g ) = ( H ` p ) <-> ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) ) )
10 1 2 symgfixelq 
 |-  ( g e. _V -> ( g e. Q <-> ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) ) )
11 10 elv 
 |-  ( g e. Q <-> ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) )
12 1 2 symgfixelq 
 |-  ( p e. _V -> ( p e. Q <-> ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) )
13 12 elv 
 |-  ( p e. Q <-> ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) )
14 11 13 anbi12i 
 |-  ( ( g e. Q /\ p e. Q ) <-> ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) )
15 f1ofn 
 |-  ( g : N -1-1-onto-> N -> g Fn N )
16 15 adantr 
 |-  ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) -> g Fn N )
17 f1ofn 
 |-  ( p : N -1-1-onto-> N -> p Fn N )
18 17 adantr 
 |-  ( ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) -> p Fn N )
19 16 18 anim12i 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> ( g Fn N /\ p Fn N ) )
20 difss 
 |-  ( N \ { K } ) C_ N
21 19 20 jctir 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> ( ( g Fn N /\ p Fn N ) /\ ( N \ { K } ) C_ N ) )
22 21 adantl 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> ( ( g Fn N /\ p Fn N ) /\ ( N \ { K } ) C_ N ) )
23 fvreseq 
 |-  ( ( ( g Fn N /\ p Fn N ) /\ ( N \ { K } ) C_ N ) -> ( ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) <-> A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) )
24 22 23 syl 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> ( ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) <-> A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) )
25 f1of 
 |-  ( g : N -1-1-onto-> N -> g : N --> N )
26 25 adantr 
 |-  ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) -> g : N --> N )
27 f1of 
 |-  ( p : N -1-1-onto-> N -> p : N --> N )
28 27 adantr 
 |-  ( ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) -> p : N --> N )
29 fdm 
 |-  ( g : N --> N -> dom g = N )
30 fdm 
 |-  ( p : N --> N -> dom p = N )
31 29 30 anim12i 
 |-  ( ( g : N --> N /\ p : N --> N ) -> ( dom g = N /\ dom p = N ) )
32 26 28 31 syl2an 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> ( dom g = N /\ dom p = N ) )
33 eqtr3 
 |-  ( ( dom g = N /\ dom p = N ) -> dom g = dom p )
34 32 33 syl 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> dom g = dom p )
35 34 ad2antlr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> dom g = dom p )
36 simpr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) )
37 eqtr3 
 |-  ( ( ( g ` K ) = K /\ ( p ` K ) = K ) -> ( g ` K ) = ( p ` K ) )
38 37 ad2ant2l 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> ( g ` K ) = ( p ` K ) )
39 38 ad2antlr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> ( g ` K ) = ( p ` K ) )
40 fveq2 
 |-  ( i = K -> ( g ` i ) = ( g ` K ) )
41 fveq2 
 |-  ( i = K -> ( p ` i ) = ( p ` K ) )
42 40 41 eqeq12d 
 |-  ( i = K -> ( ( g ` i ) = ( p ` i ) <-> ( g ` K ) = ( p ` K ) ) )
43 42 ralunsn 
 |-  ( K e. N -> ( A. i e. ( ( N \ { K } ) u. { K } ) ( g ` i ) = ( p ` i ) <-> ( A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) /\ ( g ` K ) = ( p ` K ) ) ) )
44 43 adantr 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> ( A. i e. ( ( N \ { K } ) u. { K } ) ( g ` i ) = ( p ` i ) <-> ( A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) /\ ( g ` K ) = ( p ` K ) ) ) )
45 44 adantr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> ( A. i e. ( ( N \ { K } ) u. { K } ) ( g ` i ) = ( p ` i ) <-> ( A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) /\ ( g ` K ) = ( p ` K ) ) ) )
46 36 39 45 mpbir2and 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> A. i e. ( ( N \ { K } ) u. { K } ) ( g ` i ) = ( p ` i ) )
47 f1odm 
 |-  ( g : N -1-1-onto-> N -> dom g = N )
48 47 adantr 
 |-  ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) -> dom g = N )
49 48 adantr 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> dom g = N )
50 difsnid 
 |-  ( K e. N -> ( ( N \ { K } ) u. { K } ) = N )
51 50 eqcomd 
 |-  ( K e. N -> N = ( ( N \ { K } ) u. { K } ) )
52 49 51 sylan9eqr 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> dom g = ( ( N \ { K } ) u. { K } ) )
53 52 adantr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> dom g = ( ( N \ { K } ) u. { K } ) )
54 46 53 raleqtrrdv 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> A. i e. dom g ( g ` i ) = ( p ` i ) )
55 f1ofun 
 |-  ( g : N -1-1-onto-> N -> Fun g )
56 55 adantr 
 |-  ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) -> Fun g )
57 f1ofun 
 |-  ( p : N -1-1-onto-> N -> Fun p )
58 57 adantr 
 |-  ( ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) -> Fun p )
59 56 58 anim12i 
 |-  ( ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) -> ( Fun g /\ Fun p ) )
60 59 ad2antlr 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> ( Fun g /\ Fun p ) )
61 eqfunfv 
 |-  ( ( Fun g /\ Fun p ) -> ( g = p <-> ( dom g = dom p /\ A. i e. dom g ( g ` i ) = ( p ` i ) ) ) )
62 60 61 syl 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> ( g = p <-> ( dom g = dom p /\ A. i e. dom g ( g ` i ) = ( p ` i ) ) ) )
63 35 54 62 mpbir2and 
 |-  ( ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) /\ A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) ) -> g = p )
64 63 ex 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> ( A. i e. ( N \ { K } ) ( g ` i ) = ( p ` i ) -> g = p ) )
65 24 64 sylbid 
 |-  ( ( K e. N /\ ( ( g : N -1-1-onto-> N /\ ( g ` K ) = K ) /\ ( p : N -1-1-onto-> N /\ ( p ` K ) = K ) ) ) -> ( ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) -> g = p ) )
66 14 65 sylan2b 
 |-  ( ( K e. N /\ ( g e. Q /\ p e. Q ) ) -> ( ( g |` ( N \ { K } ) ) = ( p |` ( N \ { K } ) ) -> g = p ) )
67 9 66 sylbid 
 |-  ( ( K e. N /\ ( g e. Q /\ p e. Q ) ) -> ( ( H ` g ) = ( H ` p ) -> g = p ) )
68 67 ralrimivva 
 |-  ( K e. N -> A. g e. Q A. p e. Q ( ( H ` g ) = ( H ` p ) -> g = p ) )
69 dff13 
 |-  ( H : Q -1-1-> S <-> ( H : Q --> S /\ A. g e. Q A. p e. Q ( ( H ` g ) = ( H ` p ) -> g = p ) ) )
70 5 68 69 sylanbrc 
 |-  ( K e. N -> H : Q -1-1-> S )