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⟼ifi=1Iifi≤Ii−1i
psgnfzto1st.g ⊢G=SymGrp⁡D
psgnfzto1st.b ⊢B=BaseG
psgnfzto1st.s ⊢S=pmSgn⁡D
Assertion psgnfzto1st ⊢I∈D→S⁡P=−1I+1

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢D=1…N
2 psgnfzto1st.p ⊢P=i∈D⟼ifi=1Iifi≤Ii−1i
3 psgnfzto1st.g ⊢G=SymGrp⁡D
4 psgnfzto1st.b ⊢B=BaseG
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→ifi≤mi−1i=ifi≤1i−1i
16 13 15 ifeq12d ⊢m=1→ifi=1mifi≤mi−1i=ifi=11ifi≤1i−1i
17 16 mpteq2dv ⊢m=1→i∈D⟼ifi=1mifi≤mi−1i=i∈D⟼ifi=11ifi≤1i−1i
18 17 fveq2d ⊢m=1→S⁡i∈D⟼ifi=1mifi≤mi−1i=S⁡i∈D⟼ifi=11ifi≤1i−1i
19 oveq1 ⊢m=1→m+1=1+1
20 19 oveq2d ⊢m=1→−1m+1=−11+1
21 18 20 eqeq12d ⊢m=1→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔S⁡i∈D⟼ifi=11ifi≤1i−1i=−11+1
22 12 21 imbi12d ⊢m=1→m≤N→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔1≤N→S⁡i∈D⟼ifi=11ifi≤1i−1i=−11+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→ifi≤mi−1i=ifi≤ni−1i
27 24 26 ifeq12d ⊢m=n→ifi=1mifi≤mi−1i=ifi=1nifi≤ni−1i
28 27 mpteq2dv ⊢m=n→i∈D⟼ifi=1mifi≤mi−1i=i∈D⟼ifi=1nifi≤ni−1i
29 28 fveq2d ⊢m=n→S⁡i∈D⟼ifi=1mifi≤mi−1i=S⁡i∈D⟼ifi=1nifi≤ni−1i
30 oveq1 ⊢m=n→m+1=n+1
31 30 oveq2d ⊢m=n→−1m+1=−1n+1
32 29 31 eqeq12d ⊢m=n→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1
33 23 32 imbi12d ⊢m=n→m≤N→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+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→ifi≤mi−1i=ifi≤n+1i−1i
38 35 37 ifeq12d ⊢m=n+1→ifi=1mifi≤mi−1i=ifi=1n+1ifi≤n+1i−1i
39 38 mpteq2dv ⊢m=n+1→i∈D⟼ifi=1mifi≤mi−1i=i∈D⟼ifi=1n+1ifi≤n+1i−1i
40 39 fveq2d ⊢m=n+1→S⁡i∈D⟼ifi=1mifi≤mi−1i=S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i
41 oveq1 ⊢m=n+1→m+1=n+1+1
42 41 oveq2d ⊢m=n+1→−1m+1=−1n+1+1
43 40 42 eqeq12d ⊢m=n+1→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i=−1n+1+1
44 34 43 imbi12d ⊢m=n+1→m≤N→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔n+1≤N→S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i=−1n+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→ifi≤mi−1i=ifi≤Ii−1i
49 46 48 ifeq12d ⊢m=I→ifi=1mifi≤mi−1i=ifi=1Iifi≤Ii−1i
50 49 mpteq2dv ⊢m=I→i∈D⟼ifi=1mifi≤mi−1i=i∈D⟼ifi=1Iifi≤Ii−1i
51 50 2 eqtr4di ⊢m=I→i∈D⟼ifi=1mifi≤mi−1i=P
52 51 fveq2d ⊢m=I→S⁡i∈D⟼ifi=1mifi≤mi−1i=S⁡P
53 oveq1 ⊢m=I→m+1=I+1
54 53 oveq2d ⊢m=I→−1m+1=−1I+1
55 52 54 eqeq12d ⊢m=I→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔S⁡P=−1I+1
56 45 55 imbi12d ⊢m=I→m≤N→S⁡i∈D⟼ifi=1mifi≤mi−1i=−1m+1↔I≤N→S⁡P=−1I+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⟼ifi=11ifi≤1i−1i=i∈D⟼ifi=11ifi≤1i−1i
63 1 62 fzto1st1 ⊢1=1→i∈D⟼ifi=11ifi≤1i−1i=I↾D
64 61 63 ax-mp ⊢i∈D⟼ifi=11ifi≤1i−1i=I↾D
65 64 fveq2i ⊢S⁡i∈D⟼ifi=11ifi≤1i−1i=S⁡I↾D
66 1p1e2 ⊢1+1=2
67 66 oveq2i ⊢−11+1=−12
68 neg1sqe1 ⊢−12=1
69 67 68 eqtri ⊢−11+1=1
70 60 65 69 3eqtr4i ⊢S⁡i∈D⟼ifi=11ifi≤1i−1i=−11+1
71 70 2a1i ⊢N∈ℕ→1≤N→S⁡i∈D⟼ifi=11ifi≤1i−1i=−11+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⟼ifi=1n+1ifi≤n+1i−1i=pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i
81 72 79 80 syl2anc ⊢N∈ℕ∧n∈ℕ∧n+1≤N→i∈D⟼ifi=1n+1ifi≤n+1i−1i=pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i
82 81 adantlr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→i∈D⟼ifi=1n+1ifi≤n+1i−1i=pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i
83 82 fveq2d ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i=S⁡pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i
84 58 a1i ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+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⁡nn+1∈ran⁡pmTrsp⁡D
89 72 79 88 syl2anc ⊢N∈ℕ∧n∈ℕ∧n+1≤N→pmTrsp⁡D⁡nn+1∈ran⁡pmTrsp⁡D
90 89 adantlr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→pmTrsp⁡D⁡nn+1∈ran⁡pmTrsp⁡D
91 86 90 sselid ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→pmTrsp⁡D⁡nn+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⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→n∈D
103 eqid ⊢i∈D⟼ifi=1nifi≤ni−1i=i∈D⟼ifi=1nifi≤ni−1i
104 1 103 3 4 fzto1st ⊢n∈D→i∈D⟼ifi=1nifi≤ni−1i∈B
105 102 104 syl ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→i∈D⟼ifi=1nifi≤ni−1i∈B
106 3 5 4 psgnco ⊢D∈Fin∧pmTrsp⁡D⁡nn+1∈B∧i∈D⟼ifi=1nifi≤ni−1i∈B→S⁡pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i=S⁡pmTrsp⁡D⁡nn+1⁢S⁡i∈D⟼ifi=1nifi≤ni−1i
107 84 91 105 106 syl3anc ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡pmTrsp⁡D⁡nn+1∘i∈D⟼ifi=1nifi≤ni−1i=S⁡pmTrsp⁡D⁡nn+1⁢S⁡i∈D⟼ifi=1nifi≤ni−1i
108 3 85 5 psgnpmtr ⊢pmTrsp⁡D⁡nn+1∈ran⁡pmTrsp⁡D→S⁡pmTrsp⁡D⁡nn+1=−1
109 89 108 syl ⊢N∈ℕ∧n∈ℕ∧n+1≤N→S⁡pmTrsp⁡D⁡nn+1=−1
110 109 adantlr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡pmTrsp⁡D⁡nn+1=−1
111 97 adantlr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→n≤N
112 simplr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1
113 111 112 mpd ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1
114 110 113 oveq12d ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡pmTrsp⁡D⁡nn+1⁢S⁡i∈D⟼ifi=1nifi≤ni−1i=-1⁢−1n+1
115 neg1cn ⊢−1∈ℂ
116 peano2nn ⊢n∈ℕ→n+1∈ℕ
117 116 nnnn0d ⊢n∈ℕ→n+1∈ℕ0
118 expp1 ⊢−1∈ℂ∧n+1∈ℕ0→−1n+1+1=−1n+1⁢-1
119 115 117 118 sylancr ⊢n∈ℕ→−1n+1+1=−1n+1⁢-1
120 115 a1i ⊢n∈ℕ→−1∈ℂ
121 120 117 expcld ⊢n∈ℕ→−1n+1∈ℂ
122 121 120 mulcomd ⊢n∈ℕ→−1n+1⁢-1=-1⁢−1n+1
123 119 122 eqtr2d ⊢n∈ℕ→-1⁢−1n+1=−1n+1+1
124 123 ad3antlr ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→-1⁢−1n+1=−1n+1+1
125 114 124 eqtrd ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡pmTrsp⁡D⁡nn+1⁢S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1+1
126 83 107 125 3eqtrd ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1∧n+1≤N→S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i=−1n+1+1
127 126 ex ⊢N∈ℕ∧n∈ℕ∧n≤N→S⁡i∈D⟼ifi=1nifi≤ni−1i=−1n+1→n+1≤N→S⁡i∈D⟼ifi=1n+1ifi≤n+1i−1i=−1n+1+1
128 22 33 44 56 71 127 nnindd ⊢N∈ℕ∧I∈ℕ→I≤N→S⁡P=−1I+1
129 128 imp ⊢N∈ℕ∧I∈ℕ∧I≤N→S⁡P=−1I+1
130 11 129 sylbi ⊢N∈ℕ∧I∈ℕ∧I≤N→S⁡P=−1I+1
131 10 130 syl ⊢I∈D→S⁡P=−1I+1