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 N if x = K K Z x
Assertion symgextf1 K N Z S E : N 1-1 N

Proof

Step Hyp Ref Expression
1 symgext.s S = Base SymGrp N K
2 symgext.e E = x N if x = K K Z x
3 1 2 symgextf K N Z S E : N N
4 difsnid K N N K K = N
5 4 eqcomd K N N = N K K
6 5 eleq2d K N y N y N K K
7 5 eleq2d K N z N z N K K
8 6 7 anbi12d K N y N z N y N K K z N K K
9 8 adantr K N Z S y N z N y N K K z N K K
10 elun y N K K y N K y K
11 elun z N K K z N K z K
12 1 2 symgextfv K N Z S y N K E y = Z y
13 12 com12 y N K K N Z S E y = Z y
14 13 adantr y N K z N K K N Z S E y = Z y
15 14 imp y N K z N K K N Z S E y = Z y
16 1 2 symgextfv K N Z S z N K E z = Z z
17 16 com12 z N K K N Z S E z = Z z
18 17 adantl y N K z N K K N Z S E z = Z z
19 18 imp y N K z N K K N Z S E z = Z z
20 15 19 eqeq12d y N K z N K K N Z S E y = E z Z y = Z z
21 eqid SymGrp N K = SymGrp N K
22 21 1 symgbasf1o Z 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 i N K j 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 N K z N K i N K j N K Z i = Z j i = j Z y = Z z y = z
33 32 expcom i N K j N K Z i = Z j i = j y N K z N K Z y = Z z y = z
34 33 a1d i N K j N K Z i = Z j i = j K N y N K z N K Z y = Z z y = z
35 24 34 simplbiim Z : N K 1-1 N K K N y N K z N K Z y = Z z y = z
36 22 23 35 3syl Z S K N y N K z N K Z y = Z z y = z
37 36 impcom K N Z S y N K z N K Z y = Z z y = z
38 37 impcom y N K z N K K N Z S Z y = Z z y = z
39 20 38 sylbid y N K z N K K N Z S E y = E z y = z
40 39 ex y N K z N K K N Z S E y = E z y = z
41 1 2 symgextf1lem K N Z S z N K y 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 N K y K K N Z S E y = E z y = z
46 45 ancoms y K z N K K N Z S E y = E z y = z
47 1 2 symgextf1lem K N Z S y N K z 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 N K z K K N Z S E y = E z y = z
51 elsni y K y = K
52 elsni z K z = K
53 eqtr3 y = K z = K y = z
54 53 2a1d y = K z = K K N Z S E y = E z y = z
55 51 52 54 syl2an y K z K K N Z S E y = E z y = z
56 40 46 50 55 ccase y N K y K z N K z K K N Z S E y = E z y = z
57 10 11 56 syl2anb y N K K z N K K K N Z S E y = E z y = z
58 57 com12 K N Z S y N K K z N K K E y = E z y = z
59 9 58 sylbid K N Z S y N z N E y = E z y = z
60 59 ralrimivv K N Z S y N z N E y = E z y = z
61 dff13 E : N 1-1 N E : N N y N z N E y = E z y = z
62 3 60 61 sylanbrc K N Z S E : N 1-1 N