Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem1 Structured version   Unicode version

Theorem dvnprodlem1 31982
Description:  D is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
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
Ref Expression
dvnprodlem1  |-  ( ph  ->  D : ( ( C `  ( R  u.  { Z }
) ) `  J
)
-1-1-onto-> U_ k  e.  ( 0 ... J ) ( { k }  X.  ( ( C `  R ) `  k
) ) )
Distinct variable groups:    C, c,
k    D, c, t    J, c, k, n, t    R, c, k, n, t    R, s, c, n, t    t, T, s    Z, c, k, n, t    Z, s    ph, c, n, t, k    ph, s
Allowed substitution hints:    C( t, n, s)    D( k, n, s)    T( k, n, c)    J( s)

Proof of Theorem dvnprodlem1
Dummy variables  d 
e  m  p  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2455 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  <. ( J  -  (
c `  Z )
) ,  ( c  |`  R ) >.  =  <. ( J  -  ( c `
 Z ) ) ,  ( c  |`  R ) >. )
2 0zd 10872 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
0  e.  ZZ )
3 dvnprodlem1.j . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  NN0 )
43nn0zd 10963 . . . . . . . . . . . . . 14  |-  ( ph  ->  J  e.  ZZ )
54adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  J  e.  ZZ )
6 fzssz 31706 . . . . . . . . . . . . . . . 16  |-  ( 0 ... J )  C_  ZZ
76a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0 ... J
)  C_  ZZ )
8 dvnprodlem1.c . . . . . . . . . . . . . . . . . . . . . . 23  |-  C  =  ( s  e.  ~P T  |->  ( n  e. 
NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s
)  |  sum_ t  e.  s  ( c `  t )  =  n } ) )
98a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  C  =  ( s  e.  ~P T  |->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n } ) ) )
10 oveq2 6278 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  =  ( R  u.  { Z } )  -> 
( ( 0 ... n )  ^m  s
)  =  ( ( 0 ... n )  ^m  ( R  u.  { Z } ) ) )
11 rabeq 3100 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 } )
1210, 11syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 } )
13 sumeq1 13593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  =  ( R  u.  { Z } )  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  ( R  u.  { Z } ) ( c `
 t ) )
1413eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( s  =  ( R  u.  { Z } )  -> 
( sum_ t  e.  s  ( c `  t
)  =  n  <->  sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  n ) )
1514rabbidv 3098 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 } )
1612, 15eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 } )
1716mpteq2dv 4526 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } ) )
1817adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  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 } ) )
19 dvnprodlem1.rzt . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( R  u.  { Z } )  C_  T
)
20 dvnprodlem1.t . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  T  e.  Fin )
21 ssexg 4583 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( R  u.  { Z } )  C_  T  /\  T  e.  Fin )  ->  ( R  u.  { Z } )  e. 
_V )
2219, 20, 21syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( R  u.  { Z } )  e.  _V )
23 elpwg 4007 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( R  u.  { Z } )  e.  _V  ->  ( ( R  u.  { Z } )  e. 
~P T  <->  ( R  u.  { Z } ) 
C_  T ) )
2422, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( R  u.  { Z } )  e. 
~P T  <->  ( R  u.  { Z } ) 
C_  T ) )
2519, 24mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( R  u.  { Z } )  e.  ~P T )
26 nn0ex 10797 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  e.  _V
2726mptex 6118 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  ( R  u.  { Z } ) )  | 
sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  n } )  e. 
_V
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  ( R  u.  { Z } ) )  |  sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  n } )  e. 
_V )
299, 18, 25, 28fvmptd 5936 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 } ) )
30 oveq2 6278 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  J  ->  (
0 ... n )  =  ( 0 ... J
) )
3130oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  J  ->  (
( 0 ... n
)  ^m  ( R  u.  { Z } ) )  =  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) ) )
32 rabeq 3100 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 } )
3331, 32syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } )
34 eqeq2 2469 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  J  ->  ( sum_ t  e.  ( R  u.  { Z }
) ( c `  t )  =  n  <->  sum_ t  e.  ( R  u.  { Z }
) ( c `  t )  =  J ) )
3534rabbidv 3098 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } )
3633, 35eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 } )
3736adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
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 } )
38 ovex 6298 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  e.  _V
3938rabex 4588 . . . . . . . . . . . . . . . . . . . . . 22  |-  { c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  | 
sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  J }  e.  _V
4039a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  { c  e.  ( ( 0 ... J
)  ^m  ( R  u.  { Z } ) )  |  sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  J }  e.  _V )
4129, 37, 3, 40fvmptd 5936 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( C `  ( R  u.  { Z } ) ) `  J )  =  {
c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  |  sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  J } )
42 ssrab2 3571 . . . . . . . . . . . . . . . . . . . . 21  |-  { c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  | 
sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )  =  J }  C_  (
( 0 ... J
)  ^m  ( R  u.  { Z } ) )
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 } ) ) )
4441, 43eqsstrd 3523 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C `  ( R  u.  { Z } ) ) `  J )  C_  (
( 0 ... J
)  ^m  ( R  u.  { Z } ) ) )
4544adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( C `  ( R  u.  { Z } ) ) `  J )  C_  (
( 0 ... J
)  ^m  ( R  u.  { Z } ) ) )
46 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
c  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
) )
4745, 46sseldd 3490 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) ) )
48 elmapi 7433 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  -> 
c : ( R  u.  { Z }
) --> ( 0 ... J ) )
4947, 48syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
c : ( R  u.  { Z }
) --> ( 0 ... J ) )
50 dvnprodlem1.z . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Z  e.  T )
51 snidg 4042 . . . . . . . . . . . . . . . . . . 19  |-  ( Z  e.  T  ->  Z  e.  { Z } )
5250, 51syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Z  e.  { Z } )
53 elun2 3658 . . . . . . . . . . . . . . . . . 18  |-  ( Z  e.  { Z }  ->  Z  e.  ( R  u.  { Z }
) )
5452, 53syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  e.  ( R  u.  { Z }
) )
5554adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  Z  e.  ( R  u.  { Z } ) )
5649, 55ffvelrnd 6008 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  e.  ( 0 ... J ) )
577, 56sseldd 3490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  e.  ZZ )
585, 57zsubcld 10970 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  e.  ZZ )
592, 5, 583jca 1174 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  (
c `  Z )
)  e.  ZZ ) )
60 elfzle2 11693 . . . . . . . . . . . . . 14  |-  ( ( c `  Z )  e.  ( 0 ... J )  ->  (
c `  Z )  <_  J )
6156, 60syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  <_  J )
625zred 10965 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  J  e.  RR )
6357zred 10965 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  e.  RR )
6462, 63subge0d 10138 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0  <_  ( J  -  ( c `  Z ) )  <->  ( c `  Z )  <_  J
) )
6561, 64mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
0  <_  ( J  -  ( c `  Z ) ) )
66 elfzle1 11692 . . . . . . . . . . . . . 14  |-  ( ( c `  Z )  e.  ( 0 ... J )  ->  0  <_  ( c `  Z
) )
6756, 66syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
0  <_  ( c `  Z ) )
6862, 63subge02d 10140 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0  <_  (
c `  Z )  <->  ( J  -  ( c `
 Z ) )  <_  J ) )
