Metamath Proof Explorer

Theorem dvnprodlem1

Description: D is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnprodlem1.c 
|- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
dvnprodlem1.j 
|- ( ph -> J e. NN0 )
dvnprodlem1.d 
|- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
dvnprodlem1.t 
|- ( ph -> T e. Fin )
dvnprodlem1.z 
|- ( ph -> Z e. T )
dvnprodlem1.zr 
|- ( ph -> -. Z e. R )
dvnprodlem1.rzt 
|- ( ph -> ( R u. { Z } ) C_ T )
Assertion dvnprodlem1 
|- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )

Proof

Step Hyp Ref Expression
1 dvnprodlem1.c 
 |-  C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
2 dvnprodlem1.j 
 |-  ( ph -> J e. NN0 )
3 dvnprodlem1.d 
 |-  D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
4 dvnprodlem1.t 
 |-  ( ph -> T e. Fin )
5 dvnprodlem1.z 
 |-  ( ph -> Z e. T )
6 dvnprodlem1.zr 
 |-  ( ph -> -. Z e. R )
7 dvnprodlem1.rzt 
 |-  ( ph -> ( R u. { Z } ) C_ T )
8 eqidd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
9 0zd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 e. ZZ )
10 2 nn0zd 
 |-  ( ph -> J e. ZZ )
11 10 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. ZZ )
12 oveq2 
 |-  ( s = ( R u. { Z } ) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) )
13 rabeq 
 |-  ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } )
14 12 13 syl 
 |-  ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } )
15 sumeq1 
 |-  ( s = ( R u. { Z } ) -> sum_ t e. s ( c ` t ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
16 15 eqeq1d 
 |-  ( s = ( R u. { Z } ) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = n ) )
17 16 rabbidv 
 |-  ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
18 14 17 eqtrd 
 |-  ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
19 18 mpteq2dv 
 |-  ( s = ( R u. { Z } ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) )
20 ssexg 
 |-  ( ( ( R u. { Z } ) C_ T /\ T e. Fin ) -> ( R u. { Z } ) e. _V )
21 7 4 20 syl2anc 
 |-  ( ph -> ( R u. { Z } ) e. _V )
22 elpwg 
 |-  ( ( R u. { Z } ) e. _V -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
23 21 22 syl 
 |-  ( ph -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
24 7 23 mpbird 
 |-  ( ph -> ( R u. { Z } ) e. ~P T )
25 nn0ex 
 |-  NN0 e. _V
26 25 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V
27 26 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V )
28 1 19 24 27 fvmptd3 
 |-  ( ph -> ( C ` ( R u. { Z } ) ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) )
29 oveq2 
 |-  ( n = J -> ( 0 ... n ) = ( 0 ... J ) )
30 29 oveq1d 
 |-  ( n = J -> ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
31 rabeq 
 |-  ( ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
32 30 31 syl 
 |-  ( n = J -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
33 eqeq2 
 |-  ( n = J -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
34 33 rabbidv 
 |-  ( n = J -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
35 32 34 eqtrd 
 |-  ( n = J -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
36 35 adantl 
 |-  ( ( ph /\ n = J ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
37 ovex 
 |-  ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. _V
38 37 rabex 
 |-  { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V
39 38 a1i 
 |-  ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V )
40 28 36 2 39 fvmptd 
 |-  ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
41 ssrab2 
 |-  { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } C_ ( ( 0 ... J ) ^m ( R u. { Z } ) )
42 41 a1i 
 |-  ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
43 40 42 eqsstrd 
 |-  ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
44 43 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
45 simpr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
46 44 45 sseldd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
47 elmapi 
 |-  ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
48 46 47 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
49 snidg 
 |-  ( Z e. T -> Z e. { Z } )
50 5 49 syl 
 |-  ( ph -> Z e. { Z } )
51 elun2 
 |-  ( Z e. { Z } -> Z e. ( R u. { Z } ) )
52 50 51 syl 
 |-  ( ph -> Z e. ( R u. { Z } ) )
53 52 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
54 48 53 ffvelrnd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... J ) )
55 54 elfzelzd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ZZ )
56 11 55 zsubcld 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ZZ )
57 elfzle2 
 |-  ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) <_ J )
58 54 57 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) <_ J )
59 11 zred 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. RR )
60 55 zred 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. RR )
61 59 60 subge0d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( J - ( c ` Z ) ) <-> ( c ` Z ) <_ J ) )
62 58 61 mpbird 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( J - ( c ` Z ) ) )
63 elfzle1 
 |-  ( ( c ` Z ) e. ( 0 ... J ) -> 0 <_ ( c ` Z ) )
64 54 63 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( c ` Z ) )
65 59 60 subge02d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( c ` Z ) <-> ( J - ( c ` Z ) ) <_ J ) )
66 64 65 mpbid 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) <_ J )
67 9 11 56 62 66 elfzd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
68 elmapfn 
 |-  ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c Fn ( R u. { Z } ) )
