Metamath Proof Explorer

Theorem psgnfzto1stlem

Description: Lemma for psgnfzto1st . Our permutation of rank ( n + 1 ) can be written as a permutation of rank n composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypothesis psgnfzto1st.d 
|- D = ( 1 ... N )
Assertion psgnfzto1stlem 
|- ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d 
 |-  D = ( 1 ... N )
2 ovex 
 |-  ( K + 1 ) e. _V
3 ovex 
 |-  ( i - 1 ) e. _V
4 vex 
 |-  i e. _V
5 3 4 ifex 
 |-  if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) e. _V
6 2 5 ifex 
 |-  if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) e. _V
7 eqid 
 |-  ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) )
8 6 7 fnmpti 
 |-  ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) Fn D
9 8 a1i 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) Fn D )
10 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
11 1 10 pmtrto1cl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) e. ran ( pmTrsp ` D ) )
12 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
13 10 12 pmtrff1o 
 |-  ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) e. ran ( pmTrsp ` D ) -> ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) : D -1-1-onto-> D )
14 f1ofn 
 |-  ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) : D -1-1-onto-> D -> ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) Fn D )
15 11 13 14 3syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) Fn D )
16 simpr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ i = 1 ) -> i = 1 )
17 16 iftrued 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ i = 1 ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) = K )
18 simpl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. NN )
19 18 nnred 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. RR )
20 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
21 1 eleq2i 
 |-  ( ( K + 1 ) e. D <-> ( K + 1 ) e. ( 1 ... N ) )
22 21 biimpi 
 |-  ( ( K + 1 ) e. D -> ( K + 1 ) e. ( 1 ... N ) )
23 22 adantl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. ( 1 ... N ) )
24 20 23 sseldi 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. NN )
25 24 nnred 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. RR )
26 elfz1b 
 |-  ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) e. NN /\ N e. NN /\ ( K + 1 ) <_ N ) )
27 26 simp2bi 
 |-  ( ( K + 1 ) e. ( 1 ... N ) -> N e. NN )
28 22 27 syl 
 |-  ( ( K + 1 ) e. D -> N e. NN )
29 28 adantl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> N e. NN )
30 29 nnred 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> N e. RR )
31 19 lep1d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K <_ ( K + 1 ) )
32 elfzle2 
 |-  ( ( K + 1 ) e. ( 1 ... N ) -> ( K + 1 ) <_ N )
33 23 32 syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) <_ N )
34 19 25 30 31 33 letrd 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K <_ N )
35 29 nnzd 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> N e. ZZ )
36 fznn 
 |-  ( N e. ZZ -> ( K e. ( 1 ... N ) <-> ( K e. NN /\ K <_ N ) ) )
37 35 36 syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K e. ( 1 ... N ) <-> ( K e. NN /\ K <_ N ) ) )
38 18 34 37 mpbir2and 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. ( 1 ... N ) )
39 38 1 eleqtrrdi 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. D )
40 39 ad2antrr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ i = 1 ) -> K e. D )
41 17 40 eqeltrd 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ i = 1 ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D )
42 simpr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) -> -. i = 1 )
43 42 iffalsed 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) = if ( i <_ K , ( i - 1 ) , i ) )
44 simpr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i <_ K )
45 44 iftrued 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> if ( i <_ K , ( i - 1 ) , i ) = ( i - 1 ) )
46 42 adantr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> -. i = 1 )
47 1 20 eqsstri 
 |-  D C_ NN
48 simpllr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i e. D )
49 47 48 sseldi 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i e. NN )
50 nn1m1nn 
 |-  ( i e. NN -> ( i = 1 \/ ( i - 1 ) e. NN ) )