6967, 68mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  <_  J )
7059, 65, 69jca32 533 . . . . . . . . . . 11  |-  ( (
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 11682 . . . . . . . . . . 11  |-  ( ( 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 )
) )
7270, 71sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  e.  ( 0 ... J ) )
73 elmapfn 7434 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  ( ( 0 ... J )  ^m  ( R  u.  { Z } ) )  -> 
c  Fn  ( R  u.  { Z }
) )
7447, 73syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
c  Fn  ( R  u.  { Z }
) )
75 ssun1 3653 . . . . . . . . . . . . . . . . . 18  |-  R  C_  ( R  u.  { Z } )
7675a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  R  C_  ( R  u.  { Z } ) )
77 fnssres 5676 . . . . . . . . . . . . . . . . 17  |-  ( ( c  Fn  ( R  u.  { Z }
)  /\  R  C_  ( R  u.  { Z } ) )  -> 
( c  |`  R )  Fn  R )
7874, 76, 77syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c  |`  R )  Fn  R )
79 nfv 1712 . . . . . . . . . . . . . . . . . 18  |-  F/ t
ph
80 nfcv 2616 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t
c
81 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t ~P T
82 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t NN0
83 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ t
s
8483nfsum1 13594 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t sum_ t  e.  s  ( c `  t )
85 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t
n
8684, 85nfeq 2627 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ t
sum_ t  e.  s  ( c `  t
)  =  n
87 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t
( ( 0 ... n )  ^m  s
)
8886, 87nfrab 3036 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t { c  e.  ( ( 0 ... n
)  ^m  s )  |  sum_ t  e.  s  ( c `  t
)  =  n }
8982, 88nfmpt 4527 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t
( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  s )  |  sum_ t  e.  s  ( c `  t
)  =  n }
)
9081, 89nfmpt 4527 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ t
( s  e.  ~P T  |->  ( n  e. 
NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s
)  |  sum_ t  e.  s  ( c `  t )  =  n } ) )
918, 90nfcxfr 2614 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ t C
92 nfcv 2616 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ t
( R  u.  { Z } )
9391, 92nffv 5855 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t
( C `  ( R  u.  { Z } ) )
94 nfcv 2616 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t J
9593, 94nffv 5855 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t
( ( C `  ( R  u.  { Z } ) ) `  J )
9680, 95nfel 2629 . . . . . . . . . . . . . . . . . 18  |-  F/ t  c  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
)
9779, 96nfan 1933 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )
98 fvres 5862 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  R  ->  (
( c  |`  R ) `
 t )  =  ( c `  t
) )
9998adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( ( c  |`  R ) `  t
)  =  ( c `
 t ) )