69 46 68 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c Fn ( R u. { Z } ) )
70 ssun1 
 |-  R C_ ( R u. { Z } )
71 70 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R C_ ( R u. { Z } ) )
72 fnssres 
 |-  ( ( c Fn ( R u. { Z } ) /\ R C_ ( R u. { Z } ) ) -> ( c |` R ) Fn R )
73 69 71 72 syl2anc 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) Fn R )
74 nfv 
 |-  F/ t ph
75 nfcv 
 |-  F/_ t c
76 nfcv 
 |-  F/_ t ~P T
77 nfcv 
 |-  F/_ t NN0
78 nfcv 
 |-  F/_ t s
79 78 nfsum1 
 |-  F/_ t sum_ t e. s ( c ` t )
80 nfcv 
 |-  F/_ t n
81 79 80 nfeq 
 |-  F/ t sum_ t e. s ( c ` t ) = n
82 nfcv 
 |-  F/_ t ( ( 0 ... n ) ^m s )
83 81 82 nfrabw 
 |-  F/_ t { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n }
84 77 83 nfmpt 
 |-  F/_ t ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } )
85 76 84 nfmpt 
 |-  F/_ t ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
86 1 85 nfcxfr 
 |-  F/_ t C
87 nfcv 
 |-  F/_ t ( R u. { Z } )
88 86 87 nffv 
 |-  F/_ t ( C ` ( R u. { Z } ) )
89 nfcv 
 |-  F/_ t J
90 88 89 nffv 
 |-  F/_ t ( ( C ` ( R u. { Z } ) ) ` J )
91 75 90 nfel 
 |-  F/ t c e. ( ( C ` ( R u. { Z } ) ) ` J )
92 74 91 nfan 
 |-  F/ t ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
93 fvres 
 |-  ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) )
94 93 adantl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( c ` t ) )
95 9 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 e. ZZ )
96 56 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( J - ( c ` Z ) ) e. ZZ )
97 48 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
98 71 sselda 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. ( R u. { Z } ) )
99 97 98 ffvelrnd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... J ) )
100 99 elfzelzd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ZZ )
101 elfzle1 
 |-  ( ( c ` t ) e. ( 0 ... J ) -> 0 <_ ( c ` t ) )
102 99 101 syl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 <_ ( c ` t ) )
103 7 unssad 
 |-  ( ph -> R C_ T )
104 ssfi 
 |-  ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
105 4 103 104 syl2anc 
 |-  ( ph -> R e. Fin )
106 105 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> R e. Fin )
107 fzssz 
 |-  ( 0 ... J ) C_ ZZ
108 zssre 
 |-  ZZ C_ RR
109 107 108 sstri 
 |-  ( 0 ... J ) C_ RR
110 109 a1i 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( 0 ... J ) C_ RR )
111 48 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
112 71 sselda 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> r e. ( R u. { Z } ) )
113 111 112 ffvelrnd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. ( 0 ... J ) )
114 110 113 sseldd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. RR )
115 114 adantlr 
 |-  ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> ( c ` r ) e. RR )
116 elfzle1 
 |-  ( ( c ` r ) e. ( 0 ... J ) -> 0 <_ ( c ` r ) )
117 113 116 syl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> 0 <_ ( c ` r ) )
118 117 adantlr 
 |-  ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> 0 <_ ( c ` r ) )
119 fveq2 
 |-  ( r = t -> ( c ` r ) = ( c ` t ) )
120 simpr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. R )
121 106 115 118 119 120 fsumge1 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ sum_ r e. R ( c ` r ) )
122 105 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
123 114 recnd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. CC )
124 122 123 fsumcl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) e. CC )
125 60 recnd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. CC )
126 124 125 pncand 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) - ( c ` Z ) ) = sum_ r e. R ( c ` r ) )
127 nfv 
 |-  F/ r ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
128 nfcv 
 |-  F/_ r ( c ` Z )
129 5 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
130 6 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
131 fveq2 
 |-  ( r = Z -> ( c ` r ) = ( c ` Z ) )