51 49 50 syl 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i = 1 \/ ( i - 1 ) e. NN ) )
52 51 ord 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( -. i = 1 -> ( i - 1 ) e. NN ) )
53 46 52 mpd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) e. NN )
54 53 nnred 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) e. RR )
55 49 nnred 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i e. RR )
56 30 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> N e. RR )
57 55 lem1d 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) <_ i )
58 48 1 eleqtrdi 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i e. ( 1 ... N ) )
59 elfzle2 
 |-  ( i e. ( 1 ... N ) -> i <_ N )
60 58 59 syl 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> i <_ N )
61 54 55 56 57 60 letrd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) <_ N )
62 53 61 jca 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( ( i - 1 ) e. NN /\ ( i - 1 ) <_ N ) )
63 fznn 
 |-  ( N e. ZZ -> ( ( i - 1 ) e. ( 1 ... N ) <-> ( ( i - 1 ) e. NN /\ ( i - 1 ) <_ N ) ) )
64 35 63 syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( i - 1 ) e. ( 1 ... N ) <-> ( ( i - 1 ) e. NN /\ ( i - 1 ) <_ N ) ) )
65 64 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( ( i - 1 ) e. ( 1 ... N ) <-> ( ( i - 1 ) e. NN /\ ( i - 1 ) <_ N ) ) )
66 62 65 mpbird 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) e. ( 1 ... N ) )
67 66 1 eleqtrrdi 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> ( i - 1 ) e. D )
68 45 67 eqeltrd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ i <_ K ) -> if ( i <_ K , ( i - 1 ) , i ) e. D )
69 simpr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ -. i <_ K ) -> -. i <_ K )
70 69 iffalsed 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ -. i <_ K ) -> if ( i <_ K , ( i - 1 ) , i ) = i )
71 simpllr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ -. i <_ K ) -> i e. D )
72 70 71 eqeltrd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) /\ -. i <_ K ) -> if ( i <_ K , ( i - 1 ) , i ) e. D )
73 68 72 pm2.61dan 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) -> if ( i <_ K , ( i - 1 ) , i ) e. D )
74 43 73 eqeltrd 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) /\ -. i = 1 ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D )
75 41 74 pm2.61dan 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ i e. D ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D )
76 75 ralrimiva 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> A. i e. D if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D )
77 eqid 
 |-  ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) )
78 77 fnmpt 
 |-  ( A. i e. D if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D -> ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) Fn D )
79 76 78 syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) Fn D )
80 77 rnmptss 
 |-  ( A. i e. D if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D -> ran ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) C_ D )
81 76 80 syl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ran ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) C_ D )
82 fnco 
 |-  ( ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) Fn D /\ ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) Fn D /\ ran ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) C_ D ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) Fn D )
83 15 79 81 82 syl3anc 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) Fn D )
84 simpr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ x = 1 ) -> x = 1 )
85 84 iftrued 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ x = 1 ) -> if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) = K )
86 85 fveq2d 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ x = 1 ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` K ) )
87 fzfi 
 |-  ( 1 ... N ) e. Fin
88 1 87 eqeltri 
 |-  D e. Fin
89 88 a1i 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> D e. Fin )
90 23 21 sylibr 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. D )
91 19 ltp1d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K < ( K + 1 ) )
92 19 91 ltned 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K =/= ( K + 1 ) )
93 10 pmtrprfv 
 |-  ( ( D e. Fin /\ ( K e. D /\ ( K + 1 ) e. D /\ K =/= ( K + 1 ) ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` K ) = ( K + 1 ) )