1002adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  0  e.  ZZ )
10158adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( J  -  (
c `  Z )
)  e.  ZZ )
1026a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( 0 ... J
)  C_  ZZ )
10349adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  c : ( R  u.  { Z }
) --> ( 0 ... J ) )
10476sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  t  e.  ( R  u.  { Z }
) )
105103, 104ffvelrnd 6008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  e.  ( 0 ... J ) )
106102, 105sseldd 3490 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  e.  ZZ )
107100, 101, 1063jca 1174 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 11692 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( c `  t )  e.  ( 0 ... J )  ->  0  <_  ( c `  t
) )
109105, 108syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  0  <_  ( c `  t ) )
11019unssad 3667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  R  C_  T )
111 ssfi 7733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T  e.  Fin  /\  R  C_  T )  ->  R  e.  Fin )
11220, 110, 111syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  R  e.  Fin )
113112ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  R  e.  Fin )
114 zssre 10867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ZZ  C_  RR
1156, 114sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 ... J )  C_  RR
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  ( 0 ... J
)  C_  RR )
11749adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  c : ( R  u.  { Z }
) --> ( 0 ... J ) )
11876sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  r  e.  ( R  u.  { Z }
) )
119117, 118ffvelrnd 6008 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  ( c `  r
)  e.  ( 0 ... J ) )
120116, 119sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  ( c `  r
)  e.  RR )
121120adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  /\  r  e.  R )  ->  (
c `  r )  e.  RR )
122 elfzle1 11692 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  r )  e.  ( 0 ... J )  ->  0  <_  ( c `  r
) )
123119, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  0  <_  ( c `  r ) )
124123adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  /\  r  e.  R )  ->  0  <_  ( c `  r
) )
125 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  =  t  ->  (
c `  r )  =  ( c `  t ) )
126 simpr 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  t  e.  R )
127113, 121, 124, 125, 126fsumge1 13693 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  <_  sum_ r  e.  R  ( c `  r ) )
128112adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  R  e.  Fin )
129120recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  r  e.  R )  ->  ( c `  r
)  e.  CC )
130128, 129fsumcl 13637 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  R  ( c `  r )  e.  CC )
13163recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  e.  CC )
132130, 131pncand 9923 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ r ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )
134 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ r
( c `  Z
)
13550adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  Z  e.  T )
136 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  -.  Z  e.  R
)
137136adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  -.  Z  e.  R
)
138 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( r  =  Z  ->  (
c `  r )  =  ( c `  Z ) )
139133, 134, 128, 135, 137, 129, 138, 131fsumsplitsn 31810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  ( R  u.  { Z }
) ( c `  r )  =  (
sum_ r  e.  R  ( c `  r
)  +  ( c `
 Z ) ) )
140139eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( sum_ r  e.  R  ( c `  r
)  +  ( c `
 Z ) )  =  sum_ r  e.  ( R  u.  { Z } ) ( c `
 r ) )
141125cbvsumv 13600 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  sum_ r  e.  ( R  u.  { Z } ) ( c `
 r )  = 
sum_ t  e.  ( R  u.  { Z } ) ( c `
 t )
142141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  ( R  u.  { Z }
) ( c `  r )  =  sum_ t  e.  ( R  u.  { Z } ) ( c `  t
) )
14341adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
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 } )
14446, 143eleqtrd 2544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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 } )
145 rabid 3031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) )
146144, 145sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
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 ) )
147146simprd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ t  e.  ( R  u.  { Z }
) ( c `  t )  =  J )
148142, 147eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  ( R  u.  { Z }
) ( c `  r )  =  J )
149140, 148eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( sum_ r  e.  R  ( c `  r
)  +  ( c `
 Z ) )  =  J )