132 127 128 122 129 130 123 131 125 fsumsplitsn 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) )
133 132 eqcomd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = sum_ r e. ( R u. { Z } ) ( c ` r ) )
134 119 cbvsumv 
 |-  sum_ r e. ( R u. { Z } ) ( c ` r ) = sum_ t e. ( R u. { Z } ) ( c ` t )
135 134 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
136 40 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
137 45 136 eleqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
138 rabid 
 |-  ( c e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } <-> ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
139 137 138 sylib 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
140 139 simprd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = J )
141 135 140 eqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = J )
142 133 141 eqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = J )
143 142 oveq1d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) - ( c ` Z ) ) = ( J - ( c ` Z ) ) )
144 126 143 eqtr3d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
145 144 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
146 121 145 breqtrd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ ( J - ( c ` Z ) ) )
147 95 96 100 102 146 elfzd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
148 94 147 eqeltrd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
149 148 ex 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
150 92 149 ralrimi 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
151 73 150 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
152 ffnfv 
 |-  ( ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) <-> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
153 151 152 sylibr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) )
154 ovexd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... ( J - ( c ` Z ) ) ) e. _V )
155 4 103 ssexd 
 |-  ( ph -> R e. _V )
156 155 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. _V )
157 154 156 elmapd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) <-> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) ) )
158 153 157 mpbird 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
159 93 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) ) )
160 92 159 ralrimi 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) = ( c ` t ) )
161 160 sumeq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = sum_ t e. R ( c ` t ) )
162 119 cbvsumv 
 |-  sum_ r e. R ( c ` r ) = sum_ t e. R ( c ` t )
163 162 eqcomi 
 |-  sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r )
164 163 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r ) )
165 144 idi 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
166 161 164 165 3eqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) )
167 158 166 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) /\ sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
168 eqidd 
 |-  ( e = ( c |` R ) -> R = R )
169 simpl 
 |-  ( ( e = ( c |` R ) /\ t e. R ) -> e = ( c |` R ) )
170 169 fveq1d 
 |-  ( ( e = ( c |` R ) /\ t e. R ) -> ( e ` t ) = ( ( c |` R ) ` t ) )
171 168 170 sumeq12rdv 
 |-  ( e = ( c |` R ) -> sum_ t e. R ( e ` t ) = sum_ t e. R ( ( c |` R ) ` t ) )
172 171 eqeq1d 
 |-  ( e = ( c |` R ) -> ( sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) <-> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
173 172 elrab 
 |-  ( ( c |` R ) e. { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } <-> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) /\ sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
174 167 173 sylibr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
175 oveq2 
 |-  ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
176 rabeq 
 |-  ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
177 175 176 syl 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
178 sumeq1 
 |-  ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
179 178 eqeq1d 
 |-  ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
180 179 rabbidv 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
181 177 180 eqtrd 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
182 181 mpteq2dv 
 |-  ( s = R -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
183 elpwg 
 |-  ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
184 155 183 syl 
 |-  ( ph -> ( R e. ~P T <-> R C_ T ) )
185 103 184 mpbird 
 |-  ( ph -> R e. ~P T )
186 25 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
187 186 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
188 1 182 185 187 fvmptd3 
 |-  ( ph -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
189 188 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
190 oveq2 
 |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
191 190 oveq1d 
 |-  ( n = m -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) )
192 rabeq 
 |-  ( ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
193 191 192 syl 
 |-  ( n = m -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
194 eqeq2 
 |-  ( n = m -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = m ) )
195 194 rabbidv 
 |-  ( n = m -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
196 193 195 eqtrd 
 |-  ( n = m -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
197 196 cbvmptv 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) = ( m e. NN0 |-> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
198 197 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) = ( m e. NN0 |-> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } ) )
199 189 198 eqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( C ` R ) = ( m e. NN0 |-> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } ) )
200 fveq1 
 |-  ( c = e -> ( c ` t ) = ( e ` t ) )
201 200 sumeq2sdv 
 |-  ( c = e -> sum_ t e. R ( c ` t ) = sum_ t e. R ( e ` t ) )
202 201 eqeq1d 
 |-  ( c = e -> ( sum_ t e. R ( c ` t ) = m <-> sum_ t e. R ( e ` t ) = m ) )
203 202 cbvrabv 
 |-  { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m }
204 203 a1i 
 |-  ( m = ( J - ( c ` Z ) ) -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m } )
205 oveq2 
 |-  ( m = ( J - ( c ` Z ) ) -> ( 0 ... m ) = ( 0 ... ( J - ( c ` Z ) ) ) )
206 205 oveq1d 
 |-  ( m = ( J - ( c ` Z ) ) -> ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
207 rabeq 
 |-  ( ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) -> { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } )
208 206 207 syl 
 |-  ( m = ( J - ( c ` Z ) ) -> { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } )
209 eqeq2 
 |-  ( m = ( J - ( c ` Z ) ) -> ( sum_ t e. R ( e ` t ) = m <-> sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) ) )
210 209 rabbidv 
 |-  ( m = ( J - ( c ` Z ) ) -> { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
211 204 208 210 3eqtrd 
 |-  ( m = ( J - ( c ` Z ) ) -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
212 211 adantl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ m = ( J - ( c ` Z ) ) ) -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
213 56 62 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
214 elnn0z 
 |-  ( ( J - ( c ` Z ) ) e. NN0 <-> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
215 213 214 sylibr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. NN0 )
216 ovex 
 |-  ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) e. _V
