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 ⊢ 𝐷 = ( 1 ... 𝑁 )
psgnfzto1st.p ⊢ 𝑃 = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
Assertion fzto1st1 ( 𝐼 = 1 → 𝑃 = ( I ↾ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢ 𝐷 = ( 1 ... 𝑁 )
2 psgnfzto1st.p ⊢ 𝑃 = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
3 simpll ⊢ ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → 𝐼 = 1 )
4 simpr ⊢ ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → 𝑖 = 1 )
5 3 4 eqtr4d ⊢ ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → 𝐼 = 𝑖 )
6 simpr ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ≤ 𝐼 )
7 simplll ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝐼 = 1 )
8 6 7 breqtrd ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ≤ 1 )
9 simpllr ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ∈ 𝐷 )
10 9 1 eleqtrdi ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
11 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝑖 )
12 10 11 syl ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 1 ≤ 𝑖 )
13 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
14 13 10 sseldi ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ∈ ℕ )
15 14 nnred ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 ∈ ℝ )
16 1red ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 1 ∈ ℝ )
17 15 16 letri3d ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → ( 𝑖 = 1 ↔ ( 𝑖 ≤ 1 ∧ 1 ≤ 𝑖 ) ) )
18 8 12 17 mpbir2and ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → 𝑖 = 1 )
19 simplr ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → ¬ 𝑖 = 1 )
20 18 19 pm2.21dd ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐼 ) → ( 𝑖 − 1 ) = 𝑖 )
21 eqidd ⊢ ( ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ ¬ 𝑖 ≤ 𝐼 ) → 𝑖 = 𝑖 )
22 20 21 ifeqda ⊢ ( ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) → if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) = 𝑖 )
23 5 22 ifeqda ⊢ ( ( 𝐼 = 1 ∧ 𝑖 ∈ 𝐷 ) → if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) = 𝑖 )
24 23 mpteq2dva ⊢ ( 𝐼 = 1 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ 𝑖 ) )
25 mptresid ⊢ ( I ↾ 𝐷 ) = ( 𝑖 ∈ 𝐷 ↦ 𝑖 )
26 24 2 25 3eqtr4g ⊢ ( 𝐼 = 1 → 𝑃 = ( I ↾ 𝐷 ) )