150149oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( sum_ r  e.  R  ( c `  r )  +  ( c `  Z ) )  -  ( c `
 Z ) )  =  ( J  -  ( c `  Z
) ) )
151132, 150eqtr3d 2497 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  R  ( c `  r )  =  ( J  -  ( c `  Z
) ) )
152151adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  -> 
sum_ r  e.  R  ( c `  r
)  =  ( J  -  ( c `  Z ) ) )
153127, 152breqtrd 4463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  <_  ( J  -  ( c `  Z ) ) )
154107, 109, 153jca32 533 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
) ) ) )
155 elfz2 11682 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) ) ) )
156154, 155sylibr 212 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  e.  ( 0 ... ( J  -  ( c `  Z
) ) ) )
15799, 156eqeltrd 2542 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( ( c  |`  R ) `  t
)  e.  ( 0 ... ( J  -  ( c `  Z
) ) ) )
158157ex 432 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( t  e.  R  ->  ( ( c  |`  R ) `  t
)  e.  ( 0 ... ( J  -  ( c `  Z
) ) ) ) )
15997, 158ralrimi 2854 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  A. t  e.  R  ( ( c  |`  R ) `  t
)  e.  ( 0 ... ( J  -  ( c `  Z
) ) ) )
16078, 159jca 530 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( c  |`  R )  Fn  R  /\  A. t  e.  R  ( ( c  |`  R ) `  t
)  e.  ( 0 ... ( J  -  ( c `  Z
) ) ) ) )
161 ffnfv 6033 . . . . . . . . . . . . . . 15  |-  ( ( c  |`  R ) : R --> ( 0 ... ( J  -  (
c `  Z )
) )  <->  ( (
c  |`  R )  Fn  R  /\  A. t  e.  R  ( (
c  |`  R ) `  t )  e.  ( 0 ... ( J  -  ( c `  Z ) ) ) ) )
162160, 161sylibr 212 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c  |`  R ) : R --> ( 0 ... ( J  -  ( c `  Z
) ) ) )
163 ovex 6298 . . . . . . . . . . . . . . . 16  |-  ( 0 ... ( J  -  ( c `  Z
) ) )  e. 
_V
164163a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0 ... ( J  -  ( c `  Z ) ) )  e.  _V )
16520, 110ssexd 4584 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  R  e.  _V )
166165adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  R  e.  _V )
167164, 166elmapd 7426 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( c  |`  R )  e.  ( ( 0 ... ( J  -  ( c `  Z ) ) )  ^m  R )  <->  ( c  |`  R ) : R --> ( 0 ... ( J  -  ( c `  Z ) ) ) ) )
168162, 167mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c  |`  R )  e.  ( ( 0 ... ( J  -  ( c `  Z
) ) )  ^m  R ) )
16998a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( t  e.  R  ->  ( ( c  |`  R ) `  t
)  =  ( c `
 t ) ) )
17097, 169ralrimi 2854 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  A. t  e.  R  ( ( c  |`  R ) `  t
)  =  ( c `
 t ) )
171170sumeq2d 13606 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ t  e.  R  ( ( c  |`  R ) `
 t )  = 
sum_ t  e.  R  ( c `  t
) )
172125cbvsumv 13600 . . . . . . . . . . . . . . . 16  |-  sum_ r  e.  R  ( c `  r )  =  sum_ t  e.  R  (
c `  t )
173172eqcomi 2467 . . . . . . . . . . . . . . 15  |-  sum_ t  e.  R  ( c `  t )  =  sum_ r  e.  R  (
c `  r )
174173a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ t  e.  R  ( c `  t )  =  sum_ r  e.  R  ( c `  r
) )
175151idi 2 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ r  e.  R  ( c `  r )  =  ( J  -  ( c `  Z
) ) )
176171, 174, 1753eqtrd 2499 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  sum_ t  e.  R  ( ( c  |`  R ) `
 t )  =  ( J  -  (
c `  Z )
) )
177168, 176jca 530 . . . . . . . . . . . 12  |-  ( (
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 )
) ) )
178 eqidd 2455 . . . . . . . . . . . . . . 15  |-  ( e  =  ( c  |`  R )  ->  R  =  R )
179 simpl 455 . . . . . . . . . . . . . . . 16  |-  ( ( e  =  ( c  |`  R )  /\  t  e.  R )  ->  e  =  ( c  |`  R ) )
180179fveq1d 5850 . . . . . . . . . . . . . . 15  |-  ( ( e  =  ( c  |`  R )  /\  t  e.  R )  ->  (
e `  t )  =  ( ( c  |`  R ) `  t
) )
181178, 180sumeq12rdv 13611 . . . . . . . . . . . . . 14  |-  ( e  =  ( c  |`  R )  ->  sum_ t  e.  R  ( e `  t )  =  sum_ t  e.  R  (
( c  |`  R ) `
 t ) )
182181eqeq1d 2456 . . . . . . . . . . . . 13  |-  ( e  =  ( c  |`  R )  ->  ( sum_ t  e.  R  ( e `  t )  =  ( J  -  ( c `  Z
) )  <->  sum_ t  e.  R  ( ( c  |`  R ) `  t
)  =  ( J  -  ( c `  Z ) ) ) )
183182elrab 3254 . . . . . . . . . . . 12  |-  ( ( 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 )
) ) )
184177, 183sylibr 212 . . . . . . . . . . 11  |-  ( (
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 ) ) } )
185 oveq2 6278 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  R  ->  (
( 0 ... n
)  ^m  s )  =  ( ( 0 ... n )  ^m  R ) )
186 rabeq 3100 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 }
)
187185, 186syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 }
)
188 sumeq1 13593 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  R  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  R  (
c `  t )
)
189188eqeq1d 2456 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  R  ->  ( sum_ t  e.  s  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  n ) )
190189rabbidv 3098 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 }
)
191187, 190eqtrd 2495 . . . . . . . . . . . . . . . . . 18  |-  ( 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 }
)
192191mpteq2dv 4526 . . . . . . . . . . . . . . . . 17  |-  ( 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 }
) )
193192adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  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 }
) )
194 elpwg 4007 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  _V  ->  ( R  e.  ~P T  <->  R 
C_  T ) )
195165, 194syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( R  e.  ~P T 
<->  R  C_  T )
)
196110, 195mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  R  e.  ~P T
)
19726mptex 6118 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  R )  |  sum_ t  e.  R  (
c `  t )  =  n } )  e. 
_V
198197a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  R )  |  sum_ t  e.  R  ( c `  t
)  =  n }
)  e.  _V )
1999, 193, 196, 198fvmptd 5936 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( C `  R
)  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  R )  |  sum_ t  e.  R  (
c `  t )  =  n } ) )
200199adantr 463 . . . . . . . . . . . . . 14  |-  ( (
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 } ) )
201 oveq2 6278 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
0 ... n )  =  ( 0 ... m
) )
202201oveq1d 6285 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (
( 0 ... n
)  ^m  R )  =  ( ( 0 ... m )  ^m  R ) )
203 rabeq 3100 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 }
)
204202, 203syl 16 . . . . . . . . . . . . . . . . 17  |-  ( 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 }
)
205 eqeq2 2469 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  ( sum_ t  e.  R  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  m ) )
206205rabbidv 3098 . . . . . . . . . . . . . . . . 17  |-  ( 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 }
)
207204, 206eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( 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 }
)
208207cbvmptv 4530 . . . . . . . . . . . . . . 15  |-  ( 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 }
)
209208a1i 11 . . . . . . . . . . . . . 14  |-  ( (
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 } ) )
210200, 209eqtrd 2495 . . . . . . . . . . . . 13  |-  ( (
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 } ) )
211 fveq1 5847 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  e  ->  (
c `  t )  =  ( e `  t ) )
212211sumeq2ad 31805 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  e  ->  sum_ t  e.  R  ( c `  t )  =  sum_ t  e.  R  (
e `  t )
)
213212eqeq1d 2456 . . . . . . . . . . . . . . . . 17  |-  ( c  =  e  ->  ( sum_ t  e.  R  ( c `  t )  =  m  <->  sum_ t  e.  R  ( e `  t )  =  m ) )
214213cbvrabv 3105 . . . . . . . . . . . . . . . 16  |-  { 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 }
215214a1i 11 . . . . . . . . . . . . . . 15  |-  ( 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 }
)
216 oveq2 6278 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( J  -  ( c `  Z
) )  ->  (
0 ... m )  =  ( 0 ... ( J  -  ( c `  Z ) ) ) )
217216oveq1d 6285 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( J  -  ( c `  Z
) )  ->  (
( 0 ... m
)  ^m  R )  =  ( ( 0 ... ( J  -  ( c `  Z
) ) )  ^m  R ) )
218 rabeq 3100 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 }
)
219217, 218syl 16 . . . . . . . . . . . . . . 15  |-  ( 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 }
)
220 eqeq2 2469 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( J  -  ( c `  Z
) )  ->  ( sum_ t  e.  R  ( e `  t )  =  m  <->  sum_ t  e.  R  ( e `  t )  =  ( J  -  ( c `
 Z ) ) ) )
221220rabbidv 3098 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) } )
222215, 219, 2213eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( 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 ) ) } )
223222adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) } )
22458, 65jca 530 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( J  -  ( c `  Z
) )  e.  ZZ  /\  0  <_  ( J  -  ( c `  Z ) ) ) )
225 elnn0z 10873 . . . . . . . . . . . . . 14  |-  ( ( J  -  ( c `
 Z ) )  e.  NN0  <->  ( ( J  -  ( c `  Z ) )  e.  ZZ  /\  0  <_ 
( J  -  (
c `  Z )
) ) )
226224, 225sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  e.  NN0 )
227 ovex 6298 . . . . . . . . . . . . . . 15  |-  ( ( 0 ... ( J  -  ( c `  Z ) ) )  ^m  R )  e. 
_V
228227rabex 4588 . . . . . . . . . . . . . 14  |-  { e  e.  ( ( 0 ... ( J  -  ( c `  Z
) ) )  ^m  R )  |  sum_ t  e.  R  (
e `  t )  =  ( J  -  ( c `  Z
) ) }  e.  _V
229228a1i 11 . . . . . . . . . . . . 13  |-  ( (
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 )
230210, 223, 226, 229fvmptd 5936 . . . . . . . . . . . 12  |-  ( (
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 ) ) } )
231230eqcomd 2462 . . . . . . . . . . 11  |-  ( (
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 )
) ) )
232184, 231eleqtrd 2544 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c  |`  R )  e.  ( ( C `
 R ) `  ( J  -  (
c `  Z )
) ) )
23372, 232jca 530 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( J  -  ( c `  Z
) )  e.  ( 0 ... J )  /\  ( c  |`  R )  e.  ( ( C `  R
) `  ( J  -  ( c `  Z ) ) ) ) )
2341, 233jca 530 . . . . . . . 8  |-  ( (
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 ) ) ) ) ) )
235232elfvexd 5876 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  e.  _V )
236 vex 3109 . . . . . . . . . . 11  |-  c  e. 
_V
237236resex 5305 . . . . . . . . . 10  |-  ( c  |`  R )  e.  _V
238237a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c  |`  R )  e.  _V )
239 opeq12 4205 . . . . . . . . . . . 12  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  ->  <. k ,  d >.  =  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. )
240239eqeq2d 2468 . . . . . . . . . . 11  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  -> 
( <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >.  =  <. k ,  d
>. 
<-> 
<. ( J  -  (
c `  Z )
) ,  ( c  |`  R ) >.  =  <. ( J  -  ( c `
 Z ) ) ,  ( c  |`  R ) >. )
)
241 eleq1 2526 . . . . . . . . . . . . 13  |-  ( k  =  ( J  -  ( c `  Z
) )  ->  (
k  e.  ( 0 ... J )  <->  ( J  -  ( c `  Z ) )  e.  ( 0 ... J
) ) )
242241adantr 463 . . . . . . . . . . . 12  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  -> 
( k  e.  ( 0 ... J )  <-> 
( J  -  (
c `  Z )
)  e.  ( 0 ... J ) ) )
243 simpr 459 . . . . . . . . . . . . 13  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  -> 
d  =  ( c  |`  R ) )
244 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( k  =  ( J  -  ( c `  Z
) )  ->  (
( C `  R
) `  k )  =  ( ( C `
 R ) `  ( J  -  (
c `  Z )
) ) )
245244adantr 463 . . . . . . . . . . . . 13  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  -> 
( ( C `  R ) `  k
)  =  ( ( C `  R ) `
 ( J  -  ( c `  Z
) ) ) )
246243, 245eleq12d 2536 . . . . . . . . . . . 12  |-  ( ( k  =  ( J  -  ( c `  Z ) )  /\  d  =  ( c  |`  R ) )  -> 
( d  e.  ( ( C `  R
) `  k )  <->  ( c  |`  R )  e.  ( ( C `  R ) `  ( J  -  ( c `  Z ) ) ) ) )
247242, 246anbi12d 708 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) ) )
248240, 247anbi12d 708 . . . . . . . . . 10  |-  ( ( 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 ) ) ) ) ) ) )
249248spc2egv 3193 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
250235, 238, 249syl2anc 659 . . . . . . . 8  |-  ( (
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 ) ) ) ) )
251234, 250mpd 15 . . . . . . 7  |-  ( (
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 ) ) ) )
252 eliunxp 5129 . . . . . . 7  |-  ( <.
( 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 ) ) ) )
253251, 252sylibr 212 . . . . . 6  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  <. ( J  -  (
c `  Z )
) ,  ( c  |`  R ) >.  e.  U_ k  e.  ( 0 ... J ) ( { k }  X.  ( ( C `  R ) `  k
) ) )
254 dvnprodlem1.d . . . . . 6  |-  D  =  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  |->  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>. )
255253, 254fmptd 6031 . . . . 5  |-  ( ph  ->  D : ( ( C `  ( R  u.  { Z }
) ) `  J
) --> U_ k  e.  ( 0 ... J ) ( { k }  X.  ( ( C `
 R ) `  k ) ) )
25695nfcri 2609 . . . . . . . . . . . 12  |-  F/ t  e  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
)
25796, 256nfan 1933 . . . . . . . . . . 11  |-  F/ t ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )
25879, 257nfan 1933 . . . . . . . . . 10  |-  F/ t ( ph  /\  (
c  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
)  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )
259 nfv 1712 . . . . . . . . . 10  |-  F/ t ( D `  c
)  =  ( D `
 e )
