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 ⟼ if i = 1 I if i ≤ I i − 1 i
Assertion fzto1st1 ⊢ I = 1 → P = I ↾ D

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 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 → if i ≤ I i − 1 i = i
23 5 22 ifeqda ⊢ I = 1 ∧ i ∈ D → if i = 1 I if i ≤ I i − 1 i = i
24 23 mpteq2dva ⊢ I = 1 → i ∈ D ⟼ if i = 1 I if i ≤ I i − 1 i = i ∈ D ⟼ i
25 mptresid ⊢ I ↾ D = i ∈ D ⟼ i
26 24 2 25 3eqtr4g ⊢ I = 1 → P = I ↾ D