217 216 rabex 
 |-  { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } e. _V
218 217 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } e. _V )
219 199 212 215 218 fvmptd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` R ) ` ( J - ( c ` Z ) ) ) = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
220 219 eqcomd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
221 174 220 eleqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
222 67 221 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
223 8 222 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) )
224 ovexd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. _V )
225 vex 
 |-  c e. _V
226 225 resex 
 |-  ( c |` R ) e. _V
227 226 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. _V )
228 opeq12 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> <. k , d >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
229 228 eqeq2d 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. <-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
230 eleq1 
 |-  ( k = ( J - ( c ` Z ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
231 230 adantr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
232 simpr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> d = ( c |` R ) )
233 fveq2 
 |-  ( k = ( J - ( c ` Z ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
234 233 adantr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
235 232 234 eleq12d 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( d e. ( ( C ` R ) ` k ) <-> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
236 231 235 anbi12d 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) <-> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) )
237 229 236 anbi12d 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) <-> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) ) )
238 237 spc2egv 
 |-  ( ( ( J - ( c ` Z ) ) e. _V /\ ( c |` R ) e. _V ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) -> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) ) )
239 224 227 238 syl2anc 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) -> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) ) )
240 223 239 mpd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) )
241 eliunxp 
 |-  ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) )
242 240 241 sylibr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
243 242 3 fmptd 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
244 90 nfcri 
 |-  F/ t e e. ( ( C ` ( R u. { Z } ) ) ` J )
245 91 244 nfan 
 |-  F/ t ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
246 74 245 nfan 
 |-  F/ t ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
247 nfv 
 |-  F/ t ( D ` c ) = ( D ` e )
248 246 247 nfan 
 |-  F/ t ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) )
249 94 eqcomd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
250 249 adantlrr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
251 250 adantlr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
252 3 a1i 
 |-  ( ph -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
253 opex 
 |-  <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V
254 253 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V )
255 252 254 fvmpt2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
256 255 fveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
257 256 fveq1d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) )
258 ovex 
 |-  ( J - ( c ` Z ) ) e. _V
259 258 226 op2nd 
 |-  ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( c |` R )
260 259 fveq1i 
 |-  ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t )
261 260 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t ) )
262 257 261 eqtr2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
263 262 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
264 263 ad2antrr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
265 simpr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = ( D ` e ) )
266 fveq1 
 |-  ( c = e -> ( c ` Z ) = ( e ` Z ) )
267 266 oveq2d 
 |-  ( c = e -> ( J - ( c ` Z ) ) = ( J - ( e ` Z ) ) )
268 reseq1 
 |-  ( c = e -> ( c |` R ) = ( e |` R ) )
269 267 268 opeq12d 
 |-  ( c = e -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
270 simpr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
271 opex 
 |-  <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V
272 271 a1i 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V )
273 3 269 270 272 fvmptd3 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
274 273 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
275 265 274 eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
276 275 fveq2d 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
277 276 adantlrl 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
278 277 adantr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
279 ovex 
 |-  ( J - ( e ` Z ) ) e. _V
280 vex 
 |-  e e. _V
281 280 resex 
 |-  ( e |` R ) e. _V
282 279 281 op2nd 
 |-  ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( e |` R )
283 282 a1i 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( e |` R ) )
284 278 283 eqtrd 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( 2nd ` ( D ` c ) ) = ( e |` R ) )
285 284 fveq1d 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( e |` R ) ` t ) )
286 fvres 
 |-  ( t e. R -> ( ( e |` R ) ` t ) = ( e ` t ) )
287 286 adantl 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( e |` R ) ` t ) = ( e ` t ) )
288 285 287 eqtrd 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( e ` t ) )
289 251 264 288 3eqtrd 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( c ` t ) = ( e ` t ) )
290 289 adantlr 
 |-  ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( c ` t ) = ( e ` t ) )
291 simpl 
 |-  ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) )
292 elunnel1 
 |-  ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t e. { Z } )
293 elsni 
 |-  ( t e. { Z } -> t = Z )
294 292 293 syl 
 |-  ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t = Z )
295 294 adantll 
 |-  ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> t = Z )
296 simpr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> t = Z )
297 296 fveq2d 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> ( c ` t ) = ( c ` Z ) )
298 2 nn0cnd 
 |-  ( ph -> J e. CC )
