Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  psgnfzto1st Structured version   Visualization version   GIF version

Theorem psgnfzto1st 30680
Description: The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.)
Hypotheses
Ref Expression
psgnfzto1st.d 𝐷 = (1...𝑁)
psgnfzto1st.p 𝑃 = (𝑖𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
psgnfzto1st.g 𝐺 = (SymGrp‘𝐷)
psgnfzto1st.b 𝐵 = (Base‘𝐺)
psgnfzto1st.s 𝑆 = (pmSgn‘𝐷)
Assertion
Ref Expression
psgnfzto1st (𝐼𝐷 → (𝑆𝑃) = (-1↑(𝐼 + 1)))
Distinct variable groups:   𝐷,𝑖   𝑖,𝐼   𝑖,𝑁   𝐵,𝑖
Allowed substitution hints:   𝑃(𝑖)   𝑆(𝑖)   𝐺(𝑖)

Proof of Theorem psgnfzto1st
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfz1b 12971 . . . . 5 (𝐼 ∈ (1...𝑁) ↔ (𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼𝑁))
21biimpi 217 . . . 4 (𝐼 ∈ (1...𝑁) → (𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼𝑁))
3 psgnfzto1st.d . . . 4 𝐷 = (1...𝑁)
42, 3eleq2s 2936 . . 3 (𝐼𝐷 → (𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼𝑁))
5 3ancoma 1092 . . 3 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼𝑁) ↔ (𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼𝑁))
64, 5sylibr 235 . 2 (𝐼𝐷 → (𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼𝑁))
7 df-3an 1083 . . 3 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼𝑁) ↔ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ 𝐼𝑁))
8 breq1 5066 . . . . . 6 (𝑚 = 1 → (𝑚𝑁 ↔ 1 ≤ 𝑁))
9 id 22 . . . . . . . . . 10 (𝑚 = 1 → 𝑚 = 1)
10 breq2 5067 . . . . . . . . . . 11 (𝑚 = 1 → (𝑖𝑚𝑖 ≤ 1))
1110ifbid 4492 . . . . . . . . . 10 (𝑚 = 1 → if(𝑖𝑚, (𝑖 − 1), 𝑖) = if(𝑖 ≤ 1, (𝑖 − 1), 𝑖))
129, 11ifeq12d 4490 . . . . . . . . 9 (𝑚 = 1 → if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)) = if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))
1312mpteq2dv 5159 . . . . . . . 8 (𝑚 = 1 → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖))))
1413fveq2d 6673 . . . . . . 7 (𝑚 = 1 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))))
15 oveq1 7157 . . . . . . . 8 (𝑚 = 1 → (𝑚 + 1) = (1 + 1))
1615oveq2d 7166 . . . . . . 7 (𝑚 = 1 → (-1↑(𝑚 + 1)) = (-1↑(1 + 1)))
1714, 16eqeq12d 2842 . . . . . 6 (𝑚 = 1 → ((𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1)) ↔ (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))) = (-1↑(1 + 1))))
188, 17imbi12d 346 . . . . 5 (𝑚 = 1 → ((𝑚𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1))) ↔ (1 ≤ 𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))) = (-1↑(1 + 1)))))
19 breq1 5066 . . . . . 6 (𝑚 = 𝑛 → (𝑚𝑁𝑛𝑁))
20 id 22 . . . . . . . . . 10 (𝑚 = 𝑛𝑚 = 𝑛)
21 breq2 5067 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑖𝑚𝑖𝑛))
2221ifbid 4492 . . . . . . . . . 10 (𝑚 = 𝑛 → if(𝑖𝑚, (𝑖 − 1), 𝑖) = if(𝑖𝑛, (𝑖 − 1), 𝑖))
2320, 22ifeq12d 4490 . . . . . . . . 9 (𝑚 = 𝑛 → if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)) = if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))
2423mpteq2dv 5159 . . . . . . . 8 (𝑚 = 𝑛 → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))
2524fveq2d 6673 . . . . . . 7 (𝑚 = 𝑛 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))))
26 oveq1 7157 . . . . . . . 8 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
2726oveq2d 7166 . . . . . . 7 (𝑚 = 𝑛 → (-1↑(𝑚 + 1)) = (-1↑(𝑛 + 1)))
2825, 27eqeq12d 2842 . . . . . 6 (𝑚 = 𝑛 → ((𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1)) ↔ (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1))))
2919, 28imbi12d 346 . . . . 5 (𝑚 = 𝑛 → ((𝑚𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1))) ↔ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))))
30 breq1 5066 . . . . . 6 (𝑚 = (𝑛 + 1) → (𝑚𝑁 ↔ (𝑛 + 1) ≤ 𝑁))
31 id 22 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → 𝑚 = (𝑛 + 1))
32 breq2 5067 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → (𝑖𝑚𝑖 ≤ (𝑛 + 1)))
3332ifbid 4492 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → if(𝑖𝑚, (𝑖 − 1), 𝑖) = if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖))
3431, 33ifeq12d 4490 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)) = if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))
3534mpteq2dv 5159 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖))))
3635fveq2d 6673 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))))
37 oveq1 7157 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (𝑚 + 1) = ((𝑛 + 1) + 1))
3837oveq2d 7166 . . . . . . 7 (𝑚 = (𝑛 + 1) → (-1↑(𝑚 + 1)) = (-1↑((𝑛 + 1) + 1)))
3936, 38eqeq12d 2842 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1)) ↔ (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))) = (-1↑((𝑛 + 1) + 1))))
4030, 39imbi12d 346 . . . . 5 (𝑚 = (𝑛 + 1) → ((𝑚𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1))) ↔ ((𝑛 + 1) ≤ 𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))) = (-1↑((𝑛 + 1) + 1)))))
41 breq1 5066 . . . . . 6 (𝑚 = 𝐼 → (𝑚𝑁𝐼𝑁))
42 id 22 . . . . . . . . . . 11 (𝑚 = 𝐼𝑚 = 𝐼)
43 breq2 5067 . . . . . . . . . . . 12 (𝑚 = 𝐼 → (𝑖𝑚𝑖𝐼))
4443ifbid 4492 . . . . . . . . . . 11 (𝑚 = 𝐼 → if(𝑖𝑚, (𝑖 − 1), 𝑖) = if(𝑖𝐼, (𝑖 − 1), 𝑖))
4542, 44ifeq12d 4490 . . . . . . . . . 10 (𝑚 = 𝐼 → if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)) = if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
4645mpteq2dv 5159 . . . . . . . . 9 (𝑚 = 𝐼 → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖))))
47 psgnfzto1st.p . . . . . . . . 9 𝑃 = (𝑖𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
4846, 47syl6eqr 2879 . . . . . . . 8 (𝑚 = 𝐼 → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖))) = 𝑃)
4948fveq2d 6673 . . . . . . 7 (𝑚 = 𝐼 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (𝑆𝑃))
50 oveq1 7157 . . . . . . . 8 (𝑚 = 𝐼 → (𝑚 + 1) = (𝐼 + 1))
5150oveq2d 7166 . . . . . . 7 (𝑚 = 𝐼 → (-1↑(𝑚 + 1)) = (-1↑(𝐼 + 1)))
5249, 51eqeq12d 2842 . . . . . 6 (𝑚 = 𝐼 → ((𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1)) ↔ (𝑆𝑃) = (-1↑(𝐼 + 1))))
5341, 52imbi12d 346 . . . . 5 (𝑚 = 𝐼 → ((𝑚𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑚, if(𝑖𝑚, (𝑖 − 1), 𝑖)))) = (-1↑(𝑚 + 1))) ↔ (𝐼𝑁 → (𝑆𝑃) = (-1↑(𝐼 + 1)))))
54 fzfi 13335 . . . . . . . . 9 (1...𝑁) ∈ Fin
553, 54eqeltri 2914 . . . . . . . 8 𝐷 ∈ Fin
56 psgnfzto1st.s . . . . . . . . 9 𝑆 = (pmSgn‘𝐷)
5756psgnid 30672 . . . . . . . 8 (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1)
5855, 57ax-mp 5 . . . . . . 7 (𝑆‘( I ↾ 𝐷)) = 1
59 eqid 2826 . . . . . . . . 9 1 = 1
60 eqid 2826 . . . . . . . . . 10 (𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))
613, 60fzto1st1 30677 . . . . . . . . 9 (1 = 1 → (𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖))) = ( I ↾ 𝐷))
6259, 61ax-mp 5 . . . . . . . 8 (𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖))) = ( I ↾ 𝐷)
6362fveq2i 6672 . . . . . . 7 (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))) = (𝑆‘( I ↾ 𝐷))
64 1p1e2 11756 . . . . . . . . 9 (1 + 1) = 2
6564oveq2i 7161 . . . . . . . 8 (-1↑(1 + 1)) = (-1↑2)
66 neg1sqe1 13554 . . . . . . . 8 (-1↑2) = 1
6765, 66eqtri 2849 . . . . . . 7 (-1↑(1 + 1)) = 1
6858, 63, 673eqtr4i 2859 . . . . . 6 (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))) = (-1↑(1 + 1))
69682a1i 12 . . . . 5 (𝑁 ∈ ℕ → (1 ≤ 𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 1, if(𝑖 ≤ 1, (𝑖 − 1), 𝑖)))) = (-1↑(1 + 1))))
70 simplr 765 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛 ∈ ℕ)
7170peano2nnd 11649 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 + 1) ∈ ℕ)
72 simpll 763 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑁 ∈ ℕ)
73 simpr 485 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 + 1) ≤ 𝑁)
7471, 72, 733jca 1122 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → ((𝑛 + 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑛 + 1) ≤ 𝑁))
75 elfz1b 12971 . . . . . . . . . . . 12 ((𝑛 + 1) ∈ (1...𝑁) ↔ ((𝑛 + 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑛 + 1) ≤ 𝑁))
7674, 75sylibr 235 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 + 1) ∈ (1...𝑁))
7776, 3syl6eleqr 2929 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 + 1) ∈ 𝐷)
783psgnfzto1stlem 30675 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ 𝐷) → (𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))))
7970, 77, 78syl2anc 584 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))))
8079adantlr 711 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))))
8180fveq2d 6673 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))) = (𝑆‘(((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))))
8255a1i 11 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → 𝐷 ∈ Fin)
83 eqid 2826 . . . . . . . . . 10 ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
84 psgnfzto1st.g . . . . . . . . . 10 𝐺 = (SymGrp‘𝐷)
85 psgnfzto1st.b . . . . . . . . . 10 𝐵 = (Base‘𝐺)
8683, 84, 85symgtrf 18533 . . . . . . . . 9 ran (pmTrsp‘𝐷) ⊆ 𝐵
87 eqid 2826 . . . . . . . . . . . 12 (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
883, 87pmtrto1cl 30674 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ ran (pmTrsp‘𝐷))
8970, 77, 88syl2anc 584 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → ((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ ran (pmTrsp‘𝐷))
9089adantlr 711 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → ((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ ran (pmTrsp‘𝐷))
9186, 90sseldi 3969 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → ((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ 𝐵)
9270nnred 11647 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛 ∈ ℝ)
93 1red 10636 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 1 ∈ ℝ)
9492, 93readdcld 10664 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 + 1) ∈ ℝ)
9572nnred 11647 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑁 ∈ ℝ)
9692lep1d 11565 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛 ≤ (𝑛 + 1))
9792, 94, 95, 96, 73letrd 10791 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛𝑁)
9870, 72, 973jca 1122 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑛𝑁))
99 elfz1b 12971 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑛𝑁))
10098, 99sylibr 235 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛 ∈ (1...𝑁))
101100, 3syl6eleqr 2929 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛𝐷)
102101adantlr 711 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛𝐷)
103 eqid 2826 . . . . . . . . . 10 (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))) = (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))
1043, 103, 84, 85fzto1st 30678 . . . . . . . . 9 (𝑛𝐷 → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))) ∈ 𝐵)
105102, 104syl 17 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))) ∈ 𝐵)
10684, 56, 85psgnco 20662 . . . . . . . 8 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ 𝐵 ∧ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))) ∈ 𝐵) → (𝑆‘(((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))) = ((𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) · (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))))
10782, 91, 105, 106syl3anc 1365 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘(((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∘ (𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))) = ((𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) · (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))))
10884, 83, 56psgnpmtr 18574 . . . . . . . . . . 11 (((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)}) ∈ ran (pmTrsp‘𝐷) → (𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) = -1)
10989, 108syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) = -1)
110109adantlr 711 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) = -1)
11197adantlr 711 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → 𝑛𝑁)
112 simplr 765 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1))))
113111, 112mpd 15 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))
114110, 113oveq12d 7168 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → ((𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) · (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))) = (-1 · (-1↑(𝑛 + 1))))
115 neg1cn 11745 . . . . . . . . . . 11 -1 ∈ ℂ
116 peano2nn 11644 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
117116nnnn0d 11949 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
118 expp1 13431 . . . . . . . . . . 11 ((-1 ∈ ℂ ∧ (𝑛 + 1) ∈ ℕ0) → (-1↑((𝑛 + 1) + 1)) = ((-1↑(𝑛 + 1)) · -1))
119115, 117, 118sylancr 587 . . . . . . . . . 10 (𝑛 ∈ ℕ → (-1↑((𝑛 + 1) + 1)) = ((-1↑(𝑛 + 1)) · -1))
120115a1i 11 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → -1 ∈ ℂ)
121120, 117expcld 13505 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (-1↑(𝑛 + 1)) ∈ ℂ)
122121, 120mulcomd 10656 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((-1↑(𝑛 + 1)) · -1) = (-1 · (-1↑(𝑛 + 1))))
123119, 122eqtr2d 2862 . . . . . . . . 9 (𝑛 ∈ ℕ → (-1 · (-1↑(𝑛 + 1))) = (-1↑((𝑛 + 1) + 1)))
124123ad3antlr 727 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (-1 · (-1↑(𝑛 + 1))) = (-1↑((𝑛 + 1) + 1)))
125114, 124eqtrd 2861 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → ((𝑆‘((pmTrsp‘𝐷)‘{𝑛, (𝑛 + 1)})) · (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖))))) = (-1↑((𝑛 + 1) + 1)))
12681, 107, 1253eqtrd 2865 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) ∧ (𝑛 + 1) ≤ 𝑁) → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))) = (-1↑((𝑛 + 1) + 1)))
127126ex 413 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝑛𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, 𝑛, if(𝑖𝑛, (𝑖 − 1), 𝑖)))) = (-1↑(𝑛 + 1)))) → ((𝑛 + 1) ≤ 𝑁 → (𝑆‘(𝑖𝐷 ↦ if(𝑖 = 1, (𝑛 + 1), if(𝑖 ≤ (𝑛 + 1), (𝑖 − 1), 𝑖)))) = (-1↑((𝑛 + 1) + 1))))
12818, 29, 40, 53, 69, 127nnindd 30468 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ) → (𝐼𝑁 → (𝑆𝑃) = (-1↑(𝐼 + 1))))
129128imp 407 . . 3 (((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ 𝐼𝑁) → (𝑆𝑃) = (-1↑(𝐼 + 1)))
1307, 129sylbi 218 . 2 ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼𝑁) → (𝑆𝑃) = (-1↑(𝐼 + 1)))
1316, 130syl 17 1 (𝐼𝐷 → (𝑆𝑃) = (-1↑(𝐼 + 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107  ifcif 4470  {cpr 4566   class class class wbr 5063  cmpt 5143   I cid 5458  ran crn 5555  cres 5556  ccom 5558  cfv 6354  (class class class)co 7150  Fincfn 8503  cc 10529  1c1 10532   + caddc 10534   · cmul 10536  cle 10670  cmin 10864  -cneg 10865  cn 11632  2c2 11686  0cn0 11891  ...cfz 12887  cexp 13424  Basecbs 16478  SymGrpcsymg 18440  pmTrspcpmtr 18505  pmSgncpsgn 18553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-xor 1498  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-ot 4573  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-tpos 7888  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-xnn0 11962  df-z 11976  df-dec 12093  df-uz 12238  df-rp 12385  df-fz 12888  df-fzo 13029  df-seq 13365  df-exp 13425  df-hash 13686  df-word 13857  df-lsw 13910  df-concat 13918  df-s1 13945  df-substr 13998  df-pfx 14028  df-splice 14107  df-reverse 14116  df-s2 14205  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-0g 16710  df-gsum 16711  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18051  df-minusg 18052  df-subg 18221  df-ghm 18301  df-gim 18344  df-oppg 18419  df-symg 18441  df-pmtr 18506  df-psgn 18555  df-cmn 18844  df-abl 18845  df-mgp 19176  df-ur 19188  df-ring 19235  df-cring 19236  df-oppr 19309  df-dvdsr 19327  df-unit 19328  df-invr 19358  df-dvr 19369  df-drng 19440  df-cnfld 20481
This theorem is referenced by:  madjusmdetlem4  31000
  Copyright terms: Public domain W3C validator