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 elfzelz 
 |-  ( V e. ( 0 ... N ) -> V e. ZZ )
200 6 199 syl 
 |-  ( ph -> V e. ZZ )
201 200 zred 
 |-  ( ph -> V e. RR )
202 201 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V e. RR )
203 zre 
 |-  ( V e. ZZ -> V e. RR )
204 zre 
 |-  ( y e. ZZ -> y e. RR )
205 lenlt 
 |-  ( ( V e. RR /\ y e. RR ) -> ( V <_ y <-> -. y < V ) )
206 203 204 205 syl2an 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> -. y < V ) )
207 zleltp1 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( V <_ y <-> V < ( y + 1 ) ) )
208 206 207 bitr3d 
 |-  ( ( V e. ZZ /\ y e. ZZ ) -> ( -. y < V <-> V < ( y + 1 ) ) )
209 200 190 208 syl2an 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( -. y < V <-> V < ( y + 1 ) ) )
210 209 biimpa 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> V < ( y + 1 ) )
211 202 210 gtned 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) =/= V )
212 eldifsn 
 |-  ( ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) <-> ( ( y + 1 ) e. ( 0 ... N ) /\ ( y + 1 ) =/= V ) )
213 198 211 212 sylanbrc 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < V ) -> ( y + 1 ) e. ( ( 0 ... N ) \ { V } ) )
214 197 213 ifclda 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < V , y , ( y + 1 ) ) e. ( ( 0 ... N ) \ { V } ) )
215 nfcsb1v 
 |-  F/_ j [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
216 215 nfeq2 
 |-  F/ j i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
217 csbeq1a 
 |-  ( j = if ( y < V , y , ( y + 1 ) ) -> [_ <. T , U >. / s ]_ C = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C )
218 217 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 ) )
219 216 218 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 )
220 219 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 ) )
221 214 220 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 ) )
222 221 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 ) )
223 nfv 
 |-  F/ j ph
224 nfcv 
 |-  F/_ j ( 0 ... ( N - 1 ) )
225 224 216 nfrex 
 |-  F/ j E. y e. ( 0 ... ( N - 1 ) ) i = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ [_ <. T , U >. / s ]_ C
226 eldifi 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ( 0 ... N ) )
227 226 60 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. NN0 )
228 227 nn0ge0d 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> 0 <_ j )
229 228 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> 0 <_ j )
230 227 nn0red 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. RR )
231 230 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. RR )
232 201 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V e. RR )
233 21 zred 
 |-  ( ph -> N e. RR )
234 233 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> N e. RR )
235 simpr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < V )
236 elfzle2 
 |-  ( V e. ( 0 ... N ) -> V <_ N )
237 6 236 syl 
 |-  ( ph -> V <_ N )
238 237 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> V <_ N )
239 231 232 234 235 238 ltletrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j < N )
240 227 nn0zd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. ZZ )
241 zltlem1 
 |-  ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> j <_ ( N - 1 ) ) )
242 240 21 241 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < N <-> j <_ ( N - 1 ) ) )
243 242 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j < N <-> j <_ ( N - 1 ) ) )
244 239 243 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j <_ ( N - 1 ) )
245 0z 
 |-  0 e. ZZ
246 elfz 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
247 245 246 mp3an2 
 |-  ( ( j e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
248 240 23 247 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
249 248 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> ( j e. ( 0 ... ( N - 1 ) ) <-> ( 0 <_ j /\ j <_ ( N - 1 ) ) ) )
250 229 244 249 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j e. ( 0 ... ( N - 1 ) ) )
251 0red 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 e. RR )
252 201 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V e. RR )
253 230 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. RR )
254 elfzle1 
 |-  ( V e. ( 0 ... N ) -> 0 <_ V )
255 6 254 syl 
 |-  ( ph -> 0 <_ V )
256 255 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 <_ V )
257 lenlt 
 |-  ( ( V e. RR /\ j e. RR ) -> ( V <_ j <-> -. j < V ) )
258 201 230 257 syl2an 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V <_ j <-> -. j < V ) )
259 258 biimpar 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V <_ j )
260 eldifsni 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j =/= V )
261 260 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j =/= V )
262 ltlen 
 |-  ( ( V e. RR /\ j e. RR ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
263 201 230 262 syl2an 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
264 263 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( V < j <-> ( V <_ j /\ j =/= V ) ) )
265 259 261 264 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> V < j )
266 251 252 253 256 265 lelttrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 0 < j )
267 zgt0ge1 
 |-  ( j e. ZZ -> ( 0 < j <-> 1 <_ j ) )
268 240 267 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> ( 0 < j <-> 1 <_ j ) )
269 268 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( 0 < j <-> 1 <_ j ) )
270 266 269 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> 1 <_ j )
271 elfzle2 
 |-  ( j e. ( 0 ... N ) -> j <_ N )
272 226 271 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j <_ N )
273 272 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j <_ N )
274 1z 
 |-  1 e. ZZ
275 elfz 
 |-  ( ( j e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
276 274 275 mp3an2 
 |-  ( ( j e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
277 240 21 276 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
278 277 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
279 270 273 278 mpbir2and 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j e. ( 1 ... N ) )
280 elfzmlbm 
 |-  ( j e. ( 1 ... N ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
281 279 280 syl 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) )
282 250 281 ifclda 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> if ( j < V , j , ( j - 1 ) ) e. ( 0 ... ( N - 1 ) ) )
283 breq1 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> ( j < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
284 id 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> j = if ( j < V , j , ( j - 1 ) ) )
285 oveq1 
 |-  ( j = if ( j < V , j , ( j - 1 ) ) -> ( j + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
286 283 284 285 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 ) ) )
287 286 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 ) ) ) )
288 breq1 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
289 id 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) )
290 oveq1 
 |-  ( ( j - 1 ) = if ( j < V , j , ( j - 1 ) ) -> ( ( j - 1 ) + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
291 288 289 290 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 ) ) )
292 291 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 ) ) ) )
293 iftrue 
 |-  ( j < V -> if ( j < V , j , ( j + 1 ) ) = j )
294 293 eqcomd 
 |-  ( j < V -> j = if ( j < V , j , ( j + 1 ) ) )
295 294 adantl 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ j < V ) -> j = if ( j < V , j , ( j + 1 ) ) )
296 zlem1lt 
 |-  ( ( j e. ZZ /\ V e. ZZ ) -> ( j <_ V <-> ( j - 1 ) < V ) )
297 240 200 296 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V <-> ( j - 1 ) < V ) )
298 260 necomd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> V =/= j )
299 298 adantl 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> V =/= j )
300 ltlen 
 |-  ( ( j e. RR /\ V e. RR ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
301 230 201 300 syl2anr 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j < V <-> ( j <_ V /\ V =/= j ) ) )
302 301 biimprd 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j <_ V /\ V =/= j ) -> j < V ) )
303 299 302 mpan2d 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( j <_ V -> j < V ) )
304 297 303 sylbird 
 |-  ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) -> ( ( j - 1 ) < V -> j < V ) )
305 304 con3dimp 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> -. ( j - 1 ) < V )
306 305 iffalsed 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) = ( ( j - 1 ) + 1 ) )
307 227 nn0cnd 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> j e. CC )
308 npcan1 
 |-  ( j e. CC -> ( ( j - 1 ) + 1 ) = j )
309 307 308 syl 
 |-  ( j e. ( ( 0 ... N ) \ { V } ) -> ( ( j - 1 ) + 1 ) = j )
310 309 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> ( ( j - 1 ) + 1 ) = j )
311 306 310 eqtr2d 
 |-  ( ( ( ph /\ j e. ( ( 0 ... N ) \ { V } ) ) /\ -. j < V ) -> j = if ( ( j - 1 ) < V , ( j - 1 ) , ( ( j - 1 ) + 1 ) ) )
312 287 292 295 311 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 ) ) )
313 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 )
314 312 313 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 )
315 314 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 ) )
316 315 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 ) )
317 breq1 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> ( y < V <-> if ( j < V , j , ( j - 1 ) ) < V ) )
318 id 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> y = if ( j < V , j , ( j - 1 ) ) )
319 oveq1 
 |-  ( y = if ( j < V , j , ( j - 1 ) ) -> ( y + 1 ) = ( if ( j < V , j , ( j - 1 ) ) + 1 ) )
320 317 318 319 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 ) ) )
321 320 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 )
322 321 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 ) )
323 322 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 )
324 282 316 323 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 ) )
325 324 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 ) ) )
326 223 225 325 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 ) )
327 222 326 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 ) )
328 187 327 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 ) )
329 328 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 ) )
330 132 329 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 ) )
331 330 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 ) ) )
332 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 ) ) ) )
333 332 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 ) ) ) ) )
334 131 331 333 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 ) ) ) ) )