Metamath Proof Explorer


Theorem symgextf1

Description: The extension of a permutation, fixing the additional element, is a 1-1 function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgext.e
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion symgextf1
|- ( ( K e. N /\ Z e. S ) -> E : N -1-1-> N )

Proof

Step Hyp Ref Expression
1 symgext.s
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
2 symgext.e
 |-  E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
3 1 2 symgextf
 |-  ( ( K e. N /\ Z e. S ) -> E : N --> N )
4 difsnid
 |-  ( K e. N -> ( ( N \ { K } ) u. { K } ) = N )
5 4 eqcomd
 |-  ( K e. N -> N = ( ( N \ { K } ) u. { K } ) )
6 5 eleq2d
 |-  ( K e. N -> ( y e. N <-> y e. ( ( N \ { K } ) u. { K } ) ) )
7 5 eleq2d
 |-  ( K e. N -> ( z e. N <-> z e. ( ( N \ { K } ) u. { K } ) ) )
8 6 7 anbi12d
 |-  ( K e. N -> ( ( y e. N /\ z e. N ) <-> ( y e. ( ( N \ { K } ) u. { K } ) /\ z e. ( ( N \ { K } ) u. { K } ) ) ) )
9 8 adantr
 |-  ( ( K e. N /\ Z e. S ) -> ( ( y e. N /\ z e. N ) <-> ( y e. ( ( N \ { K } ) u. { K } ) /\ z e. ( ( N \ { K } ) u. { K } ) ) ) )
10 elun
 |-  ( y e. ( ( N \ { K } ) u. { K } ) <-> ( y e. ( N \ { K } ) \/ y e. { K } ) )
11 elun
 |-  ( z e. ( ( N \ { K } ) u. { K } ) <-> ( z e. ( N \ { K } ) \/ z e. { K } ) )
12 1 2 symgextfv
 |-  ( ( K e. N /\ Z e. S ) -> ( y e. ( N \ { K } ) -> ( E ` y ) = ( Z ` y ) ) )
13 12 com12
 |-  ( y e. ( N \ { K } ) -> ( ( K e. N /\ Z e. S ) -> ( E ` y ) = ( Z ` y ) ) )
14 13 adantr
 |-  ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( E ` y ) = ( Z ` y ) ) )
15 14 imp
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ ( K e. N /\ Z e. S ) ) -> ( E ` y ) = ( Z ` y ) )
16 1 2 symgextfv
 |-  ( ( K e. N /\ Z e. S ) -> ( z e. ( N \ { K } ) -> ( E ` z ) = ( Z ` z ) ) )
17 16 com12
 |-  ( z e. ( N \ { K } ) -> ( ( K e. N /\ Z e. S ) -> ( E ` z ) = ( Z ` z ) ) )
18 17 adantl
 |-  ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( E ` z ) = ( Z ` z ) ) )
19 18 imp
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ ( K e. N /\ Z e. S ) ) -> ( E ` z ) = ( Z ` z ) )
20 15 19 eqeq12d
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ ( K e. N /\ Z e. S ) ) -> ( ( E ` y ) = ( E ` z ) <-> ( Z ` y ) = ( Z ` z ) ) )
21 eqid
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
22 21 1 symgbasf1o
 |-  ( Z e. S -> Z : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) )
23 f1of1
 |-  ( Z : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) -> Z : ( N \ { K } ) -1-1-> ( N \ { K } ) )
24 dff13
 |-  ( Z : ( N \ { K } ) -1-1-> ( N \ { K } ) <-> ( Z : ( N \ { K } ) --> ( N \ { K } ) /\ A. i e. ( N \ { K } ) A. j e. ( N \ { K } ) ( ( Z ` i ) = ( Z ` j ) -> i = j ) ) )
25 fveqeq2
 |-  ( i = y -> ( ( Z ` i ) = ( Z ` j ) <-> ( Z ` y ) = ( Z ` j ) ) )
26 equequ1
 |-  ( i = y -> ( i = j <-> y = j ) )
27 25 26 imbi12d
 |-  ( i = y -> ( ( ( Z ` i ) = ( Z ` j ) -> i = j ) <-> ( ( Z ` y ) = ( Z ` j ) -> y = j ) ) )
28 fveq2
 |-  ( j = z -> ( Z ` j ) = ( Z ` z ) )
29 28 eqeq2d
 |-  ( j = z -> ( ( Z ` y ) = ( Z ` j ) <-> ( Z ` y ) = ( Z ` z ) ) )
30 equequ2
 |-  ( j = z -> ( y = j <-> y = z ) )
