Metamath Proof Explorer

Theorem fzto1st1

Description: Special case where the permutation defined in psgnfzto1st is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypotheses psgnfzto1st.d ⊢D=1…N
psgnfzto1st.p ⊢P=i∈D⟼ifi=1Iifi≤Ii−1i
Assertion fzto1st1 ⊢I=1→P=I↾D

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢D=1…N
2 psgnfzto1st.p ⊢P=i∈D⟼ifi=1Iifi≤Ii−1i
3 simpll ⊢I=1∧i∈D∧i=1→I=1
4 simpr ⊢I=1∧i∈D∧i=1→i=1
5 3 4 eqtr4d ⊢I=1∧i∈D∧i=1→I=i
6 simpr ⊢I=1∧i∈D∧¬i=1∧i≤I→i≤I
7 simplll ⊢I=1∧i∈D∧¬i=1∧i≤I→I=1
8 6 7 breqtrd ⊢I=1∧i∈D∧¬i=1∧i≤I→i≤1
9 simpllr ⊢I=1∧i∈D∧¬i=1∧i≤I→i∈D
10 9 1 eleqtrdi ⊢I=1∧i∈D∧¬i=1∧i≤I→i∈1…N
11 elfzle1 ⊢i∈1…N→1≤i
12 10 11 syl ⊢I=1∧i∈D∧¬i=1∧i≤I→1≤i
13 fz1ssnn ⊢1…N⊆ℕ
14 13 10 sselid ⊢I=1∧i∈D∧¬i=1∧i≤I→i∈ℕ
15 14 nnred ⊢I=1∧i∈D∧¬i=1∧i≤I→i∈ℝ
16 1red ⊢I=1∧i∈D∧¬i=1∧i≤I→1∈ℝ
17 15 16 letri3d ⊢I=1∧i∈D∧¬i=1∧i≤I→i=1↔i≤1∧1≤i
18 8 12 17 mpbir2and ⊢I=1∧i∈D∧¬i=1∧i≤I→i=1
19 simplr ⊢I=1∧i∈D∧¬i=1∧i≤I→¬i=1
20 18 19 pm2.21dd ⊢I=1∧i∈D∧¬i=1∧i≤I→i−1=i
21 eqidd ⊢I=1∧i∈D∧¬i=1∧¬i≤I→i=i
22 20 21 ifeqda ⊢I=1∧i∈D∧¬i=1→ifi≤Ii−1i=i
23 5 22 ifeqda ⊢I=1∧i∈D→ifi=1Iifi≤Ii−1i=i
24 23 mpteq2dva ⊢I=1→i∈D⟼ifi=1Iifi≤Ii−1i=i∈D⟼i
25 mptresid ⊢I↾D=i∈D⟼i
26 24 2 25 3eqtr4g ⊢I=1→P=I↾D