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 46 53 raleqtrrdv ⊢ 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
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 ∈ 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
61 eqfunfv ⊢ Fun ⁡ g ∧ Fun ⁡ p → g = p ↔ dom ⁡ g = dom ⁡ p ∧ ∀ i ∈ dom ⁡ g g ⁡ i = p ⁡ i
62 60 61 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
63 35 54 62 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
64 63 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
65 24 64 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
66 14 65 sylan2b ⊢ K ∈ N ∧ g ∈ Q ∧ p ∈ Q → g ↾ N ∖ K = p ↾ N ∖ K → g = p
67 9 66 sylbid ⊢ K ∈ N ∧ g ∈ Q ∧ p ∈ Q → H ⁡ g = H ⁡ p → g = p
68 67 ralrimivva ⊢ K ∈ N → ∀ g ∈ Q ∀ p ∈ Q H ⁡ g = H ⁡ p → g = p
69 dff13 ⊢ H : Q ⟶ 1-1 S ↔ H : Q ⟶ S ∧ ∀ g ∈ Q ∀ p ∈ Q H ⁡ g = H ⁡ p → g = p
70 5 68 69 sylanbrc ⊢ K ∈ N → H : Q ⟶ 1-1 S