260258, 259nfan 1933 . . . . . . . . 9  |-  F/ t ( ( ph  /\  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  /\  ( D `  c )  =  ( D `  e ) )
26199eqcomd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  t  e.  R )  ->  ( c `  t
)  =  ( ( c  |`  R ) `  t ) )
262261adantlrr 718 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
c  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
)  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  /\  t  e.  R
)  ->  ( c `  t )  =  ( ( c  |`  R ) `
 t ) )
263262adantlr 712 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) )
264254a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  =  ( c  e.  ( ( C `
 ( R  u.  { Z } ) ) `
 J )  |->  <.
( J  -  (
c `  Z )
) ,  ( c  |`  R ) >. )
)
265 opex 4701 . . . . . . . . . . . . . . . . . . . 20  |-  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>.  e.  _V
266265a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  <. ( J  -  (
c `  Z )
) ,  ( c  |`  R ) >.  e.  _V )
267264, 266fvmpt2d 5941 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( D `  c
)  =  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>. )
268267fveq2d 5852 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 2nd `  ( D `  c )
)  =  ( 2nd `  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. ) )
269268fveq1d 5850 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( 2nd `  ( D `  c )
) `  t )  =  ( ( 2nd `  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. ) `  t ) )
270 ovex 6298 . . . . . . . . . . . . . . . . . . 19  |-  ( J  -  ( c `  Z ) )  e. 
_V
271270, 237op2nd 6782 . . . . . . . . . . . . . . . . . 18  |-  ( 2nd `  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. )  =  ( c  |`  R )
272271fveq1i 5849 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>. ) `  t )  =  ( ( c  |`  R ) `  t
)
273272a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( 2nd `  <. ( J  -  ( c `
 Z ) ) ,  ( c  |`  R ) >. ) `  t )  =  ( ( c  |`  R ) `
 t ) )
274269, 273eqtr2d 2496 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( ( c  |`  R ) `  t
)  =  ( ( 2nd `  ( D `
 c ) ) `
 t ) )
