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 )