299 298 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
300 299 125 nncand 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( c ` Z ) )
301 300 eqcomd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
302 301 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
303 302 adantr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
304 255 fveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
305 258 226 op1st 
 |-  ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) )
306 305 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) ) )
307 304 306 eqtr2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) = ( 1st ` ( D ` c ) ) )
308 307 oveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
309 308 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
310 309 adantr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
311 fveq2 
 |-  ( ( D ` c ) = ( D ` e ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
312 311 adantl 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
313 273 fveq2d 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
314 313 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
315 279 281 op1st 
 |-  ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) )
316 315 a1i 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) ) )
317 312 314 316 3eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( J - ( e ` Z ) ) )
318 317 oveq2d 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( J - ( J - ( e ` Z ) ) ) )
319 298 adantr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
320 zsscn 
 |-  ZZ C_ CC
321 107 320 sstri 
 |-  ( 0 ... J ) C_ CC
322 321 a1i 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... J ) C_ CC )
323 eleq1w 
 |-  ( c = e -> ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) <-> e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
324 323 anbi2d 
 |-  ( c = e -> ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) <-> ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) )
325 feq1 
 |-  ( c = e -> ( c : ( R u. { Z } ) --> ( 0 ... J ) <-> e : ( R u. { Z } ) --> ( 0 ... J ) ) )
326 324 325 imbi12d 
 |-  ( c = e -> ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) ) <-> ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) ) ) )
327 326 48 chvarvv 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) )
328 52 adantr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
329 327 328 ffvelrnd 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. ( 0 ... J ) )
330 322 329 sseldd 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. CC )
331 319 330 nncand 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
332 331 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
333 eqidd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( e ` Z ) = ( e ` Z ) )
334 318 332 333 3eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
335 334 adantlrl 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
336 303 310 335 3eqtrd 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c ` Z ) = ( e ` Z ) )
337 336 adantr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> ( c ` Z ) = ( e ` Z ) )
338 fveq2 
 |-  ( t = Z -> ( e ` t ) = ( e ` Z ) )
339 338 eqcomd 
 |-  ( t = Z -> ( e ` Z ) = ( e ` t ) )
340 339 adantl 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> ( e ` Z ) = ( e ` t ) )
341 297 337 340 3eqtrd 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> ( c ` t ) = ( e ` t ) )
342 341 adantlr 
 |-  ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ t = Z ) -> ( c ` t ) = ( e ` t ) )
343 291 295 342 syl2anc 
 |-  ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( c ` t ) = ( e ` t ) )
344 290 343 pm2.61dan 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) -> ( c ` t ) = ( e ` t ) )
345 344 ex 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( t e. ( R u. { Z } ) -> ( c ` t ) = ( e ` t ) ) )
346 248 345 ralrimi 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> A. t e. ( R u. { Z } ) ( c ` t ) = ( e ` t ) )
347 69 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> c Fn ( R u. { Z } ) )
348 347 adantr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> c Fn ( R u. { Z } ) )
349 327 ffnd 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e Fn ( R u. { Z } ) )
350 349 adantrl 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> e Fn ( R u. { Z } ) )
351 350 adantr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> e Fn ( R u. { Z } ) )
352 eqfnfv 
 |-  ( ( c Fn ( R u. { Z } ) /\ e Fn ( R u. { Z } ) ) -> ( c = e <-> A. t e. ( R u. { Z } ) ( c ` t ) = ( e ` t ) ) )
353 348 351 352 syl2anc 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c = e <-> A. t e. ( R u. { Z } ) ( c ` t ) = ( e ` t ) ) )
354 346 353 mpbird 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> c = e )
355 354 ex 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( D ` c ) = ( D ` e ) -> c = e ) )
356 355 ralrimivva 
 |-  ( ph -> A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) )
357 243 356 jca 
 |-  ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) ) )
358 dff13 
 |-  ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) ) )
359 357 358 sylibr 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
360 eliun 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
361 360 biimpi 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
362 361 adantl 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
363 nfv 
 |-  F/ k ph
364 nfcv 
 |-  F/_ k p
365 nfiu1 
 |-  F/_ k U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
366 364 365 nfel 
 |-  F/ k p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
367 363 366 nfan 
 |-  F/ k ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
368 nfv 
 |-  F/ k ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J }
369 nfv 
 |-  F/ t k e. ( 0 ... J )
370 nfcv 
 |-  F/_ t p
371 nfcv 
 |-  F/_ t { k }
372 nfcv 
 |-  F/_ t R
373 86 372 nffv 
 |-  F/_ t ( C ` R )
374 nfcv 
 |-  F/_ t k
375 373 374 nffv 
 |-  F/_ t ( ( C ` R ) ` k )
376 371 375 nfxp 
 |-  F/_ t ( { k } X. ( ( C ` R ) ` k ) )
377 370 376 nfel 
 |-  F/ t p e. ( { k } X. ( ( C ` R ) ` k ) )
378 74 369 377 nf3an 
 |-  F/ t ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) )
379 0zd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> 0 e. ZZ )
380 10 adantr 
 |-  ( ( ph /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
381 380 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
382 iftrue 
 |-  ( t e. R -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
383 382 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
384 simp1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ph )
385 simp2 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
386 xp2nd 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
387 386 3ad2ant3 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
388 188 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
389 oveq2 
 |-  ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
390 389 oveq1d 
 |-  ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
391 rabeq 
 |-  ( ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
392 390 391 syl 
 |-  ( n = k -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
393 eqeq2 
 |-  ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
394 393 rabbidv 
 |-  ( n = k -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
395 392 394 eqtrd 
 |-  ( n = k -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
396 395 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ n = k ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
397 elfznn0 
 |-  ( k e. ( 0 ... J ) -> k e. NN0 )
398 397 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
399 ovex 
 |-  ( ( 0 ... k ) ^m R ) e. _V
400 399 rabex 
 |-  { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V
401 400 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
402 388 396 398 401 fvmptd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
403 402 3adant3 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
404 387 403 eleqtrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
405 elrabi 
 |-  ( ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
406 405 3ad2ant3 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
407 384 385 404 406 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
408 elmapi 
 |-  ( ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
409 407 408 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
410 409 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
411 410 ffvelrnda 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) )
412 411 elfzelzd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
413 383 412 eqeltrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ )
414 simpl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) )
415 294 adantll 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> t = Z )
416 simpr 
 |-  ( ( ph /\ t = Z ) -> t = Z )
417 6 adantr 
 |-  ( ( ph /\ t = Z ) -> -. Z e. R )
418 416 417 eqneltrd 
 |-  ( ( ph /\ t = Z ) -> -. t e. R )
419 418 iffalsed 
 |-  ( ( ph /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
420 419 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
421 10 adantr 
 |-  ( ( ph /\ t = Z ) -> J e. ZZ )
422 421 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> J e. ZZ )
423 xp1st 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. { k } )
424 elsni 
 |-  ( ( 1st ` p ) e. { k } -> ( 1st ` p ) = k )
425 423 424 syl 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) = k )
426 425 adantl 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
427 107 sseli 
 |-  ( k e. ( 0 ... J ) -> k e. ZZ )
428 427 adantr 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ZZ )
429 426 428 eqeltrd 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
430 429 3adant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
431 430 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( 1st ` p ) e. ZZ )
432 422 431 zsubcld 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) e. ZZ )
433 420 432 eqeltrd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ )
434 433 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ )
435 414 415 434 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ )
436 413 435 pm2.61dan 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ )
437 409 ffvelrnda 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) )
438 elfzle1 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
439 437 438 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
440 382 eqcomd 
 |-  ( t e. R -> ( ( 2nd ` p ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
441 440 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
442 439 441 breqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
443 442 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
444 simpll 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) )
445 elfzle2 
 |-  ( k e. ( 0 ... J ) -> k <_ J )
446 elfzel2 
 |-  ( k e. ( 0 ... J ) -> J e. ZZ )
447 446 zred 
 |-  ( k e. ( 0 ... J ) -> J e. RR )
448 109 sseli 
 |-  ( k e. ( 0 ... J ) -> k e. RR )
449 447 448 subge0d 
 |-  ( k e. ( 0 ... J ) -> ( 0 <_ ( J - k ) <-> k <_ J ) )
450 445 449 mpbird 
 |-  ( k e. ( 0 ... J ) -> 0 <_ ( J - k ) )
451 450 adantr 
 |-  ( ( k e. ( 0 ... J ) /\ t = Z ) -> 0 <_ ( J - k ) )
452 451 3ad2antl2 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> 0 <_ ( J - k ) )
453 384 418 sylan 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> -. t e. R )
454 453 iffalsed 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
455 426 3adant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
456 455 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
457 456 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
458 454 457 eqtr2d 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - k ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
459 452 458 breqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
460 444 415 459 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
461 443 460 pm2.61dan 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
462 simpl2 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> k e. ( 0 ... J ) )
463 fzssz 
 |-  ( 0 ... k ) C_ ZZ