275274adantrr 714 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  ->  ( ( c  |`  R ) `  t
)  =  ( ( 2nd `  ( D `
 c ) ) `
 t ) )
276275ad2antrr 723 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
)
277 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( D `  c
)  =  ( D `
 e ) )
278254a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  D  =  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  |->  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>. ) )
279 fveq1 5847 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  e  ->  (
c `  Z )  =  ( e `  Z ) )
280279oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  e  ->  ( J  -  ( c `  Z ) )  =  ( J  -  (
e `  Z )
) )
281 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  e  ->  (
c  |`  R )  =  ( e  |`  R ) )
282280, 281opeq12d 4211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  e  ->  <. ( J  -  ( c `  Z ) ) ,  ( c  |`  R )
>.  =  <. ( J  -  ( e `  Z ) ) ,  ( e  |`  R )
>. )
283282adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  c  =  e )  -> 
<. ( J  -  (
c `  Z )
) ,  ( c  |`  R ) >.  =  <. ( J  -  ( e `
 Z ) ) ,  ( e  |`  R ) >. )
284 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
e  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
) )
285 opex 4701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  <. ( J  -  ( e `  Z ) ) ,  ( e  |`  R )
>.  e.  _V
286285a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  <. ( J  -  (
e `  Z )
) ,  ( e  |`  R ) >.  e.  _V )
287278, 283, 284, 286fvmptd 5936 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( D `  e
)  =  <. ( J  -  ( e `  Z ) ) ,  ( e  |`  R )
>. )
288287adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( D `  e
)  =  <. ( J  -  ( e `  Z ) ) ,  ( e  |`  R )
>. )
289277, 288eqtrd 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( D `  c
)  =  <. ( J  -  ( e `  Z ) ) ,  ( e  |`  R )
>. )
290289fveq2d 5852 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( 2nd `  ( D `  c )
)  =  ( 2nd `  <. ( J  -  ( e `  Z
) ) ,  ( e  |`  R ) >. ) )
291290adantlrl 717 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
>. ) )
292291adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) >. )
)
293 ovex 6298 . . . . . . . . . . . . . . . . . 18  |-  ( J  -  ( e `  Z ) )  e. 
_V
294 vex 3109 . . . . . . . . . . . . . . . . . . 19  |-  e  e. 
_V
295294resex 5305 . . . . . . . . . . . . . . . . . 18  |-  ( e  |`  R )  e.  _V
296293, 295op2nd 6782 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  <. ( J  -  ( e `  Z
) ) ,  ( e  |`  R ) >. )  =  ( e  |`  R )
297296a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
298292, 297eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
299298fveq1d 5850 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) )
300 fvres 5862 . . . . . . . . . . . . . . 15  |-  ( t  e.  R  ->  (
( e  |`  R ) `
 t )  =  ( e `  t
) )
301300adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) )
302299, 301eqtrd 2495 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
303263, 276, 3023eqtrd 2499 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
304303adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
305 simpl 455 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 } ) ) )
306 elunnel1 31654 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( R  u.  { Z }
)  /\  -.  t  e.  R )  ->  t  e.  { Z } )
307 elsni 4041 . . . . . . . . . . . . . 14  |-  ( t  e.  { Z }  ->  t  =  Z )
308306, 307syl 16 . . . . . . . . . . . . 13  |-  ( ( t  e.  ( R  u.  { Z }
)  /\  -.  t  e.  R )  ->  t  =  Z )
309308adantll 711 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
310 simpr 459 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  /\  ( D `  c )  =  ( D `  e ) )  /\  t  =  Z )  ->  t  =  Z )
311310fveq2d 5852 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
3123nn0cnd 10850 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  J  e.  CC )
313312adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  J  e.  CC )
314313, 131nncand 9927 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  ( J  -  ( c `  Z ) ) )  =  ( c `  Z ) )
315314eqcomd 2462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( c `  Z
)  =  ( J  -  ( J  -  ( c `  Z
) ) ) )
316315adantrr 714 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  ->  ( c `  Z )  =  ( J  -  ( J  -  ( c `  Z ) ) ) )
317316adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
318267fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 1st `  ( D `  c )
)  =  ( 1st `  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. ) )
319270, 237op1st 6781 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1st `  <. ( J  -  ( c `  Z
) ) ,  ( c  |`  R ) >. )  =  ( J  -  ( c `  Z ) )
320319a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 1st `  <. ( J  -  ( c `
 Z ) ) ,  ( c  |`  R ) >. )  =  ( J  -  ( c `  Z
) ) )
321318, 320eqtr2d 2496 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  (
c `  Z )
)  =  ( 1st `  ( D `  c
) ) )
322321oveq2d 6286 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  ( J  -  ( c `  Z ) ) )  =  ( J  -  ( 1st `  ( D `
 c ) ) ) )
