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