464 463 sseli 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
465 464 zred 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. RR )
466 465 adantr 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) e. RR )
467 448 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k e. RR )
468 447 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> J e. RR )
469 elfzle2 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) <_ k )
470 469 adantr 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ k )
471 445 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k <_ J )
472 466 467 468 470 471 letrd 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ J )
473 437 462 472 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) <_ J )
474 473 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) <_ J )
475 383 474 eqbrtrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J )
476 458 eqcomd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - k ) )
477 398 nn0ge0d 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> 0 <_ k )
478 447 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> J e. RR )
479 448 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. RR )
480 478 479 subge02d 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 <_ k <-> ( J - k ) <_ J ) )
481 477 480 mpbid 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( J - k ) <_ J )
482 481 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ t = Z ) -> ( J - k ) <_ J )
483 482 3adantl3 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - k ) <_ J )
484 476 483 eqbrtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J )
485 444 415 484 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J )
486 475 485 pm2.61dan 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J )
487 379 381 436 461 486 elfzd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ( 0 ... J ) )
488 eqid 
 |-  ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
489 378 487 488 fmptdf 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) : ( R u. { Z } ) --> ( 0 ... J ) )
490 ovexd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 0 ... J ) e. _V )
491 384 21 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( R u. { Z } ) e. _V )
492 490 491 elmapd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) <-> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) : ( R u. { Z } ) --> ( 0 ... J ) ) )
493 489 492 mpbird 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
494 eqidd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
495 eleq1w 
 |-  ( r = t -> ( r e. R <-> t e. R ) )