323322adantrr 714 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J )  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )  ->  ( J  -  ( J  -  (
c `  Z )
) )  =  ( J  -  ( 1st `  ( D `  c
) ) ) )
324323adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
325 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D `  c )  =  ( D `  e )  ->  ( 1st `  ( D `  c ) )  =  ( 1st `  ( D `  e )
) )
326325adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( 1st `  ( D `  c )
)  =  ( 1st `  ( D `  e
) ) )
327287fveq2d 5852 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 1st `  ( D `  e )
)  =  ( 1st `  <. ( J  -  ( e `  Z
) ) ,  ( e  |`  R ) >. ) )
328327adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( 1st `  ( D `  e )
)  =  ( 1st `  <. ( J  -  ( e `  Z
) ) ,  ( e  |`  R ) >. ) )
329293, 295op1st 6781 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1st `  <. ( J  -  ( e `  Z
) ) ,  ( e  |`  R ) >. )  =  ( J  -  ( e `  Z ) )
330329a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( 1st `  <. ( J  -  ( e `
 Z ) ) ,  ( e  |`  R ) >. )  =  ( J  -  ( e `  Z
) ) )
331326, 328, 3303eqtrd 2499 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( 1st `  ( D `  c )
)  =  ( J  -  ( e `  Z ) ) )
332331oveq2d 6286 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( J  -  ( 1st `  ( D `  c ) ) )  =  ( J  -  ( J  -  (
e `  Z )
) ) )
333312adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  J  e.  CC )
334 zsscn 10868 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ZZ  C_  CC
3356, 334sstri 3498 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 ... J )  C_  CC
336335a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( 0 ... J
)  C_  CC )
337 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  e  ->  (
c  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
)  <->  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) ) )
338337anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  e  ->  (
( ph  /\  c  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  <->  ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z }
) ) `  J
) ) ) )
339 feq1 5695 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  e  ->  (
c : ( R  u.  { Z }
) --> ( 0 ... J )  <->  e :
( R  u.  { Z } ) --> ( 0 ... J ) ) )
340338, 339imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) )
341340, 49chvarv 2019 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
e : ( R  u.  { Z }
) --> ( 0 ... J ) )
34254adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  ->  Z  e.  ( R  u.  { Z } ) )
343341, 342ffvelrnd 6008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( e `  Z
)  e.  ( 0 ... J ) )
344336, 343sseldd 3490 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( e `  Z
)  e.  CC )
345333, 344nncand 9927 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  -> 
( J  -  ( J  -  ( e `  Z ) ) )  =  ( e `  Z ) )
346345adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( J  -  ( J  -  ( e `  Z ) ) )  =  ( e `  Z ) )
347 eqidd 2455 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( e `  Z
)  =  ( e `
 Z ) )
348332, 346, 3473eqtrd 2499 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  e  e.  ( ( C `  ( R  u.  { Z } ) ) `  J ) )  /\  ( D `  c )  =  ( D `  e ) )  -> 
( J  -  ( 1st `  ( D `  c ) ) )  =  ( e `  Z ) )
349348adantlrl 717 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
350317, 324, 3493eqtrd 2499 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
c  e.  (