Metamath Proof Explorer

Theorem poimirlem24

Description: Lemma for poimir , two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem28.1 
|- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
poimirlem28.2 
|- ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
poimirlem25.3 
|- ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
poimirlem25.4 
|- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem24.5 
|- ( ph -> V e. ( 0 ... N ) )
Assertion poimirlem24 
|- ( ph -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem28.1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
3 poimirlem28.2 
 |-  ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
4 poimirlem25.3 
 |-  ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
5 poimirlem25.4 
 |-  ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
6 poimirlem24.5 
 |-  ( ph -> V e. ( 0 ... N ) )
7 nfv 
 |-  F/ j ( ph /\ y e. ( 0 ... ( N - 1 ) ) )
8 nfcsb1v 
 |-  F/_ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
9 nfcv 
 |-  F/_ j ( 1 ... N )
10 nfcv 
 |-  F/_ j ( 0 ... K )
11 8 9 10 nff 
 |-  F/ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K )
12 7 11 nfim 
 |-  F/ j ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
13 eleq1 
 |-  ( j = y -> ( j e. ( 0 ... ( N - 1 ) ) <-> y e. ( 0 ... ( N - 1 ) ) ) )
14 13 anbi2d 
 |-  ( j = y -> ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) <-> ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) ) )
15 csbeq1a 
 |-  ( j = y -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
16 15 feq1d 
 |-  ( j = y -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
17 14 16 imbi12d 
 |-  ( j = y -> ( ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
18 1 nncnd 
 |-  ( ph -> N e. CC )
19 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
20 18 19 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
21 1 nnzd 
 |-  ( ph -> N e. ZZ )
22 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
23 21 22 syl 
 |-  ( ph -> ( N - 1 ) e. ZZ )
24 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
25 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
26 23 24 25 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
27 20 26 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
28 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
29 27 28 syl 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
30 29 sselda 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. ( 0 ... N ) )
31 elun 
 |-  ( y e. ( { 1 } u. { 0 } ) <-> ( y e. { 1 } \/ y e. { 0 } ) )
32 fzofzp1 
 |-  ( x e. ( 0 ..^ K ) -> ( x + 1 ) e. ( 0 ... K ) )
33 elsni 
 |-  ( y e. { 1 } -> y = 1 )
34 33 oveq2d 
 |-  ( y e. { 1 } -> ( x + y ) = ( x + 1 ) )
35 34 eleq1d 
 |-  ( y e. { 1 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 1 ) e. ( 0 ... K ) ) )
36 32 35 syl5ibrcom 
 |-  ( x e. ( 0 ..^ K ) -> ( y e. { 1 } -> ( x + y ) e. ( 0 ... K ) ) )
37 elfzoelz 
 |-  ( x e. ( 0 ..^ K ) -> x e. ZZ )
38 37 zcnd 
 |-  ( x e. ( 0 ..^ K ) -> x e. CC )
39 38 addid1d 
 |-  ( x e. ( 0 ..^ K ) -> ( x + 0 ) = x )
40 elfzofz 
 |-  ( x e. ( 0 ..^ K ) -> x e. ( 0 ... K ) )
41 39 40 eqeltrd 
 |-  ( x e. ( 0 ..^ K ) -> ( x + 0 ) e. ( 0 ... K ) )
42 elsni 
 |-  ( y e. { 0 } -> y = 0 )
43 42 oveq2d 
 |-  ( y e. { 0 } -> ( x + y ) = ( x + 0 ) )
44 43 eleq1d 
 |-  ( y e. { 0 } -> ( ( x + y ) e. ( 0 ... K ) <-> ( x + 0 ) e. ( 0 ... K ) ) )
45 41 44 syl5ibrcom 
 |-  ( x e. ( 0 ..^ K ) -> ( y e. { 0 } -> ( x + y ) e. ( 0 ... K ) ) )
46 36 45 jaod 
 |-  ( x e. ( 0 ..^ K ) -> ( ( y e. { 1 } \/ y e. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
47 31 46 syl5bi 
 |-  ( x e. ( 0 ..^ K ) -> ( y e. ( { 1 } u. { 0 } ) -> ( x + y ) e. ( 0 ... K ) ) )
48 47 imp 
 |-  ( ( x e. ( 0 ..^ K ) /\ y e. ( { 1 } u. { 0 } ) ) -> ( x + y ) e. ( 0 ... K ) )
49 48 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. ( 0 ..^ K ) /\ y e. ( { 1 } u. { 0 } ) ) ) -> ( x + y ) e. ( 0 ... K ) )
50 4 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
51 1ex 
 |-  1 e. _V
52 51 fconst 
 |-  ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 }
53 c0ex 
 |-  0 e. _V
54 53 fconst 
 |-  ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 }
