dvnprodlem1

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

Proof

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

Metamath Proof Explorer

Theorem dvnprodlem1

Proof