31 29 30 imbi12d
 |-  ( j = z -> ( ( ( Z ` y ) = ( Z ` j ) -> y = j ) <-> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) )
32 27 31 rspc2va
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ A. i e. ( N \ { K } ) A. j e. ( N \ { K } ) ( ( Z ` i ) = ( Z ` j ) -> i = j ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) )
33 32 expcom
 |-  ( A. i e. ( N \ { K } ) A. j e. ( N \ { K } ) ( ( Z ` i ) = ( Z ` j ) -> i = j ) -> ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) )
34 33 a1d
 |-  ( A. i e. ( N \ { K } ) A. j e. ( N \ { K } ) ( ( Z ` i ) = ( Z ` j ) -> i = j ) -> ( K e. N -> ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) ) )
35 24 34 simplbiim
 |-  ( Z : ( N \ { K } ) -1-1-> ( N \ { K } ) -> ( K e. N -> ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) ) )
36 22 23 35 3syl
 |-  ( Z e. S -> ( K e. N -> ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) ) )
37 36 impcom
 |-  ( ( K e. N /\ Z e. S ) -> ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) ) )
38 37 impcom
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ ( K e. N /\ Z e. S ) ) -> ( ( Z ` y ) = ( Z ` z ) -> y = z ) )
39 20 38 sylbid
 |-  ( ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) /\ ( K e. N /\ Z e. S ) ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) )
40 39 ex
 |-  ( ( y e. ( N \ { K } ) /\ z e. ( N \ { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
41 1 2 symgextf1lem
 |-  ( ( K e. N /\ Z e. S ) -> ( ( z e. ( N \ { K } ) /\ y e. { K } ) -> ( E ` z ) =/= ( E ` y ) ) )
42 eqneqall
 |-  ( ( E ` z ) = ( E ` y ) -> ( ( E ` z ) =/= ( E ` y ) -> y = z ) )
43 42 eqcoms
 |-  ( ( E ` y ) = ( E ` z ) -> ( ( E ` z ) =/= ( E ` y ) -> y = z ) )
44 43 com12
 |-  ( ( E ` z ) =/= ( E ` y ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) )
45 41 44 syl6com
 |-  ( ( z e. ( N \ { K } ) /\ y e. { K } ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
46 45 ancoms
 |-  ( ( y e. { K } /\ z e. ( N \ { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
47 1 2 symgextf1lem
 |-  ( ( K e. N /\ Z e. S ) -> ( ( y e. ( N \ { K } ) /\ z e. { K } ) -> ( E ` y ) =/= ( E ` z ) ) )
48 eqneqall
 |-  ( ( E ` y ) = ( E ` z ) -> ( ( E ` y ) =/= ( E ` z ) -> y = z ) )
49 48 com12
 |-  ( ( E ` y ) =/= ( E ` z ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) )
50 47 49 syl6com
 |-  ( ( y e. ( N \ { K } ) /\ z e. { K } ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
51 elsni
 |-  ( y e. { K } -> y = K )
52 elsni
 |-  ( z e. { K } -> z = K )
53 eqtr3
 |-  ( ( y = K /\ z = K ) -> y = z )
54 53 2a1d
 |-  ( ( y = K /\ z = K ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
55 51 52 54 syl2an
 |-  ( ( y e. { K } /\ z e. { K } ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
56 40 46 50 55 ccase
 |-  ( ( ( y e. ( N \ { K } ) \/ y e. { K } ) /\ ( z e. ( N \ { K } ) \/ z e. { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
57 10 11 56 syl2anb
 |-  ( ( y e. ( ( N \ { K } ) u. { K } ) /\ z e. ( ( N \ { K } ) u. { K } ) ) -> ( ( K e. N /\ Z e. S ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
58 57 com12
 |-  ( ( K e. N /\ Z e. S ) -> ( ( y e. ( ( N \ { K } ) u. { K } ) /\ z e. ( ( N \ { K } ) u. { K } ) ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
59 9 58 sylbid
 |-  ( ( K e. N /\ Z e. S ) -> ( ( y e. N /\ z e. N ) -> ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
60 59 ralrimivv
 |-  ( ( K e. N /\ Z e. S ) -> A. y e. N A. z e. N ( ( E ` y ) = ( E ` z ) -> y = z ) )
61 dff13
 |-  ( E : N -1-1-> N <-> ( E : N --> N /\ A. y e. N A. z e. N ( ( E ` y ) = ( E ` z ) -> y = z ) ) )
62 3 60 61 sylanbrc
 |-  ( ( K e. N /\ Z e. S ) -> E : N -1-1-> N )