55 52 54 pm3.2i 
 |-  ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } )
56 dff1o3 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
57 56 simprbi 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
58 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
59 5 57 58 3syl 
 |-  ( ph -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
60 elfznn0 
 |-  ( j e. ( 0 ... N ) -> j e. NN0 )
61 60 nn0red 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
62 61 ltp1d 
 |-  ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
63 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
64 62 63 syl 
 |-  ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
65 64 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( U " (/) ) )
66 ima0 
 |-  ( U " (/) ) = (/)
67 65 66 eqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
68 59 67 sylan9req 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
69 fun 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } ) /\ ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
70 55 68 69 sylancr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
71 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
72 60 71 syl 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
73 nnuz 
 |-  NN = ( ZZ>= ` 1 )
74 72 73 eleqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
75 elfzuz3 
 |-  ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
76 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
77 74 75 76 syl2anc 
 |-  ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
78 77 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
79 imaundi 
 |-  ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) )
80 78 79 eqtr2di 
 |-  ( j e. ( 0 ... N ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( U " ( 1 ... N ) ) )
81 f1ofo 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
82 foima 
 |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
83 5 81 82 3syl 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
84 80 83 sylan9eqr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
85 84 feq2d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
86 70 85 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
87 ovex 
 |-  ( 1 ... N ) e. _V
88 87 a1i 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. _V )
89 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
90 49 50 86 88 88 89 off 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
91 30 90 syldan 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
92 12 17 91 chvarfv 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
93 fzp1elp1 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) )
94 20 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
95 94 eleq2d 
 |-  ( ph -> ( ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
96 95 biimpa 
 |-  ( ( ph /\ ( y + 1 ) e. ( 0 ... ( ( N - 1 ) + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
97 93 96 sylan2 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( 0 ... N ) )
98 nfv 
 |-  F/ j ( ph /\ ( y + 1 ) e. ( 0 ... N ) )
99 nfcsb1v 
 |-  F/_ j [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
100 99 9 10 nff 
 |-  F/ j [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K )
101 98 100 nfim 
 |-  F/ j ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
102 ovex 
 |-  ( y + 1 ) e. _V
103 eleq1 
 |-  ( j = ( y + 1 ) -> ( j e. ( 0 ... N ) <-> ( y + 1 ) e. ( 0 ... N ) ) )
104 103 anbi2d 
 |-  ( j = ( y + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) ) )
105 csbeq1a 
 |-  ( j = ( y + 1 ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
106 105 feq1d 
 |-  ( j = ( y + 1 ) -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
107 104 106 imbi12d 
 |-  ( j = ( y + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
108 101 102 107 90 vtoclf 
 |-  ( ( ph /\ ( y + 1 ) e. ( 0 ... N ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
109 97 108 syldan 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
110 csbeq1 
 |-  ( y = if ( y < V , y , ( y + 1 ) ) -> [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
111 110 feq1d 
 |-  ( y = if ( y < V , y , ( y + 1 ) ) -> ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
112 csbeq1 
 |-  ( ( y + 1 ) = if ( y < V , y , ( y + 1 ) ) -> [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
113 112 feq1d 
 |-  ( ( y + 1 ) = if ( y < V , y , ( y + 1 ) ) -> ( [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
114 111 113 ifboth 
 |-  ( ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) /\ [_ ( y + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
115 92 109 114 syl2anc 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
116 ovex 
 |-  ( 0 ... K ) e. _V
117 116 87 elmap 
 |-  ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) <-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
118 115 117 sylibr 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) )
119 118 fmpttd 
 |-  ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
120 ovex 
 |-  ( ( 0 ... K ) ^m ( 1 ... N ) ) e. _V
121 ovex 
 |-  ( 0 ... ( N - 1 ) ) e. _V
122 120 121 elmap 
 |-  ( ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) <-> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
123 119 122 sylibr 
 |-  ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) )
124 rneq 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ran x = ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
125 124 mpteq1d 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p e. ran x |-> B ) = ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
126 125 rneqd 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ran ( p e. ran x |-> B ) = ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
127 126 sseq2d 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) <-> ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) ) )
128 124 rexeqdv 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( E. p e. ran x ( p ` N ) =/= 0 <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) )
129 127 128 anbi12d 
 |-  ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