94 89 39 90 92 93 syl13anc 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` K ) = ( K + 1 ) )
95 94 ad2antrr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ x = 1 ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` K ) = ( K + 1 ) )
96 86 95 eqtr2d 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ x = 1 ) -> ( K + 1 ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) )
97 88 a1i 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> D e. Fin )
98 39 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K e. D )
99 90 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( K + 1 ) e. D )
100 92 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K =/= ( K + 1 ) )
101 10 pmtrprfv2 
 |-  ( ( D e. Fin /\ ( K e. D /\ ( K + 1 ) e. D /\ K =/= ( K + 1 ) ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( K + 1 ) ) = K )
102 97 98 99 100 101 syl13anc 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( K + 1 ) ) = K )
103 91 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K < ( K + 1 ) )
104 simpr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> x = ( K + 1 ) )
105 103 104 breqtrrd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K < x )
106 19 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K e. RR )
107 simpr 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> x e. D )
108 47 107 sseldi 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> x e. NN )
109 108 nnred 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> x e. RR )
110 109 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> x e. RR )
111 106 110 ltnled 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( K < x <-> -. x <_ K ) )
112 105 111 mpbid 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> -. x <_ K )
113 112 iffalsed 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> if ( x <_ K , ( x - 1 ) , x ) = x )
114 113 104 eqtrd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> if ( x <_ K , ( x - 1 ) , x ) = ( K + 1 ) )
115 114 fveq2d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( K + 1 ) ) )
116 104 oveq1d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( x - 1 ) = ( ( K + 1 ) - 1 ) )
117 106 recnd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> K e. CC )
118 1cnd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> 1 e. CC )
119 117 118 pncand 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( ( K + 1 ) - 1 ) = K )
120 116 119 eqtrd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( x - 1 ) = K )
121 102 115 120 3eqtr4rd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x = ( K + 1 ) ) -> ( x - 1 ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
122 simplr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x <_ ( K + 1 ) )
123 simpr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x =/= ( K + 1 ) )
124 123 necomd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K + 1 ) =/= x )
125 109 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x e. RR )
126 25 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K + 1 ) e. RR )
127 125 126 ltlend 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x < ( K + 1 ) <-> ( x <_ ( K + 1 ) /\ ( K + 1 ) =/= x ) ) )
128 122 124 127 mpbir2and 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x < ( K + 1 ) )
129 108 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x e. NN )
130 simpll 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> K e. NN )
131 130 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> K e. NN )
132 nnleltp1 
 |-  ( ( x e. NN /\ K e. NN ) -> ( x <_ K <-> x < ( K + 1 ) ) )
