Metamath Proof Explorer

Theorem psgnfzto1st

Description: The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypotheses psgnfzto1st.d ⊢ D = 1 … N
psgnfzto1st.p ⊢ P = i ∈ D ⟼ if i = 1 I if i ≤ I i − 1 i
psgnfzto1st.g ⊢ G = SymGrp ⁡ D
psgnfzto1st.b ⊢ B = Base G
psgnfzto1st.s ⊢ S = pmSgn ⁡ D
Assertion psgnfzto1st ⊢ I ∈ D → S ⁡ P = − 1 I + 1

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢ D = 1 … N
2 psgnfzto1st.p ⊢ P = i ∈ D ⟼ if i = 1 I if i ≤ I i − 1 i
3 psgnfzto1st.g ⊢ G = SymGrp ⁡ D
4 psgnfzto1st.b ⊢ B = Base G
5 psgnfzto1st.s ⊢ S = pmSgn ⁡ D
6 elfz1b ⊢ I ∈ 1 … N ↔ I ∈ ℕ ∧ N ∈ ℕ ∧ I ≤ N
7 6 biimpi ⊢ I ∈ 1 … N → I ∈ ℕ ∧ N ∈ ℕ ∧ I ≤ N
8 7 1 eleq2s ⊢ I ∈ D → I ∈ ℕ ∧ N ∈ ℕ ∧ I ≤ N
9 3ancoma ⊢ N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N ↔ I ∈ ℕ ∧ N ∈ ℕ ∧ I ≤ N
10 8 9 sylibr ⊢ I ∈ D → N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N
11 df-3an ⊢ N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N ↔ N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N
12 breq1 ⊢ m = 1 → m ≤ N ↔ 1 ≤ N
13 id ⊢ m = 1 → m = 1
14 breq2 ⊢ m = 1 → i ≤ m ↔ i ≤ 1
15 14 ifbid ⊢ m = 1 → if i ≤ m i − 1 i = if i ≤ 1 i − 1 i
16 13 15 ifeq12d ⊢ m = 1 → if i = 1 m if i ≤ m i − 1 i = if i = 1 1 if i ≤ 1 i − 1 i
17 16 mpteq2dv ⊢ m = 1 → i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i
18 17 fveq2d ⊢ m = 1 → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i
19 oveq1 ⊢ m = 1 → m + 1 = 1 + 1
20 19 oveq2d ⊢ m = 1 → − 1 m + 1 = − 1 1 + 1
21 18 20 eqeq12d ⊢ m = 1 → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = − 1 1 + 1
22 12 21 imbi12d ⊢ m = 1 → m ≤ N → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = − 1 1 + 1
23 breq1 ⊢ m = n → m ≤ N ↔ n ≤ N
24 id ⊢ m = n → m = n
25 breq2 ⊢ m = n → i ≤ m ↔ i ≤ n
26 25 ifbid ⊢ m = n → if i ≤ m i − 1 i = if i ≤ n i − 1 i
27 24 26 ifeq12d ⊢ m = n → if i = 1 m if i ≤ m i − 1 i = if i = 1 n if i ≤ n i − 1 i
28 27 mpteq2dv ⊢ m = n → i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
29 28 fveq2d ⊢ m = n → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
30 oveq1 ⊢ m = n → m + 1 = n + 1
31 30 oveq2d ⊢ m = n → − 1 m + 1 = − 1 n + 1
32 29 31 eqeq12d ⊢ m = n → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1
33 23 32 imbi12d ⊢ m = n → m ≤ N → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1
34 breq1 ⊢ m = n + 1 → m ≤ N ↔ n + 1 ≤ N
35 id ⊢ m = n + 1 → m = n + 1
36 breq2 ⊢ m = n + 1 → i ≤ m ↔ i ≤ n + 1
37 36 ifbid ⊢ m = n + 1 → if i ≤ m i − 1 i = if i ≤ n + 1 i − 1 i
38 35 37 ifeq12d ⊢ m = n + 1 → if i = 1 m if i ≤ m i − 1 i = if i = 1 n + 1 if i ≤ n + 1 i − 1 i
39 38 mpteq2dv ⊢ m = n + 1 → i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i
40 39 fveq2d ⊢ m = n + 1 → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i
41 oveq1 ⊢ m = n + 1 → m + 1 = n + 1 + 1
42 41 oveq2d ⊢ m = n + 1 → − 1 m + 1 = − 1 n + 1 + 1
43 40 42 eqeq12d ⊢ m = n + 1 → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = − 1 n + 1 + 1
44 34 43 imbi12d ⊢ m = n + 1 → m ≤ N → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ n + 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = − 1 n + 1 + 1
45 breq1 ⊢ m = I → m ≤ N ↔ I ≤ N
46 id ⊢ m = I → m = I
47 breq2 ⊢ m = I → i ≤ m ↔ i ≤ I
48 47 ifbid ⊢ m = I → if i ≤ m i − 1 i = if i ≤ I i − 1 i
49 46 48 ifeq12d ⊢ m = I → if i = 1 m if i ≤ m i − 1 i = if i = 1 I if i ≤ I i − 1 i
50 49 mpteq2dv ⊢ m = I → i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = i ∈ D ⟼ if i = 1 I if i ≤ I i − 1 i
51 50 2 eqtr4di ⊢ m = I → i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = P
52 51 fveq2d ⊢ m = I → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = S ⁡ P
53 oveq1 ⊢ m = I → m + 1 = I + 1
54 53 oveq2d ⊢ m = I → − 1 m + 1 = − 1 I + 1
55 52 54 eqeq12d ⊢ m = I → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ S ⁡ P = − 1 I + 1
56 45 55 imbi12d ⊢ m = I → m ≤ N → S ⁡ i ∈ D ⟼ if i = 1 m if i ≤ m i − 1 i = − 1 m + 1 ↔ I ≤ N → S ⁡ P = − 1 I + 1
57 fzfi ⊢ 1 … N ∈ Fin
58 1 57 eqeltri ⊢ D ∈ Fin
59 5 psgnid ⊢ D ∈ Fin → S ⁡ I ↾ D = 1
60 58 59 ax-mp ⊢ S ⁡ I ↾ D = 1
61 eqid ⊢ 1 = 1
62 eqid ⊢ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i
63 1 62 fzto1st1 ⊢ 1 = 1 → i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = I ↾ D
64 61 63 ax-mp ⊢ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = I ↾ D
65 64 fveq2i ⊢ S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = S ⁡ I ↾ D
66 1p1e2 ⊢ 1 + 1 = 2
67 66 oveq2i ⊢ − 1 1 + 1 = − 1 2
68 neg1sqe1 ⊢ − 1 2 = 1
69 67 68 eqtri ⊢ − 1 1 + 1 = 1
70 60 65 69 3eqtr4i ⊢ S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = − 1 1 + 1
71 70 2a1i ⊢ N ∈ ℕ → 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 1 if i ≤ 1 i − 1 i = − 1 1 + 1
72 simplr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ∈ ℕ
73 72 peano2nnd ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ∈ ℕ
74 simpll ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → N ∈ ℕ
75 simpr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ≤ N
76 73 74 75 3jca ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ∈ ℕ ∧ N ∈ ℕ ∧ n + 1 ≤ N
77 elfz1b ⊢ n + 1 ∈ 1 … N ↔ n + 1 ∈ ℕ ∧ N ∈ ℕ ∧ n + 1 ≤ N
78 76 77 sylibr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ∈ 1 … N
79 78 1 eleqtrrdi ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ∈ D
80 1 psgnfzto1stlem ⊢ n ∈ ℕ ∧ n + 1 ∈ D → i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
81 72 79 80 syl2anc ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
82 81 adantlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
83 82 fveq2d ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
84 58 a1i ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → D ∈ Fin
85 eqid ⊢ ran ⁡ pmTrsp ⁡ D = ran ⁡ pmTrsp ⁡ D
86 85 3 4 symgtrf ⊢ ran ⁡ pmTrsp ⁡ D ⊆ B
87 eqid ⊢ pmTrsp ⁡ D = pmTrsp ⁡ D
88 1 87 pmtrto1cl ⊢ n ∈ ℕ ∧ n + 1 ∈ D → pmTrsp ⁡ D ⁡ n n + 1 ∈ ran ⁡ pmTrsp ⁡ D
89 72 79 88 syl2anc ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → pmTrsp ⁡ D ⁡ n n + 1 ∈ ran ⁡ pmTrsp ⁡ D
90 89 adantlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → pmTrsp ⁡ D ⁡ n n + 1 ∈ ran ⁡ pmTrsp ⁡ D
91 86 90 sselid ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → pmTrsp ⁡ D ⁡ n n + 1 ∈ B
92 72 nnred ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ∈ ℝ
93 1red ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → 1 ∈ ℝ
94 92 93 readdcld ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n + 1 ∈ ℝ
95 74 nnred ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → N ∈ ℝ
96 92 lep1d ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ≤ n + 1
97 92 94 95 96 75 letrd ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ≤ N
98 72 74 97 3jca ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ∈ ℕ ∧ N ∈ ℕ ∧ n ≤ N
99 elfz1b ⊢ n ∈ 1 … N ↔ n ∈ ℕ ∧ N ∈ ℕ ∧ n ≤ N
100 98 99 sylibr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ∈ 1 … N
101 100 1 eleqtrrdi ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → n ∈ D
102 101 adantlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → n ∈ D
103 eqid ⊢ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
104 1 103 3 4 fzto1st ⊢ n ∈ D → i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i ∈ B
105 102 104 syl ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i ∈ B
106 3 5 4 psgnco ⊢ D ∈ Fin ∧ pmTrsp ⁡ D ⁡ n n + 1 ∈ B ∧ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i ∈ B → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ⁢ S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
107 84 91 105 106 syl3anc ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ∘ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ⁢ S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i
108 3 85 5 psgnpmtr ⊢ pmTrsp ⁡ D ⁡ n n + 1 ∈ ran ⁡ pmTrsp ⁡ D → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 = − 1
109 89 108 syl ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n + 1 ≤ N → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 = − 1
110 109 adantlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 = − 1
111 97 adantlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → n ≤ N
112 simplr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1
113 111 112 mpd ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1
114 110 113 oveq12d ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ⁢ S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = -1 ⁢ − 1 n + 1
115 neg1cn ⊢ − 1 ∈ ℂ
116 peano2nn ⊢ n ∈ ℕ → n + 1 ∈ ℕ
117 116 nnnn0d ⊢ n ∈ ℕ → n + 1 ∈ ℕ 0
118 expp1 ⊢ − 1 ∈ ℂ ∧ n + 1 ∈ ℕ 0 → − 1 n + 1 + 1 = − 1 n + 1 ⁢ -1
119 115 117 118 sylancr ⊢ n ∈ ℕ → − 1 n + 1 + 1 = − 1 n + 1 ⁢ -1
120 115 a1i ⊢ n ∈ ℕ → − 1 ∈ ℂ
121 120 117 expcld ⊢ n ∈ ℕ → − 1 n + 1 ∈ ℂ
122 121 120 mulcomd ⊢ n ∈ ℕ → − 1 n + 1 ⁢ -1 = -1 ⁢ − 1 n + 1
123 119 122 eqtr2d ⊢ n ∈ ℕ → -1 ⁢ − 1 n + 1 = − 1 n + 1 + 1
124 123 ad3antlr ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → -1 ⁢ − 1 n + 1 = − 1 n + 1 + 1
125 114 124 eqtrd ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ pmTrsp ⁡ D ⁡ n n + 1 ⁢ S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 + 1
126 83 107 125 3eqtrd ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 ∧ n + 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = − 1 n + 1 + 1
127 126 ex ⊢ N ∈ ℕ ∧ n ∈ ℕ ∧ n ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n if i ≤ n i − 1 i = − 1 n + 1 → n + 1 ≤ N → S ⁡ i ∈ D ⟼ if i = 1 n + 1 if i ≤ n + 1 i − 1 i = − 1 n + 1 + 1
128 22 33 44 56 71 127 nnindd ⊢ N ∈ ℕ ∧ I ∈ ℕ → I ≤ N → S ⁡ P = − 1 I + 1
129 128 imp ⊢ N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N → S ⁡ P = − 1 I + 1
130 11 129 sylbi ⊢ N ∈ ℕ ∧ I ∈ ℕ ∧ I ≤ N → S ⁡ P = − 1 I + 1
131 10 130 syl ⊢ I ∈ D → S ⁡ P = − 1 I + 1