130 129 ceqsrexv 
 |-  ( ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
131 123 130 syl 
 |-  ( ph -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
132 dfss3 
 |-  ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> A. i e. ( 0 ... ( N - 1 ) ) i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) )
133 ovex 
 |-  ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
134 133 2 csbie 
 |-  [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = C
135 134 csbeq2i 
 |-  [_ <. T , U >. / s ]_ [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ <. T , U >. / s ]_ C
136 opex 
 |-  <. T , U >. e. _V
137 136 a1i 
 |-  ( ph -> <. T , U >. e. _V )
138 fveq2 
 |-  ( s = <. T , U >. -> ( 1st ` s ) = ( 1st ` <. T , U >. ) )
139 fex 
 |-  ( ( T : ( 1 ... N ) --> ( 0 ..^ K ) /\ ( 1 ... N ) e. _V ) -> T e. _V )
140 4 87 139 sylancl 
 |-  ( ph -> T e. _V )
141 f1oexrnex 
 |-  ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( 1 ... N ) e. _V ) -> U e. _V )
142 5 87 141 sylancl 
 |-  ( ph -> U e. _V )
143 op1stg 
 |-  ( ( T e. _V /\ U e. _V ) -> ( 1st ` <. T , U >. ) = T )
144 140 142 143 syl2anc 
 |-  ( ph -> ( 1st ` <. T , U >. ) = T )
145 138 144 sylan9eqr 
 |-  ( ( ph /\ s = <. T , U >. ) -> ( 1st ` s ) = T )
146 fveq2 
 |-  ( s = <. T , U >. -> ( 2nd ` s ) = ( 2nd ` <. T , U >. ) )
147 op2ndg 
 |-  ( ( T e. _V /\ U e. _V ) -> ( 2nd ` <. T , U >. ) = U )
148 140 142 147 syl2anc 
 |-  ( ph -> ( 2nd ` <. T , U >. ) = U )
149 146 148 sylan9eqr 
 |-  ( ( ph /\ s = <. T , U >. ) -> ( 2nd ` s ) = U )
150 imaeq1 
 |-  ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( U " ( 1 ... j ) ) )
151 150 xpeq1d 
 |-  ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... j ) ) X. { 1 } ) )