133 129 131 132 syl2anc 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x <_ K <-> x < ( K + 1 ) ) )
134 128 133 mpbird 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x <_ K )
135 134 iftrued 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> if ( x <_ K , ( x - 1 ) , x ) = ( x - 1 ) )
136 135 fveq2d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( x - 1 ) ) )
137 88 a1i 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> D e. Fin )
138 39 ad4antr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> K e. D )
139 simp-5r 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K + 1 ) e. D )
140 simpr 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> -. x = 1 )
141 140 ad2antrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> -. x = 1 )
142 elnn1uz2 
 |-  ( x e. NN <-> ( x = 1 \/ x e. ( ZZ>= ` 2 ) ) )
143 129 142 sylib 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x = 1 \/ x e. ( ZZ>= ` 2 ) ) )
144 143 ord 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( -. x = 1 -> x e. ( ZZ>= ` 2 ) ) )
145 141 144 mpd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x e. ( ZZ>= ` 2 ) )
146 uz2m1nn 
 |-  ( x e. ( ZZ>= ` 2 ) -> ( x - 1 ) e. NN )
147 145 146 syl 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) e. NN )
148 139 28 syl 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> N e. NN )
149 147 nnred 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) e. RR )
150 131 139 30 syl2anc 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> N e. RR )
151 125 lem1d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) <_ x )
152 107 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x e. D )
153 152 1 eleqtrdi 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x e. ( 1 ... N ) )
154 elfzle2 
 |-  ( x e. ( 1 ... N ) -> x <_ N )
155 153 154 syl 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> x <_ N )
156 149 125 150 151 155 letrd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) <_ N )
157 147 148 156 3jca 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( ( x - 1 ) e. NN /\ N e. NN /\ ( x - 1 ) <_ N ) )
158 elfz1b 
 |-  ( ( x - 1 ) e. ( 1 ... N ) <-> ( ( x - 1 ) e. NN /\ N e. NN /\ ( x - 1 ) <_ N ) )
159 157 158 sylibr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) e. ( 1 ... N ) )
160 159 1 eleqtrrdi 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) e. D )
161 138 139 160 3jca 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K e. D /\ ( K + 1 ) e. D /\ ( x - 1 ) e. D ) )
162 131 139 92 syl2anc 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> K =/= ( K + 1 ) )
163 simpr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> K = ( x - 1 ) )
164 163 oveq1d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> ( K + 1 ) = ( ( x - 1 ) + 1 ) )
165 109 recnd 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> x e. CC )
166 165 ad3antrrr 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> x e. CC )
167 1cnd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> 1 e. CC )
168 166 167 npcand 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> ( ( x - 1 ) + 1 ) = x )
169 164 168 eqtr2d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ K = ( x - 1 ) ) -> x = ( K + 1 ) )
170 169 ex 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) -> ( K = ( x - 1 ) -> x = ( K + 1 ) ) )
171 170 necon3d 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) -> ( x =/= ( K + 1 ) -> K =/= ( x - 1 ) ) )
172 171 imp 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> K =/= ( x - 1 ) )
173 149 125 126 151 128 lelttrd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) < ( K + 1 ) )
174 149 173 ltned 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) =/= ( K + 1 ) )
175 174 necomd 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K + 1 ) =/= ( x - 1 ) )
176 162 172 175 3jca 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( K =/= ( K + 1 ) /\ K =/= ( x - 1 ) /\ ( K + 1 ) =/= ( x - 1 ) ) )
177 10 pmtrprfv3 
 |-  ( ( D e. Fin /\ ( K e. D /\ ( K + 1 ) e. D /\ ( x - 1 ) e. D ) /\ ( K =/= ( K + 1 ) /\ K =/= ( x - 1 ) /\ ( K + 1 ) =/= ( x - 1 ) ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( x - 1 ) ) = ( x - 1 ) )
178 137 161 176 177 syl3anc 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( x - 1 ) ) = ( x - 1 ) )
179 136 178 eqtr2d 
 |-  ( ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) /\ x =/= ( K + 1 ) ) -> ( x - 1 ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
180 121 179 pm2.61dane 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ ( K + 1 ) ) -> ( x - 1 ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
181 109 ad2antrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> x e. RR )
182 19 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> K e. RR )
183 25 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> ( K + 1 ) e. RR )
184 simpr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> x <_ K )
185 31 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> K <_ ( K + 1 ) )
186 181 182 183 184 185 letrd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ x <_ K ) -> x <_ ( K + 1 ) )
187 186 ex 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> ( x <_ K -> x <_ ( K + 1 ) ) )
188 187 con3d 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> ( -. x <_ ( K + 1 ) -> -. x <_ K ) )
189 188 imp 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> -. x <_ K )
190 189 iffalsed 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> if ( x <_ K , ( x - 1 ) , x ) = x )
191 190 fveq2d 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` x ) )
192 88 a1i 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> D e. Fin )
193 39 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K e. D )
194 90 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K + 1 ) e. D )
195 107 ad2antrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> x e. D )
196 193 194 195 3jca 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K e. D /\ ( K + 1 ) e. D /\ x e. D ) )
197 92 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K =/= ( K + 1 ) )
198 19 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K e. RR )
199 25 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K + 1 ) e. RR )
200 109 ad2antrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> x e. RR )
201 91 ad3antrrr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K < ( K + 1 ) )
202 simpr 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> -. x <_ ( K + 1 ) )
203 199 200 ltnled 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( ( K + 1 ) < x <-> -. x <_ ( K + 1 ) ) )
204 202 203 mpbird 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K + 1 ) < x )
205 198 199 200 201 204 lttrd 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K < x )
206 198 205 ltned 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> K =/= x )
207 199 204 ltned 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K + 1 ) =/= x )
208 197 206 207 3jca 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( K =/= ( K + 1 ) /\ K =/= x /\ ( K + 1 ) =/= x ) )
209 10 pmtrprfv3 
 |-  ( ( D e. Fin /\ ( K e. D /\ ( K + 1 ) e. D /\ x e. D ) /\ ( K =/= ( K + 1 ) /\ K =/= x /\ ( K + 1 ) =/= x ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` x ) = x )
210 192 196 208 209 syl3anc 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` x ) = x )
211 191 210 eqtr2d 
 |-  ( ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) /\ -. x <_ ( K + 1 ) ) -> x = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
