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 e. 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 e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
3 simpll 
 |-  ( ( ( I = 1 /\ i e. D ) /\ i = 1 ) -> I = 1 )
4 simpr 
 |-  ( ( ( I = 1 /\ i e. D ) /\ i = 1 ) -> i = 1 )
5 3 4 eqtr4d 
 |-  ( ( ( I = 1 /\ i e. D ) /\ i = 1 ) -> I = i )
6 simpr 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i <_ I )
7 simplll 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> I = 1 )
8 6 7 breqtrd 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i <_ 1 )
9 simpllr 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i e. D )
10 9 1 eleqtrdi 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i e. ( 1 ... N ) )
11 elfzle1 
 |-  ( i e. ( 1 ... N ) -> 1 <_ i )
12 10 11 syl 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> 1 <_ i )
13 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
14 13 10 sseldi 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i e. NN )
15 14 nnred 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i e. RR )
16 1red 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> 1 e. RR )
17 15 16 letri3d 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> ( i = 1 <-> ( i <_ 1 /\ 1 <_ i ) ) )
18 8 12 17 mpbir2and 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> i = 1 )
19 simplr 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> -. i = 1 )
20 18 19 pm2.21dd 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ i <_ I ) -> ( i - 1 ) = i )
21 eqidd 
 |-  ( ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) /\ -. i <_ I ) -> i = i )
22 20 21 ifeqda 
 |-  ( ( ( I = 1 /\ i e. D ) /\ -. i = 1 ) -> if ( i <_ I , ( i - 1 ) , i ) = i )
23 5 22 ifeqda 
 |-  ( ( I = 1 /\ i e. D ) -> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) = i )
24 23 mpteq2dva 
 |-  ( I = 1 -> ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) ) = ( i e. D |-> i ) )
25 mptresid 
 |-  ( _I |` D ) = ( i e. D |-> i )
26 24 2 25 3eqtr4g 
 |-  ( I = 1 -> P = ( _I |` D ) )