496 fveq2 
 |-  ( r = t -> ( ( 2nd ` p ) ` r ) = ( ( 2nd ` p ) ` t ) )
497 495 496 ifbieq1d 
 |-  ( r = t -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
498 497 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ r = t ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
499 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> t e. ( R u. { Z } ) )
500 494 498 499 436 fvmptd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
501 500 ex 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) -> ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) )
502 378 501 ralrimi 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> A. t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
503 502 sumeq2d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = sum_ t e. ( R u. { Z } ) if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
504 nfcv 
 |-  F/_ t if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) )
505 384 105 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> R e. Fin )
506 384 5 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> Z e. T )
507 384 6 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
508 382 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
509 437 elfzelzd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
510 509 zcnd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. CC )
511 508 510 eqeltrd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. CC )
512 eleq1 
 |-  ( t = Z -> ( t e. R <-> Z e. R ) )
513 fveq2 
 |-  ( t = Z -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` Z ) )
514 512 513 ifbieq1d 
 |-  ( t = Z -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) )
515 6 adantr 
 |-  ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
516 515 iffalsed 
 |-  ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
517 516 3adant2 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
518 10 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. ZZ )
519 518 430 zsubcld 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ZZ )
520 519 zcnd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. CC )
521 517 520 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) e. CC )
522 378 504 505 506 507 511 514 521 fsumsplitsn 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. ( R u. { Z } ) if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( sum_ t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) + if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) ) )
523 382 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. R -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) ) )
524 378 523 ralrimi 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> A. t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
525 524 sumeq2d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = sum_ t e. R ( ( 2nd ` p ) ` t ) )
526 eqidd 
 |-  ( c = ( 2nd ` p ) -> R = R )
527 simpl 
 |-  ( ( c = ( 2nd ` p ) /\ t e. R ) -> c = ( 2nd ` p ) )
528 527 fveq1d 
 |-  ( ( c = ( 2nd ` p ) /\ t e. R ) -> ( c ` t ) = ( ( 2nd ` p ) ` t ) )
529 526 528 sumeq12rdv 
 |-  ( c = ( 2nd ` p ) -> sum_ t e. R ( c ` t ) = sum_ t e. R ( ( 2nd ` p ) ` t ) )
530 529 eqeq1d 
 |-  ( c = ( 2nd ` p ) -> ( sum_ t e. R ( c ` t ) = k <-> sum_ t e. R ( ( 2nd ` p ) ` t ) = k ) )
531 530 elrab 
 |-  ( ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } <-> ( ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) /\ sum_ t e. R ( ( 2nd ` p ) ` t ) = k ) )
532 404 531 sylib 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) /\ sum_ t e. R ( ( 2nd ` p ) ` t ) = k ) )
533 532 simprd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. R ( ( 2nd ` p ) ` t ) = k )
534 525 533 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = k )
535 507 iffalsed 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
536 535 456 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - k ) )
537 534 536 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( sum_ t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) + if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) ) = ( k + ( J - k ) ) )
538 321 sseli 
 |-  ( k e. ( 0 ... J ) -> k e. CC )
539 538 3ad2ant2 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. CC )
540 384 298 syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. CC )
541 539 540 pncan3d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k + ( J - k ) ) = J )
542 537 541 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( sum_ t e. R if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) + if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) ) = J )
543 503 522 542 3eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J )
544 493 543 jca 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J ) )
545 eleq1w 
 |-  ( t = r -> ( t e. R <-> r e. R ) )
546 fveq2 
 |-  ( t = r -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` r ) )
547 545 546 ifbieq1d 
 |-  ( t = r -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) )
548 547 cbvmptv 
 |-  ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) )
549 548 eqeq2i 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) <-> c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
550 549 biimpi 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
551 fveq1 
 |-  ( c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) -> ( c ` t ) = ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) )
