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 P | q K = K
symgfixf.s S = Base SymGrp N K
symgfixf.h H = q Q q N K
Assertion symgfixf1 K N H : Q 1-1 S

Proof

Step Hyp Ref Expression
1 symgfixf.p P = Base SymGrp N
2 symgfixf.q Q = q P | q K = K
3 symgfixf.s S = Base SymGrp N K
4 symgfixf.h H = q Q q N K
5 1 2 3 4 symgfixf K N H : Q S
6 4 fvtresfn g Q H g = g N K
7 4 fvtresfn p Q H p = p N K
8 6 7 eqeqan12d g Q p Q H g = H p g N K = p N K
9 8 adantl K N g Q p Q H g = H p g N K = p N K
10 1 2 symgfixelq g V g Q g : N 1-1 onto N g K = K
11 10 elv g Q g : N 1-1 onto N g K = K
12 1 2 symgfixelq p V p Q p : N 1-1 onto N p K = K
13 12 elv p Q p : N 1-1 onto N p K = K
14 11 13 anbi12i g Q p 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 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 N
22 21 adantl K 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 N
23 fvreseq g Fn N p Fn N N K N g N K = p N K i N K g i = p i
24 22 23 syl K 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 i 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 N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i dom g = dom p
36 simpr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i i 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 N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i 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 N i N K K g i = p i i N K g i = p i g K = p K
44 43 adantr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K K g i = p i i N K g i = p i g K = p K
45 44 adantr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i i N K K g i = p i i N K g i = p i g K = p K
46 36 39 45 mpbir2and K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i i N K 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 N N K K = N
51 50 eqcomd K N N = N K K
52 49 51 sylan9eqr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K dom g = N K K
53 52 adantr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i dom g = N K K
54 53 raleqdv K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i i dom g g i = p i i N K K g i = p i
55 46 54 mpbird K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i i dom g g i = p i
56 f1ofun g : N 1-1 onto N Fun g
57 56 adantr g : N 1-1 onto N g K = K Fun g
58 f1ofun p : N 1-1 onto N Fun p
59 58 adantr p : N 1-1 onto N p K = K Fun p
60 57 59 anim12i g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K Fun g Fun p
61 60 ad2antlr K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i Fun g Fun p
62 eqfunfv Fun g Fun p g = p dom g = dom p i dom g g i = p i
63 61 62 syl K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i g = p dom g = dom p i dom g g i = p i
64 35 55 63 mpbir2and K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i g = p
65 64 ex K N g : N 1-1 onto N g K = K p : N 1-1 onto N p K = K i N K g i = p i g = p
66 24 65 sylbid K 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
67 14 66 sylan2b K N g Q p Q g N K = p N K g = p
68 9 67 sylbid K N g Q p Q H g = H p g = p
69 68 ralrimivva K N g Q p Q H g = H p g = p
70 dff13 H : Q 1-1 S H : Q S g Q p Q H g = H p g = p
71 5 69 70 sylanbrc K N H : Q 1-1 S