212 180 211 ifeqda 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
213 140 iffalsed 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) = if ( x <_ K , ( x - 1 ) , x ) )
214 213 fveq2d 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x <_ K , ( x - 1 ) , x ) ) )
215 212 214 eqtr4d 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ -. x = 1 ) -> if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) )
216 96 215 ifeqda 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) )
217 eqidd 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) )
218 eqeq1 
 |-  ( i = x -> ( i = 1 <-> x = 1 ) )
219 breq1 
 |-  ( i = x -> ( i <_ K <-> x <_ K ) )
220 oveq1 
 |-  ( i = x -> ( i - 1 ) = ( x - 1 ) )
221 id 
 |-  ( i = x -> i = x )
222 219 220 221 ifbieq12d 
 |-  ( i = x -> if ( i <_ K , ( i - 1 ) , i ) = if ( x <_ K , ( x - 1 ) , x ) )
223 218 222 ifbieq2d 
 |-  ( i = x -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) = if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) )
224 223 adantl 
 |-  ( ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) /\ i = x ) -> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) = if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) )
225 ovex 
 |-  ( x - 1 ) e. _V
226 vex 
 |-  x e. _V
227 225 226 ifcli 
 |-  if ( x <_ K , ( x - 1 ) , x ) e. _V
228 227 a1i 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> if ( x <_ K , ( x - 1 ) , x ) e. _V )
229 130 228 ifexd 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) e. _V )
230 217 224 107 229 fvmptd 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ` x ) = if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) )
231 230 fveq2d 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ` x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` if ( x = 1 , K , if ( x <_ K , ( x - 1 ) , x ) ) ) )
232 216 231 eqtr4d 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ` x ) ) )
233 breq1 
 |-  ( i = x -> ( i <_ ( K + 1 ) <-> x <_ ( K + 1 ) ) )
234 233 220 221 ifbieq12d 
 |-  ( i = x -> if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) = if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) )
235 218 234 ifbieq2d 
 |-  ( i = x -> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) = if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) )
236 225 226 ifex 
 |-  if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) e. _V
237 2 236 ifex 
 |-  if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) e. _V
238 235 7 237 fvmpt 
 |-  ( x e. D -> ( ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) ` x ) = if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) )
239 238 adantl 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) ` x ) = if ( x = 1 , ( K + 1 ) , if ( x <_ ( K + 1 ) , ( x - 1 ) , x ) ) )
240 funmpt 
 |-  Fun ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) )
241 240 a1i 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> Fun ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) )
242 76 adantr 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> A. i e. D if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D )
243 dmmptg 
 |-  ( A. i e. D if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) e. D -> dom ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) = D )
244 242 243 syl 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> dom ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) = D )
245 107 244 eleqtrrd 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> x e. dom ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) )
246 fvco 
 |-  ( ( Fun ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) /\ x e. dom ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) -> ( ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) ` x ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ` x ) ) )
247 241 245 246 syl2anc 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) ` x ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) ` ( ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ` x ) ) )
248 232 239 247 3eqtr4d 
 |-  ( ( ( K e. NN /\ ( K + 1 ) e. D ) /\ x e. D ) -> ( ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) ` x ) = ( ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) ` x ) )
249 9 83 248 eqfnfvd 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) )