552 551 sumeq2sdv 
 |-  ( c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) )
553 550 552 syl 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) )
554 553 eqeq1d 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = J <-> sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J ) )
555 554 elrab 
 |-  ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } <-> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J ) )
556 544 555 sylibr 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
557 556 3exp 
 |-  ( ph -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } ) ) )
558 557 adantr 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } ) ) )
559 367 368 558 rexlimd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } ) )
560 362 559 mpd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
561 40 eqcomd 
 |-  ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } = ( ( C ` ( R u. { Z } ) ) ` J ) )
562 561 adantr 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } = ( ( C ` ( R u. { Z } ) ) ` J ) )
563 560 562 eleqtrd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( C ` ( R u. { Z } ) ) ` J ) )
564 3 a1i 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
565 simpr 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) )
566 548 a1i 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
567 565 566 eqtrd 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
568 simpr 
 |-  ( ( ph /\ r = Z ) -> r = Z )
569 6 adantr 
 |-  ( ( ph /\ r = Z ) -> -. Z e. R )
570 568 569 eqneltrd 
 |-  ( ( ph /\ r = Z ) -> -. r e. R )
571 570 iffalsed 
 |-  ( ( ph /\ r = Z ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
572 571 adantlr 
 |-  ( ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) /\ r = Z ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
573 52 adantr 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> Z e. ( R u. { Z } ) )
574 ovexd 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( 1st ` p ) ) e. _V )
575 567 572 573 574 fvmptd 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( c ` Z ) = ( J - ( 1st ` p ) ) )
576 575 oveq2d 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( c ` Z ) ) = ( J - ( J - ( 1st ` p ) ) ) )
577 576 adantlr 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( c ` Z ) ) = ( J - ( J - ( 1st ` p ) ) ) )
578 298 ad2antrr 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> J e. CC )
579 nfv 
 |-  F/ k ( 1st ` p ) e. ( 0 ... J )
580 simpl 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
581 simpr 
 |-  ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> ( 1st ` p ) = k )
582 simpl 
 |-  ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> k e. ( 0 ... J ) )
583 581 582 eqeltrd 
 |-  ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> ( 1st ` p ) e. ( 0 ... J ) )
584 580 426 583 syl2anc 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
585 584 ex 
 |-  ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) )
586 585 a1i 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) ) )
587 366 579 586 rexlimd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) )
588 361 587 mpd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
589 588 elfzelzd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ZZ )
590 589 zcnd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. CC )
591 590 ad2antlr 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( 1st ` p ) e. CC )
592 578 591 nncand 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( J - ( 1st ` p ) ) ) = ( 1st ` p ) )
593 577 592 eqtrd 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( c ` Z ) ) = ( 1st ` p ) )
594 reseq1 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> ( c |` R ) = ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) |` R ) )
595 594 adantl 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( c |` R ) = ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) |` R ) )
596 70 a1i 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> R C_ ( R u. { Z } ) )
597 596 resmptd 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) |` R ) = ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) )
598 nfv 
 |-  F/ k ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p )
599 382 mpteq2ia 
 |-  ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) )
600 599 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) ) )
601 409 feqmptd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) ) )
602 600 601 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) )
603 602 3exp 
 |-  ( ph -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) ) ) )
604 603 adantr 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) ) ) )
605 367 598 604 rexlimd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) ) )
606 362 605 mpd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) )
607 606 adantr 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p ) )
608 595 597 607 3eqtrd 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( c |` R ) = ( 2nd ` p ) )
609 593 608 opeq12d 
 |-  ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
610 opex 
 |-  <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V
611 610 a1i 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V )
612 564 609 563 611 fvmptd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( D ` ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) = <. ( 1st ` p ) , ( 2nd ` p ) >. )
613 nfv 
 |-  F/ k <. ( 1st ` p ) , ( 2nd ` p ) >. = p
614 1st2nd2 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
615 614 eqcomd 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
616 615 a1i 
 |-  ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p ) )
617 616 a1i 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p ) ) )
618 367 613 617 rexlimd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p ) )
619 362 618 mpd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
620 612 619 eqtr2d 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> p = ( D ` ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) )
621 fveq2 
 |-  ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> ( D ` c ) = ( D ` ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) )
622 621 rspceeqv 
 |-  ( ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ p = ( D ` ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) ) -> E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) )
623 563 620 622 syl2anc 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) )
624 623 ralrimiva 
 |-  ( ph -> A. p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) )
625 243 624 jca 
 |-  ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) ) )
626 dffo3 
 |-  ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) ) )
627 625 626 sylibr 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
628 359 627 jca 
 |-  ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) )
629 df-f1o 
 |-  ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) )
630 628 629 sylibr 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )