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 
 |-  ( n = J -> ( 0 ... n ) = ( 0 ... J ) )
13 12 oveq1d 
 |-  ( n = J -> ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
14 eqeq2 
 |-  ( n = J -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
15 13 14 rabeqbidv 
 |-  ( 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 } )
16 oveq2 
 |-  ( s = ( R u. { Z } ) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) )
17 sumeq1 
 |-  ( s = ( R u. { Z } ) -> sum_ t e. s ( c ` t ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
18 17 eqeq1d 
 |-  ( s = ( R u. { Z } ) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = n ) )
19 16 18 rabeqbidv 
 |-  ( 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 } )
20 19 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 } ) )
21 4 7 sselpwd 
 |-  ( ph -> ( R u. { Z } ) e. ~P T )
22 nn0ex 
 |-  NN0 e. _V
23 22 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V
24 23 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V )
25 1 20 21 24 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 } ) )
26 ovex 
 |-  ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. _V
27 26 rabex 
 |-  { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V
28 27 a1i 
 |-  ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V )
29 15 25 2 28 fvmptd4 
 |-  ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
30 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 } ) )
31 29 30 eqsstrdi 
 |-  ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
32 31 sselda 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
33 elmapi 
 |-  ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
34 32 33 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
35 snidg 
 |-  ( Z e. T -> Z e. { Z } )
36 elun2 
 |-  ( Z e. { Z } -> Z e. ( R u. { Z } ) )
37 5 35 36 3syl 
 |-  ( ph -> Z e. ( R u. { Z } ) )
38 37 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
39 34 38 ffvelcdmd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... J ) )
40 39 elfzelzd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ZZ )
41 11 40 zsubcld 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ZZ )
42 elfzle2 
 |-  ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) <_ J )
43 39 42 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) <_ J )
44 11 zred 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. RR )
45 40 zred 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. RR )
46 44 45 subge0d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( J - ( c ` Z ) ) <-> ( c ` Z ) <_ J ) )
47 43 46 mpbird 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( J - ( c ` Z ) ) )
48 elfzle1 
 |-  ( ( c ` Z ) e. ( 0 ... J ) -> 0 <_ ( c ` Z ) )
49 39 48 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( c ` Z ) )
50 44 45 subge02d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( c ` Z ) <-> ( J - ( c ` Z ) ) <_ J ) )
51 49 50 mpbid 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) <_ J )
52 9 11 41 47 51 elfzd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
53 eqidd 
 |-  ( e = ( c |` R ) -> R = R )
54 simpl 
 |-  ( ( e = ( c |` R ) /\ t e. R ) -> e = ( c |` R ) )
55 54 fveq1d 
 |-  ( ( e = ( c |` R ) /\ t e. R ) -> ( e ` t ) = ( ( c |` R ) ` t ) )
56 53 55 sumeq12rdv 
 |-  ( e = ( c |` R ) -> sum_ t e. R ( e ` t ) = sum_ t e. R ( ( c |` R ) ` t ) )
57 56 eqeq1d 
 |-  ( e = ( c |` R ) -> ( sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) <-> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
58 ovexd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... ( J - ( c ` Z ) ) ) e. _V )
59 7 unssad 
 |-  ( ph -> R C_ T )
60 4 59 ssfid 
 |-  ( ph -> R e. Fin )
61 60 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
62 elmapfn 
 |-  ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c Fn ( R u. { Z } ) )
63 32 62 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c Fn ( R u. { Z } ) )
64 ssun1 
 |-  R C_ ( R u. { Z } )
65 64 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R C_ ( R u. { Z } ) )
66 63 65 fnssresd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) Fn R )
67 nfv 
 |-  F/ t ph
68 nfcv 
 |-  F/_ t ~P T
69 nfcv 
 |-  F/_ t NN0
70 nfcv 
 |-  F/_ t s
71 70 nfsum1 
 |-  F/_ t sum_ t e. s ( c ` t )
72 71 nfeq1 
 |-  F/ t sum_ t e. s ( c ` t ) = n
73 nfcv 
 |-  F/_ t ( ( 0 ... n ) ^m s )
74 72 73 nfrabw 
 |-  F/_ t { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n }
75 69 74 nfmpt 
 |-  F/_ t ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } )
76 68 75 nfmpt 
 |-  F/_ t ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
77 1 76 nfcxfr 
 |-  F/_ t C
78 nfcv 
 |-  F/_ t ( R u. { Z } )
79 77 78 nffv 
 |-  F/_ t ( C ` ( R u. { Z } ) )
80 nfcv 
 |-  F/_ t J
81 79 80 nffv 
 |-  F/_ t ( ( C ` ( R u. { Z } ) ) ` J )
82 81 nfcri 
 |-  F/ t c e. ( ( C ` ( R u. { Z } ) ) ` J )
83 67 82 nfan 
 |-  F/ t ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
84 fvres 
 |-  ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) )
85 84 adantl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( c ` t ) )
86 0zd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 e. ZZ )
87 41 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( J - ( c ` Z ) ) e. ZZ )
88 34 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
89 65 sselda 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. ( R u. { Z } ) )
90 88 89 ffvelcdmd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... J ) )
91 90 elfzelzd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ZZ )
92 elfzle1 
 |-  ( ( c ` t ) e. ( 0 ... J ) -> 0 <_ ( c ` t ) )
93 90 92 syl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 <_ ( c ` t ) )
94 60 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> R e. Fin )
95 fzssre 
 |-  ( 0 ... J ) C_ RR
96 34 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
97 65 sselda 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> r e. ( R u. { Z } ) )
98 96 97 ffvelcdmd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. ( 0 ... J ) )
99 95 98 sselid 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. RR )
100 99 adantlr 
 |-  ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> ( c ` r ) e. RR )
101 elfzle1 
 |-  ( ( c ` r ) e. ( 0 ... J ) -> 0 <_ ( c ` r ) )
102 98 101 syl 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> 0 <_ ( c ` r ) )
103 102 adantlr 
 |-  ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> 0 <_ ( c ` r ) )
104 fveq2 
 |-  ( r = t -> ( c ` r ) = ( c ` t ) )
105 simpr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. R )
106 94 100 103 104 105 fsumge1 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ sum_ r e. R ( c ` r ) )
107 99 recnd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. CC )
108 61 107 fsumcl 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) e. CC )
109 40 zcnd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. CC )
110 104 cbvsumv 
 |-  sum_ r e. ( R u. { Z } ) ( c ` r ) = sum_ t e. ( R u. { Z } ) ( c ` t )
111 nfv 
 |-  F/ r ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
112 nfcv 
 |-  F/_ r ( c ` Z )
113 5 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
114 6 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
115 fveq2 
 |-  ( r = Z -> ( c ` r ) = ( c ` Z ) )
116 111 112 61 113 114 107 115 109 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 ) ) )
117 simpr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
118 29 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 } )
119 117 118 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 } )
120 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 ) )
121 119 120 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 ) )
122 121 simprd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = J )
123 110 116 122 3eqtr3a 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = J )
124 108 109 123 mvlraddd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
125 124 adantr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
126 106 125 breqtrd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ ( J - ( c ` Z ) ) )
127 86 87 91 93 126 elfzd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
128 85 127 eqeltrd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
129 83 128 ralrimia 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
130 ffnfv 
 |-  ( ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) <-> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
131 66 129 130 sylanbrc 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) )
132 58 61 131 elmapdd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
133 84 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) ) )
134 83 133 ralrimi 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) = ( c ` t ) )
135 134 sumeq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = sum_ t e. R ( c ` t ) )
136 104 cbvsumv 
 |-  sum_ r e. R ( c ` r ) = sum_ t e. R ( c ` t )
137 136 eqcomi 
 |-  sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r )
138 137 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r ) )
139 135 138 124 3eqtrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) )
140 57 132 139 elrabd 
 |-  ( ( 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 ) ) } )
141 fveq1 
 |-  ( c = e -> ( c ` t ) = ( e ` t ) )
142 141 sumeq2sdv 
 |-  ( c = e -> sum_ t e. R ( c ` t ) = sum_ t e. R ( e ` t ) )
143 142 eqeq1d 
 |-  ( c = e -> ( sum_ t e. R ( c ` t ) = m <-> sum_ t e. R ( e ` t ) = m ) )
144 143 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 }
145 144 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 } )
146 oveq2 
 |-  ( m = ( J - ( c ` Z ) ) -> ( 0 ... m ) = ( 0 ... ( J - ( c ` Z ) ) ) )
147 146 oveq1d 
 |-  ( m = ( J - ( c ` Z ) ) -> ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
148 147 rabeqdv 
 |-  ( 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 } )
149 eqeq2 
 |-  ( m = ( J - ( c ` Z ) ) -> ( sum_ t e. R ( e ` t ) = m <-> sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) ) )
150 149 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 ) ) } )
151 145 148 150 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 ) ) } )
152 oveq2 
 |-  ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
153 sumeq1 
 |-  ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
154 153 eqeq1d 
 |-  ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
155 152 154 rabeqbidv 
 |-  ( 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 } )
156 155 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 } ) )
157 4 59 sselpwd 
 |-  ( ph -> R e. ~P T )
158 22 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
159 158 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
160 1 156 157 159 fvmptd3 
 |-  ( ph -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
161 160 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 } ) )
162 oveq2 
 |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
163 162 oveq1d 
 |-  ( n = m -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) )
164 eqeq2 
 |-  ( n = m -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = m ) )
165 163 164 rabeqbidv 
 |-  ( 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 } )
166 165 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 } )
167 161 166 eqtrdi 
 |-  ( ( 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 } ) )
168 elnn0z 
 |-  ( ( J - ( c ` Z ) ) e. NN0 <-> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
169 41 47 168 sylanbrc 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. NN0 )
170 ovex 
 |-  ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) e. _V
171 170 rabex 
 |-  { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } e. _V
172 171 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 )
173 151 167 169 172 fvmptd4 
 |-  ( ( 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 ) ) } )
174 140 173 eleqtrrd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
175 52 174 jca 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
176 ovexd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. _V )
177 vex 
 |-  c e. _V
178 177 resex 
 |-  ( c |` R ) e. _V
179 opeq12 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> <. k , d >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
180 179 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 ) >. ) )
181 eleq1 
 |-  ( k = ( J - ( c ` Z ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
182 181 adantr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
183 simpr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> d = ( c |` R ) )
184 fveq2 
 |-  ( k = ( J - ( c ` Z ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
185 184 adantr 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
186 183 185 eleq12d 
 |-  ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( d e. ( ( C ` R ) ` k ) <-> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
187 182 186 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 ) ) ) ) ) )
188 180 187 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 ) ) ) ) ) ) )
189 188 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 ) ) ) ) )
190 176 178 189 sylancl 
 |-  ( ( 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 ) ) ) ) )
191 8 175 190 mp2and 
 |-  ( ( 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 ) ) ) )
192 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 ) ) ) )
193 191 192 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 ) ) )
194 193 3 fmptd 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
195 81 nfcri 
 |-  F/ t e e. ( ( C ` ( R u. { Z } ) ) ` J )
196 82 195 nfan 
 |-  F/ t ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
197 67 196 nfan 
 |-  F/ t ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
198 nfv 
 |-  F/ t ( D ` c ) = ( D ` e )
199 197 198 nfan 
 |-  F/ t ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) )
200 85 eqcomd 
 |-  ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
201 200 adantlrr 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
202 201 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 ) )
203 3 a1i 
 |-  ( ph -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
204 opex 
 |-  <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V
205 204 a1i 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V )
206 203 205 fvmpt2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
207 206 fveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
208 207 fveq1d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) )
209 ovex 
 |-  ( J - ( c ` Z ) ) e. _V
210 209 178 op2nd 
 |-  ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( c |` R )
211 210 fveq1i 
 |-  ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t )
212 208 211 eqtr2di 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
213 212 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
214 213 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 ) )
215 simpr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = ( D ` e ) )
216 fveq1 
 |-  ( c = e -> ( c ` Z ) = ( e ` Z ) )
217 216 oveq2d 
 |-  ( c = e -> ( J - ( c ` Z ) ) = ( J - ( e ` Z ) ) )
218 reseq1 
 |-  ( c = e -> ( c |` R ) = ( e |` R ) )
219 217 218 opeq12d 
 |-  ( c = e -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
220 simpr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
221 opex 
 |-  <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V
222 221 a1i 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V )
223 3 219 220 222 fvmptd3 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
224 223 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
225 215 224 eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
226 225 fveq2d 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
227 226 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 ) >. ) )
228 227 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 ) >. ) )
229 ovex 
 |-  ( J - ( e ` Z ) ) e. _V
230 vex 
 |-  e e. _V
231 230 resex 
 |-  ( e |` R ) e. _V
232 229 231 op2nd 
 |-  ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( e |` R )
233 228 232 eqtrdi 
 |-  ( ( ( ( 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 ) )
234 233 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 ) )
235 fvres 
 |-  ( t e. R -> ( ( e |` R ) ` t ) = ( e ` t ) )
236 235 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 ) )
237 234 236 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 ) )
238 202 214 237 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 ) )
239 238 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 ) )
240 elunnel1 
 |-  ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t e. { Z } )
241 elsni 
 |-  ( t e. { Z } -> t = Z )
242 240 241 syl 
 |-  ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t = Z )
243 242 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 )
244 simpr 
 |-  ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> t = Z )
245 244 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 ) )
246 2 nn0cnd 
 |-  ( ph -> J e. CC )
247 246 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
248 247 109 nncand 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( c ` Z ) )
249 248 eqcomd 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
250 249 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
251 250 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 ) ) ) )
252 206 fveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
253 209 178 op1st 
 |-  ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) )
254 252 253 eqtr2di 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) = ( 1st ` ( D ` c ) ) )
255 254 oveq2d 
 |-  ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
256 255 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
257 256 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 ) ) ) )
258 fveq2 
 |-  ( ( D ` c ) = ( D ` e ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
259 258 adantl 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
260 223 fveq2d 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
261 260 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
262 229 231 op1st 
 |-  ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) )
263 262 a1i 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) ) )
264 259 261 263 3eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( J - ( e ` Z ) ) )
265 264 oveq2d 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( J - ( J - ( e ` Z ) ) ) )
266 246 adantr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
267 fzsscn 
 |-  ( 0 ... J ) C_ CC
268 eleq1w 
 |-  ( c = e -> ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) <-> e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
269 268 anbi2d 
 |-  ( c = e -> ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) <-> ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) )
270 feq1 
 |-  ( c = e -> ( c : ( R u. { Z } ) --> ( 0 ... J ) <-> e : ( R u. { Z } ) --> ( 0 ... J ) ) )
271 269 270 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 ) ) ) )
272 271 34 chvarvv 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) )
273 37 adantr 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
274 272 273 ffvelcdmd 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. ( 0 ... J ) )
275 267 274 sselid 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. CC )
276 266 275 nncand 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
277 276 adantr 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
278 265 277 eqtrd 
 |-  ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
279 278 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 ) )
280 251 257 279 3eqtrd 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c ` Z ) = ( e ` Z ) )
281 280 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 ) )
282 fveq2 
 |-  ( t = Z -> ( e ` t ) = ( e ` Z ) )
283 282 eqcomd 
 |-  ( t = Z -> ( e ` Z ) = ( e ` t ) )
284 283 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 ) )
285 245 281 284 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 ) )
286 285 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 ) )
287 243 286 syldan 
 |-  ( ( ( ( ( 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 ) )
288 239 287 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 ) )
289 199 288 ralrimia 
 |-  ( ( ( 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 ) )
290 63 adantrr 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> c Fn ( R u. { Z } ) )
291 290 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 } ) )
292 272 ffnd 
 |-  ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e Fn ( R u. { Z } ) )
293 292 adantrl 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> e Fn ( R u. { Z } ) )
294 293 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 } ) )
295 eqfnfv 
 |-  ( ( c Fn ( R u. { Z } ) /\ e Fn ( R u. { Z } ) ) -> ( c = e <-> A. t e. ( R u. { Z } ) ( c ` t ) = ( e ` t ) ) )
296 291 294 295 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 ) ) )
297 289 296 mpbird 
 |-  ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> c = e )
298 297 ex 
 |-  ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( D ` c ) = ( D ` e ) -> c = e ) )
299 298 ralrimivva 
 |-  ( ph -> A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) )
300 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 ) ) )
301 194 299 300 sylanbrc 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
302 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 ) ) )
303 302 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 ) ) )
304 303 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 ) ) )
305 nfv 
 |-  F/ k ph
306 nfiu1 
 |-  F/_ k U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
307 306 nfcri 
 |-  F/ k p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
308 305 307 nfan 
 |-  F/ k ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
309 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 }
310 eleq1w 
 |-  ( t = r -> ( t e. R <-> r e. R ) )
311 fveq2 
 |-  ( t = r -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` r ) )
312 310 311 ifbieq1d 
 |-  ( t = r -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) )
313 312 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 ) ) ) )
314 313 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 ) ) ) ) )
315 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 ) )
316 315 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 ) )
317 314 316 sylbi 
 |-  ( 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 ) )
318 317 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 ) )
319 ovexd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 0 ... J ) e. _V )
320 4 7 ssexd 
 |-  ( ph -> ( R u. { Z } ) e. _V )
321 320 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( R u. { Z } ) e. _V )
322 nfv 
 |-  F/ t k e. ( 0 ... J )
323 nfcv 
 |-  F/_ t { k }
324 nfcv 
 |-  F/_ t R
325 77 324 nffv 
 |-  F/_ t ( C ` R )
326 nfcv 
 |-  F/_ t k
327 325 326 nffv 
 |-  F/_ t ( ( C ` R ) ` k )
328 323 327 nfxp 
 |-  F/_ t ( { k } X. ( ( C ` R ) ` k ) )
329 328 nfcri 
 |-  F/ t p e. ( { k } X. ( ( C ` R ) ` k ) )
330 67 322 329 nf3an 
 |-  F/ t ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) )
331 0zd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> 0 e. ZZ )
332 10 adantr 
 |-  ( ( ph /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
333 332 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
334 iftrue 
 |-  ( t e. R -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
335 334 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 ) )
336 xp2nd 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
337 336 3ad2ant3 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
338 oveq2 
 |-  ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
339 338 oveq1d 
 |-  ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
340 eqeq2 
 |-  ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
341 339 340 rabeqbidv 
 |-  ( 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 } )
342 160 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
343 elfznn0 
 |-  ( k e. ( 0 ... J ) -> k e. NN0 )
344 343 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
345 ovex 
 |-  ( ( 0 ... k ) ^m R ) e. _V
346 345 rabex 
 |-  { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V
347 346 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
348 341 342 344 347 fvmptd4 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
349 348 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 } )
350 337 349 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 } )
351 elrabi 
 |-  ( ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
352 elmapi 
 |-  ( ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
353 350 351 352 3syl 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
354 353 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
355 354 ffvelcdmda 
 |-  ( ( ( ( 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 ) )
356 355 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 )
357 335 356 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 )
358 242 adantll 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> t = Z )
359 simpr 
 |-  ( ( ph /\ t = Z ) -> t = Z )
360 6 adantr 
 |-  ( ( ph /\ t = Z ) -> -. Z e. R )
361 359 360 eqneltrd 
 |-  ( ( ph /\ t = Z ) -> -. t e. R )
362 361 iffalsed 
 |-  ( ( ph /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
363 362 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 ) ) )
364 10 adantr 
 |-  ( ( ph /\ t = Z ) -> J e. ZZ )
365 364 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> J e. ZZ )
366 xp1st 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. { k } )
367 elsni 
 |-  ( ( 1st ` p ) e. { k } -> ( 1st ` p ) = k )
368 366 367 syl 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) = k )
369 368 adantl 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
370 elfzelz 
 |-  ( k e. ( 0 ... J ) -> k e. ZZ )
371 370 adantr 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ZZ )
372 369 371 eqeltrd 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
373 372 3adant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
374 373 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( 1st ` p ) e. ZZ )
375 365 374 zsubcld 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) e. ZZ )
376 363 375 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 )
377 376 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 )
378 358 377 syldan 
 |-  ( ( ( ( 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 )
379 357 378 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 )
380 353 ffvelcdmda 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) )
381 elfzle1 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
382 380 381 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
383 334 eqcomd 
 |-  ( t e. R -> ( ( 2nd ` p ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
384 383 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 ) ) ) )
385 382 384 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 ) ) ) )
386 385 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 ) ) ) )
387 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 ) ) ) )
388 elfzle2 
 |-  ( k e. ( 0 ... J ) -> k <_ J )
