Metamath Proof Explorer

Theorem poimirlem10

Description: Lemma for poimir establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem22.s 
|- S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
poimirlem22.1 
|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
poimirlem12.2 
|- ( ph -> T e. S )
poimirlem11.3 
|- ( ph -> ( 2nd ` T ) = 0 )
Assertion poimirlem10 
|- ( ph -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` T ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem22.s 
 |-  S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
3 poimirlem22.1 
 |-  ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
4 poimirlem12.2 
 |-  ( ph -> T e. S )
5 poimirlem11.3 
 |-  ( ph -> ( 2nd ` T ) = 0 )
6 ovexd 
 |-  ( ph -> ( 1 ... N ) e. _V )
7 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
8 1 7 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
9 nn0fz0 
 |-  ( ( N - 1 ) e. NN0 <-> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
10 8 9 sylib 
 |-  ( ph -> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
11 3 10 ffvelrnd 
 |-  ( ph -> ( F ` ( N - 1 ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) )
12 elmapfn 
 |-  ( ( F ` ( N - 1 ) ) e. ( ( 0 ... K ) ^m ( 1 ... N ) ) -> ( F ` ( N - 1 ) ) Fn ( 1 ... N ) )
13 11 12 syl 
 |-  ( ph -> ( F ` ( N - 1 ) ) Fn ( 1 ... N ) )
14 1ex 
 |-  1 e. _V
15 fnconstg 
 |-  ( 1 e. _V -> ( ( 1 ... N ) X. { 1 } ) Fn ( 1 ... N ) )
16 14 15 mp1i 
 |-  ( ph -> ( ( 1 ... N ) X. { 1 } ) Fn ( 1 ... N ) )
17 elrabi 
 |-  ( T e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
18 17 2 eleq2s 
 |-  ( T e. S -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
19 4 18 syl 
 |-  ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
20 xp1st 
 |-  ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
21 19 20 syl 
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
22 xp1st 
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
23 21 22 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
24 elmapfn 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
25 23 24 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
26 fveq2 
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
27 26 breq2d 
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
28 27 ifbid 
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
29 28 csbeq1d 
 |-  ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
30 2fveq3 
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
31 2fveq3 
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
32 31 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
33 32 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
34 31 imaeq1d 
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
35 34 xpeq1d 
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
36 33 35 uneq12d 
 |-  ( t = T -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
37 30 36 oveq12d 
 |-  ( t = T -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
38 37 csbeq2dv 
 |-  ( t = T -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
39 29 38 eqtrd 
 |-  ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
40 39 mpteq2dv 
 |-  ( t = T -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
41 40 eqeq2d 
 |-  ( t = T -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
42 41 2 elrab2 
 |-  ( T e. S <-> ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
43 42 simprbi 
 |-  ( T e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
44 4 43 syl 
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
45 breq12 
 |-  ( ( y = ( N - 1 ) /\ ( 2nd ` T ) = 0 ) -> ( y < ( 2nd ` T ) <-> ( N - 1 ) < 0 ) )
46 5 45 sylan2 
 |-  ( ( y = ( N - 1 ) /\ ph ) -> ( y < ( 2nd ` T ) <-> ( N - 1 ) < 0 ) )
47 46 ancoms 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> ( y < ( 2nd ` T ) <-> ( N - 1 ) < 0 ) )
48 oveq1 
 |-  ( y = ( N - 1 ) -> ( y + 1 ) = ( ( N - 1 ) + 1 ) )
49 1 nncnd 
 |-  ( ph -> N e. CC )
50 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
51 49 50 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
52 48 51 sylan9eqr 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> ( y + 1 ) = N )
53 47 52 ifbieq2d 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = if ( ( N - 1 ) < 0 , y , N ) )
54 8 nn0ge0d 
 |-  ( ph -> 0 <_ ( N - 1 ) )
55 0red 
 |-  ( ph -> 0 e. RR )
56 8 nn0red 
 |-  ( ph -> ( N - 1 ) e. RR )
57 55 56 lenltd 
 |-  ( ph -> ( 0 <_ ( N - 1 ) <-> -. ( N - 1 ) < 0 ) )
58 54 57 mpbid 
 |-  ( ph -> -. ( N - 1 ) < 0 )
59 58 iffalsed 
 |-  ( ph -> if ( ( N - 1 ) < 0 , y , N ) = N )
60 59 adantr 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> if ( ( N - 1 ) < 0 , y , N ) = N )
61 53 60 eqtrd 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = N )
62 61 csbeq1d 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ N / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
63 oveq2 
 |-  ( j = N -> ( 1 ... j ) = ( 1 ... N ) )
64 63 imaeq2d 
 |-  ( j = N -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) )
65 xp2nd 
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
66 21 65 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
67 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
68 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
69 67 68 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
70 66 69 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
71 f1ofo 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
72 foima 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
73 70 71 72 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
74 64 73 sylan9eqr 
 |-  ( ( ph /\ j = N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( 1 ... N ) )
75 74 xpeq1d 
 |-  ( ( ph /\ j = N ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( 1 ... N ) X. { 1 } ) )
76 oveq1 
 |-  ( j = N -> ( j + 1 ) = ( N + 1 ) )
77 76 oveq1d 
 |-  ( j = N -> ( ( j + 1 ) ... N ) = ( ( N + 1 ) ... N ) )
78 1 nnred 
 |-  ( ph -> N e. RR )
79 78 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
80 1 nnzd 
 |-  ( ph -> N e. ZZ )
81 80 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
82 fzn 
 |-  ( ( ( N + 1 ) e. ZZ /\ N e. ZZ ) -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
83 81 80 82 syl2anc 
 |-  ( ph -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
84 79 83 mpbid 
 |-  ( ph -> ( ( N + 1 ) ... N ) = (/) )
85 77 84 sylan9eqr 
 |-  ( ( ph /\ j = N ) -> ( ( j + 1 ) ... N ) = (/) )
86 85 imaeq2d 
 |-  ( ( ph /\ j = N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
87 86 xpeq1d 
 |-  ( ( ph /\ j = N ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " (/) ) X. { 0 } ) )
88 ima0 
 |-  ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
89 88 xpeq1i 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " (/) ) X. { 0 } ) = ( (/) X. { 0 } )
90 0xp 
 |-  ( (/) X. { 0 } ) = (/)
91 89 90 eqtri 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " (/) ) X. { 0 } ) = (/)
92 87 91 eqtrdi 
 |-  ( ( ph /\ j = N ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = (/) )
93 75 92 uneq12d 
 |-  ( ( ph /\ j = N ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( 1 ... N ) X. { 1 } ) u. (/) ) )
94 un0 
 |-  ( ( ( 1 ... N ) X. { 1 } ) u. (/) ) = ( ( 1 ... N ) X. { 1 } )
95 93 94 eqtrdi 
 |-  ( ( ph /\ j = N ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( 1 ... N ) X. { 1 } ) )
96 95 oveq2d 
 |-  ( ( ph /\ j = N ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) )
97 1 96 csbied 
 |-  ( ph -> [_ N / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) )
98 97 adantr 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> [_ N / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) )
99 62 98 eqtrd 
 |-  ( ( ph /\ y = ( N - 1 ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) )
100 ovexd 
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) e. _V )
101 44 99 10 100 fvmptd 
 |-  ( ph -> ( F ` ( N - 1 ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) )
102 101 fveq1d 
 |-  ( ph -> ( ( F ` ( N - 1 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) ` n ) )
103 102 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( F ` ( N - 1 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) ` n ) )
104 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
105 eqidd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
106 14 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 1 } ) ` n ) = 1 )
107 106 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { 1 } ) ` n ) = 1 )
108 25 16 6 6 104 105 107 ofval 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( 1 ... N ) X. { 1 } ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) )
109 103 108 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( F ` ( N - 1 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) )
110 elmapi 
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
111 23 110 syl 
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
112 111 ffvelrnda 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) )
113 elfzonn0 
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
114 112 113 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
115 114 nn0cnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC )
116 pncan1 
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) - 1 ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
117 115 116 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) - 1 ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
118 6 13 16 25 109 107 117 offveq 
 |-  ( ph -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` T ) ) )