152 imaeq1 
 |-  ( ( 2nd ` s ) = U -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( U " ( ( j + 1 ) ... N ) ) )
153 152 xpeq1d 
 |-  ( ( 2nd ` s ) = U -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
154 151 153 uneq12d 
 |-  ( ( 2nd ` s ) = U -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
155 149 154 syl 
 |-  ( ( ph /\ s = <. T , U >. ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
156 145 155 oveq12d 
 |-  ( ( ph /\ s = <. T , U >. ) -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
157 156 csbeq1d 
 |-  ( ( ph /\ s = <. T , U >. ) -> [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
158 137 157 csbied 
 |-  ( ph -> [_ <. T , U >. / s ]_ [_ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
159 135 158 eqtr3id 
 |-  ( ph -> [_ <. T , U >. / s ]_ C = [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
160 159 csbeq2dv 
 |-  ( ph -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
161 160 eqeq2d 
 |-  ( ph -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
162 161 rexbidv 
 |-  ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
163 vex 
 |-  i e. _V
164 eqid 
 |-  ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) = ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B )
165 164 elrnmpt 
 |-  ( i e. _V -> ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B ) )
166 163 165 ax-mp 
 |-  ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B )
167 nfv 
 |-  F/ k i = B
168 nfcsb1v 
 |-  F/_ p [_ k / p ]_ B
169 168 nfeq2 
 |-  F/ p i = [_ k / p ]_ B
170 csbeq1a 
 |-  ( p = k -> B = [_ k / p ]_ B )
171 170 eqeq2d 
 |-  ( p = k -> ( i = B <-> i = [_ k / p ]_ B ) )
172 167 169 171 cbvrexw 
 |-  ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = B <-> E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B )
173 ovex 
 |-  ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
174 173 csbex 
 |-  [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
175 174 rgenw 
 |-  A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
176 eqid 
 |-  ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
177 csbeq1 
 |-  ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> [_ k / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
178 vex 
 |-  y e. _V
179 178 102 ifex 
 |-  if ( y < V , y , ( y + 1 ) ) e. _V
180 csbnestgw 
 |-  ( if ( y < V , y , ( y + 1 ) ) e. _V -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
181 179 180 ax-mp 
 |-  [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B = [_ [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B
182 177 181 eqtr4di 
 |-  ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> [_ k / p ]_ B = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
183 182 eqeq2d 
 |-  ( k = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( i = [_ k / p ]_ B <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
184 176 183 rexrnmptw 
 |-  ( A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V -> ( E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B ) )
185 175 184 ax-mp 
 |-  ( E. k e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) i = [_ k / p ]_ B <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
186 166 172 185 3bitri 
 |-  ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) / p ]_ B )
187 162 186 bitr4di 
 |-  ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) ) )
188 29 sselda 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. ( 0 ... N ) )
189 188 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( 0 ... N ) )
190 elfzelz 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
191 190 zred 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
192 191 adantl 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
193 ltne 
 |-  ( ( y e. RR /\ y < V ) -> V =/= y )
194 193 necomd 
 |-  ( ( y e. RR /\ y < V ) -> y =/= V )
195 192 194 sylan 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y =/= V )
196 eldifsn 
 |-  ( y e. ( ( 0 ... N ) \ { V } ) <-> ( y e. ( 0 ... N ) /\ y =/= V ) )
197 189 195 196 sylanbrc 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < V ) -> y e. ( ( 0 ... N ) \ { V } ) )
198 97 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( 0 ... N ) )
199 6 elfzelzd 
 |-  ( ph -> V e. ZZ )
200 199 zred 
 |-  ( ph -> V e. RR )
201 200 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V e. RR )
202 zre 
 |-  ( V e. ZZ -> V e. RR )
203 zre 
 |-  ( y e. ZZ -> y e. RR )
204 lenlt 
 |-  ( ( V e. RR /\ y e. RR ) -> ( V <_ y <-> -. y < V ) )
205 202 203 204 syl2an 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> -. y < V ) )
206 zleltp1 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> V < ( y + 1 ) ) )
207 205 206 bitr3d 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( -. y < V <-> V < ( y + 1 ) ) )
208 199 190 207 syl2an 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( -. y < V <-> V < ( y + 1 ) ) )
209 208 biimpa 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V < ( y + 1 ) )
210 201 209 gtned 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) =/= V )
211 eldifsn 
 |-  ( ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) <-> ( ( y + 1 ) e. ( 0 ... N ) /\ ( y + 1 ) =/= V ) )
212 198 210 211 sylanbrc 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) )
213 197 212 ifclda 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) )
214 nfcsb1v 
 |-  F/_ j [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
215 214 nfeq2 
 |-  F/ j i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
216 csbeq1a 
 |-  ( j = if ( y < V , y , ( y + 1 ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
217 216 eqeq2d 
 |-  ( j = if ( y < V , y , ( y + 1 ) ) -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
218 215 217 rspce 
 |-  ( ( if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) /\ i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C )
219 218 ex 
 |-  ( if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
220 213 219 syl 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
221 220 rexlimdva 
 |-  ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
222 nfv 
 |-  F/ j ph
223 nfcv 
 |-  F/_ j ( 0 ... ( N - 1 ) )
224 223 215 nfrex 
 |-  F/ j E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
225 eldifi 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ( 0 ... N ) )
226 225 60 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. NN0 )
227 226 nn0ge0d 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> 0 <_ j )
228 227 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> 0 <_ j )
229 226 nn0red 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. RR )
230 229 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. RR )
231 200 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V e. RR )
232 21 zred 
 |-  ( ph -> N e. RR )
233 232 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> N e. RR )
234 simpr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < V )
235 elfzle2 
 |-  ( V e. ( 0 ... N ) -> V <_ N )
236 6 235 syl 
 |-  ( ph -> V <_ N )
237 236 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V <_ N )
238 230 231 233 234 237 ltletrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < N )
239 225 elfzelzd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ZZ )
240 zltlem1 
 |-  ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> j <_ ( N - 1 ) ) )
241 239 21 240 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < N <-> j <_ ( N - 1 ) ) )
242 241 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j < N <-> j <_ ( N - 1 ) ) )
243 238 242 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j <_ ( N - 1 ) )
244 0z 
 |-  0 e. ZZ
245 elfz 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
246 244 245 mp3an2 
 |-  ( ( j e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
247 239 23 246 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
248 247 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
249 228 243 248 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. ( 0 ... ( N - 1 ) ) )
250 0red 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 e. RR )
251 200 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V e. RR )
252 229 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. RR )
253 elfzle1 
 |-  ( V e. ( 0 ... N ) -> 0 <_ V )
254 6 253 syl 
 |-  ( ph -> 0 <_ V )
255 254 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 <_ V )
256 lenlt 
 |-  ( ( V e. RR /\ j e. RR ) -> ( V <_ j <-> -. j < V ) )
257 200 229 256 syl2an 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V <_ j <-> -. j < V ) )
258 257 biimpar 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V <_ j )
259 eldifsni 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j =/= V )
260 259 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j =/= V )
261 ltlen 
 |-  ( ( V e. RR /\ j e. RR ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
262 200 229 261 syl2an 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
263 262 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
264 258 260 263 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V < j )
265 250 251 252 255 264 lelttrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 < j )
266 zgt0ge1 
 |-  ( j e. ZZ -> ( 0 < j <-> 1 <_ j ) )
267 239 266 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> ( 0 < j <-> 1 <_ j ) )
268 267 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( 0 < j <-> 1 <_ j ) )
269 265 268 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 1 <_ j )
270 elfzle2 
 |-  ( j e. ( 0 ... N ) -> j <_ N )
271 225 270 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j <_ N )
272 271 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j <_ N )
273 1z 
 |-  1 e. ZZ
274 elfz 
 |-  ( ( j e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
275 273 274 mp3an2 
 |-  ( ( j e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
276 239 21 275 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
277 276 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
278 269 272 277 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. ( 1 ... N ) )
279 elfzmlbm 
 |-  ( j e. ( 1 ... N ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
280 278 279 syl 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
281 249 280 ifclda 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) )
282 breq1 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> ( j < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
283 id 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> j = if ( j < V , j , ( j - 1 ) ) )
284 oveq1 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> ( j + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
285 282 283 284 ifbieq12d 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> if ( j < V , j , ( j + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
286 285 eqeq2d 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> ( j = if ( j < V , j , ( j + 1 ) ) <-> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) ) )
287 breq1 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
288 id 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) )
289 oveq1 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
290 287 288 289 ifbieq12d 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
291 290 eqeq2d 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( j = if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) <-> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) ) )
292 iftrue 
 |-  ( j < V -> if ( j < V , j , ( j + 1 ) ) = j )
293 292 eqcomd 
 |-  ( j < V -> j = if ( j < V , j , ( j + 1 ) ) )
294 293 adantl 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j = if ( j < V , j , ( j + 1 ) ) )
295 zlem1lt 
 |-  ( ( j e. ZZ /\ V e. ZZ ) -> ( j <_ V <-> ( j - 1 ) < V ) )
296 239 199 295 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V <-> ( j - 1 ) < V ) )
297 259 necomd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> V =/= j )
298 297 adantl 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> V =/= j )
299 ltlen 
 |-  ( ( j e. RR /\ V e. RR ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
300 229 200 299 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
301 300 biimprd 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j <_ V /\ V =/= j ) -> j < V ) )
302 298 301 mpan2d 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V -> j < V ) )
303 296 302 sylbird 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j - 1 ) < V -> j < V ) )
304 303 con3dimp 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> -. ( j - 1 ) < V )
305 304 iffalsed 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) = ( ( j - 1 ) + 1 ) )
306 226 nn0cnd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. CC )
307 npcan1 
 |-  ( j e. CC -> ( ( j - 1 ) + 1 ) = j )
308 306 307 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> ( ( j - 1 ) + 1 ) = j )
309 308 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( ( j - 1 ) + 1 ) = j )
310 305 309 eqtr2d 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j = if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) )
311 286 291 294 310 ifbothda 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
312 csbeq1a 
 |-  ( j = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
313 311 312 syl 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
314 313 eqeq2d 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
315 314 biimpd 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C -> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
316 breq1 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> ( y < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
317 id 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> y = if ( j < V , j , ( j - 1 ) ) )
318 oveq1 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> ( y + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
319 316 317 318 ifbieq12d 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> if ( y < V , y , ( y + 1 ) ) = if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) )
320 319 csbeq1d 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
321 320 eqeq2d 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> ( i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
322 321 rspcev 
 |-  ( ( if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) /\ i = [_ if ( if ( j < V , j , ( j - 1 ) ) < V , if ( j < V , j , ( j - 1 ) ) , ( if ( j < V , j , ( j - 1 ) ) + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
323 281 315 322 syl6an 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
324 323 ex 
 |-  ( ph -> ( j e. ( ( 0 ... N ) \ { V } ) -> ( i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) ) )
325 222 224 324 rexlimd 
 |-  ( ph -> ( E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C -> E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C ) )
326 221 325 impbid 
 |-  ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
327 187 326 bitr3d 
 |-  ( ph -> ( i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
328 327 ralbidv 
 |-  ( ph -> ( A. i e. ( 0 ... ( N - 1 ) ) i e. ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
329 132 328 syl5bb 
 |-  ( ph -> ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C ) )
330 329 anbi1d 
 |-  ( ph -> ( ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) |-> B ) /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) ) )
331 1 4 5 6 poimirlem23 
 |-  ( ph -> ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )
332 331 anbi2d 
 |-  ( ph -> ( ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) ) )
333 131 330 332 3bitrd 
 |-  ( ph -> ( E. x e. ( ( ( 0 ... K ) ^m ( 1 ... N ) ) ^m ( 0 ... ( N - 1 ) ) ) ( x = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) /\ ( ( 0 ... ( N - 1 ) ) C_ ran ( p e. ran x |-> B ) /\ E. p e. ran x ( p ` N ) =/= 0 ) ) <-> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { V } ) i = [_ <. T , U >. / s ]_ C /\ -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) ) )