389 elfzel2 
 |-  ( k e. ( 0 ... J ) -> J e. ZZ )
390 389 zred 
 |-  ( k e. ( 0 ... J ) -> J e. RR )
391 95 sseli 
 |-  ( k e. ( 0 ... J ) -> k e. RR )
392 390 391 subge0d 
 |-  ( k e. ( 0 ... J ) -> ( 0 <_ ( J - k ) <-> k <_ J ) )
393 388 392 mpbird 
 |-  ( k e. ( 0 ... J ) -> 0 <_ ( J - k ) )
394 393 adantr 
 |-  ( ( k e. ( 0 ... J ) /\ t = Z ) -> 0 <_ ( J - k ) )
395 394 3ad2antl2 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> 0 <_ ( J - k ) )
396 361 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> -. t e. R )
397 396 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 ) ) )
398 368 3ad2ant3 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
399 398 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
400 399 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
401 397 400 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 ) ) ) )
402 395 401 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 ) ) ) )
403 387 358 402 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 ) ) ) )
404 386 403 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 ) ) ) )
405 simpl2 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> k e. ( 0 ... J ) )
406 elfzelz 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
407 406 zred 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. RR )
408 407 adantr 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) e. RR )
409 391 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k e. RR )
410 390 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> J e. RR )
411 elfzle2 
 |-  ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) <_ k )
412 411 adantr 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ k )
413 388 adantl 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k <_ J )
414 408 409 410 412 413 letrd 
 |-  ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ J )
415 380 405 414 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) <_ J )
416 415 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 )
417 335 416 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 )
418 344 nn0ge0d 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> 0 <_ k )
419 390 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> J e. RR )
420 391 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. RR )
421 419 420 subge02d 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 <_ k <-> ( J - k ) <_ J ) )
422 418 421 mpbid 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( J - k ) <_ J )
423 422 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ t = Z ) -> ( J - k ) <_ J )
424 423 3adantl3 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - k ) <_ J )
425 401 424 eqbrtrrd 
 |-  ( ( ( 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 )
426 387 358 425 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 )
427 417 426 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 )
428 331 333 379 404 427 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 ) )
429 330 428 fmptd2f 
 |-  ( ( 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 ) )
430 319 321 429 elmapdd 
 |-  ( ( 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 } ) ) )
431 eleq1w 
 |-  ( r = t -> ( r e. R <-> t e. R ) )
432 fveq2 
 |-  ( r = t -> ( ( 2nd ` p ) ` r ) = ( ( 2nd ` p ) ` t ) )
433 431 432 ifbieq1d 
 |-  ( r = t -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
434 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 ) ) ) ) )
435 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> t e. ( R u. { Z } ) )
436 433 434 435 379 fvmptd4 
 |-  ( ( ( 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 ) ) ) )
437 330 436 ralrimia 
 |-  ( ( 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 ) ) ) )
438 437 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 ) ) ) )
439 nfcv 
 |-  F/_ t if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) )
440 60 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> R e. Fin )
441 5 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> Z e. T )
442 6 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
443 334 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 ) )
444 380 elfzelzd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
445 444 zcnd 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. CC )
446 443 445 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 )
447 eleq1 
 |-  ( t = Z -> ( t e. R <-> Z e. R ) )
448 fveq2 
 |-  ( t = Z -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` Z ) )
449 447 448 ifbieq1d 
 |-  ( t = Z -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) )
450 6 adantr 
 |-  ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
451 450 iffalsed 
 |-  ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
452 451 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 ) ) )
453 10 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. ZZ )
454 453 373 zsubcld 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ZZ )
455 454 zcnd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. CC )
456 452 455 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 )
457 330 439 440 441 442 446 449 456 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 ) ) ) ) )
458 334 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 ) ) )
459 330 458 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 ) )
460 459 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 ) )
461 eqidd 
 |-  ( c = ( 2nd ` p ) -> R = R )
462 simpl 
 |-  ( ( c = ( 2nd ` p ) /\ t e. R ) -> c = ( 2nd ` p ) )
463 462 fveq1d 
 |-  ( ( c = ( 2nd ` p ) /\ t e. R ) -> ( c ` t ) = ( ( 2nd ` p ) ` t ) )
464 461 463 sumeq12rdv 
 |-  ( c = ( 2nd ` p ) -> sum_ t e. R ( c ` t ) = sum_ t e. R ( ( 2nd ` p ) ` t ) )
465 464 eqeq1d 
 |-  ( c = ( 2nd ` p ) -> ( sum_ t e. R ( c ` t ) = k <-> sum_ t e. R ( ( 2nd ` p ) ` t ) = k ) )
466 465 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 ) )
467 350 466 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 ) )
468 467 simprd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. R ( ( 2nd ` p ) ` t ) = k )
469 460 468 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 )
470 442 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 ) ) )
471 470 399 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 ) )
472 469 471 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 ) ) )
473 267 sseli 
 |-  ( k e. ( 0 ... J ) -> k e. CC )
474 473 3ad2ant2 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. CC )
475 246 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. CC )
476 474 475 pncan3d 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k + ( J - k ) ) = J )
477 472 476 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 )
478 438 457 477 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 )
479 318 430 478 elrabd 
 |-  ( ( 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 } )
480 479 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 } ) ) )
481 480 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 } ) ) )
482 308 309 481 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 } ) )
483 304 482 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 } )
484 29 eqcomd 
 |-  ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } = ( ( C ` ( R u. { Z } ) ) ` J ) )
485 484 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 ) )
486 483 485 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 ) )
487 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 ) ) ) ) )
488 487 313 eqtrdi 
 |-  ( ( 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 ) ) ) ) )
489 simpr 
 |-  ( ( ph /\ r = Z ) -> r = Z )
490 6 adantr 
 |-  ( ( ph /\ r = Z ) -> -. Z e. R )
491 489 490 eqneltrd 
 |-  ( ( ph /\ r = Z ) -> -. r e. R )
492 491 iffalsed 
 |-  ( ( ph /\ r = Z ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
493 492 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 ) ) )
494 37 adantr 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> Z e. ( R u. { Z } ) )
495 ovexd 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( 1st ` p ) ) e. _V )
496 488 493 494 495 fvmptd 
 |-  ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( c ` Z ) = ( J - ( 1st ` p ) ) )
497 496 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 ) ) ) )
498 497 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 ) ) ) )
499 246 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 )
500 nfv 
 |-  F/ k ( 1st ` p ) e. ( 0 ... J )
501 simpl 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
502 369 501 eqeltrd 
 |-  ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
503 502 ex 
 |-  ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) )
504 503 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 ) ) ) )
505 307 500 504 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 ) ) )
506 303 505 mpd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
507 506 elfzelzd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ZZ )
508 507 zcnd 
 |-  ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. CC )
509 508 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 )
510 499 509 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 ) )
511 498 510 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 ) )
512 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 ) )
513 512 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 ) )
514 64 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 } ) )
515 514 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 ) ) ) ) )
516 nfv 
 |-  F/ k ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p )
517 334 mpteq2ia 
 |-  ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) )
518 353 feqmptd 
 |-  ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) ) )
519 517 518 eqtr4id 
 |-  ( ( 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 ) )
520 519 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 ) ) ) )
521 520 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 ) ) ) )
522 308 516 521 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 ) ) )
523 304 522 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 ) )
524 523 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 ) )
525 513 515 524 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 ) )
526 511 525 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 ) >. )
527 opex 
 |-  <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V
528 527 a1i 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V )
529 3 526 486 528 fvmptd2 
 |-  ( ( 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 ) >. )
530 nfv 
 |-  F/ k <. ( 1st ` p ) , ( 2nd ` p ) >. = p
531 1st2nd2 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
532 531 eqcomd 
 |-  ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
533 532 2a1i 
 |-  ( ( 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 ) ) )
534 308 530 533 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 ) )
535 304 534 mpd 
 |-  ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
536 529 535 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 ) ) ) ) ) )
537 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 ) ) ) ) ) )
538 537 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 ) )
539 486 536 538 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 ) )
540 539 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 ) )
541 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 ) ) )
542 194 540 541 sylanbrc 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
543 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 ) ) ) )
544 301 542 543 sylanbrc 
 |-  ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )