Theorem dvnprodlem1 40161

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.

Step	Hyp	Ref	Expression
1		eqidd 2623	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
2		0zd 11389	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 e. ZZ )
3		dvnprodlem1.j	. . . . . . . . . . . . . . 15 |- ( ph -> J e. NN0 )
4	3	nn0zd 11480	. . . . . . . . . . . . . 14 |- ( ph -> J e. ZZ )
5	4	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. ZZ )
6		fzssz 12343	. . . . . . . . . . . . . . . 16 |- ( 0 ... J ) C_ ZZ
7	6	a1i 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 } ) )
9	8	a1i 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 6658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = ( R u. { Z } ) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) )
11		rabeq 3192	. . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
12	10, 11	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 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 14419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = ( R u. { Z } ) -> sum_ t e. s ( c ` t ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
14	13	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = ( R u. { Z } ) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = n ) )
15	14	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . 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 } )
16	12, 15	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 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 } )
17	16	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . 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 } ) )
18	17	adantl 482	. . . . . . . . . . . . . . . . . . . . . 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 4804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( R u. { Z } ) C_ T /\ T e. Fin ) -> ( R u. { Z } ) e. _V )
22	19, 20, 21	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( R u. { Z } ) e. _V )
23		elpwg 4166	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( R u. { Z } ) e. _V -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
24	22, 23	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
25	19, 24	mpbird 247	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( R u. { Z } ) e. ~P T )
26		nn0ex 11298	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
27	26	mptex 6486	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V
28	27	a1i 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 )
29	9, 18, 25, 28	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . 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 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = J -> ( 0 ... n ) = ( 0 ... J ) )
31	30	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = J -> ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
32		rabeq 3192	. . . . . . . . . . . . . . . . . . . . . . . 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 } )
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . 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 2633	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = J -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
35	34	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . 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 } )
36	33, 35	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 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 } )
37	36	adantl 482	. . . . . . . . . . . . . . . . . . . . 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 6678	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. _V
39	38	rabex 4813	. . . . . . . . . . . . . . . . . . . . . 22 |- { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V
40	39	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V )
41	29, 37, 3, 40	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 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 3687	. . . . . . . . . . . . . . . . . . . . 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 } ) )
43	42	a1i 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 } ) ) )
44	41, 43	eqsstrd 3639	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
45	44	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
46		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
47	45, 46	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
48		elmapi 7879	. . . . . . . . . . . . . . . . 17 |- ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
49	47, 48	syl 17	. . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . 19 |- ( Z e. T -> Z e. { Z } )
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Z e. { Z } )
53		elun2 3781	. . . . . . . . . . . . . . . . . 18 |- ( Z e. { Z } -> Z e. ( R u. { Z } ) )
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> Z e. ( R u. { Z } ) )
55	54	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
56	49, 55	ffvelrnd 6360	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... J ) )
57	7, 56	sseldd 3604	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ZZ )
58	5, 57	zsubcld 11487	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ZZ )
59	2, 5, 58	3jca 1242	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) )
60		elfzle2 12345	. . . . . . . . . . . . . 14 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) <_ J )
61	56, 60	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) <_ J )
62	5	zred 11482	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. RR )
63	57	zred 11482	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. RR )
64	62, 63	subge0d 10617	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( J - ( c ` Z ) ) <-> ( c ` Z ) <_ J ) )
65	61, 64	mpbird 247	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( J - ( c ` Z ) ) )
66		elfzle1 12344	. . . . . . . . . . . . . 14 |- ( ( c ` Z ) e. ( 0 ... J ) -> 0 <_ ( c ` Z ) )
67	56, 66	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( c ` Z ) )
68	62, 63	subge02d 10619	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( c ` Z ) <-> ( J - ( c ` Z ) ) <_ J ) )
69	67, 68	mpbid 222	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) <_ J )
70	59, 65, 69	jca32 558	. . . . . . . . . . 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 12333	. . . . . . . . . . 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 ) ) )
72	70, 71	sylibr 224	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
73		elmapfn 7880	. . . . . . . . . . . . . . . . . 18 |- ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c Fn ( R u. { Z } ) )
74	47, 73	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c Fn ( R u. { Z } ) )
75		ssun1 3776	. . . . . . . . . . . . . . . . . 18 |- R C_ ( R u. { Z } )
76	75	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R C_ ( R u. { Z } ) )
77		fnssres 6004	. . . . . . . . . . . . . . . . 17 |- ( ( c Fn ( R u. { Z } ) /\ R C_ ( R u. { Z } ) ) -> ( c |` R ) Fn R )
78	74, 76, 77	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) Fn R )
79		nfv 1843	. . . . . . . . . . . . . . . . . 18 |- F/ t ph
80		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ t c
81		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ~P T
82		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t NN0
83		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F/_ t s
84	83	nfsum1 14420	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ t sum_ t e. s ( c ` t )
85		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ t n
86	84, 85	nfeq 2776	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ t sum_ t e. s ( c ` t ) = n
87		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ t ( ( 0 ... n ) ^m s )
88	86, 87	nfrab 3123	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n }
89	82, 88	nfmpt 4746	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } )
90	81, 89	nfmpt 4746	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ t ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
91	8, 90	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t C
92		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t ( R u. { Z } )
93	91, 92	nffv 6198	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t ( C ` ( R u. { Z } ) )
94		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t J
95	93, 94	nffv 6198	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( ( C ` ( R u. { Z } ) ) ` J )
96	80, 95	nfel 2777	. . . . . . . . . . . . . . . . . 18 |- F/ t c e. ( ( C ` ( R u. { Z } ) ) ` J )
97	79, 96	nfan 1828	. . . . . . . . . . . . . . . . 17 |- F/ t ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
98		fvres 6207	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) )
99	98	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( c ` t ) )
100	2	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 e. ZZ )
101	58	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( J - ( c ` Z ) ) e. ZZ )
102	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( 0 ... J ) C_ ZZ )
103	49	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
104	76	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. ( R u. { Z } ) )
105	103, 104	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... J ) )
106	102, 105	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ZZ )
107	100, 101, 106	3jca 1242	. . . . . . . . . . . . . . . . . . . . 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 12344	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( c ` t ) e. ( 0 ... J ) -> 0 <_ ( c ` t ) )
109	105, 108	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 <_ ( c ` t ) )
110	19	unssad 3790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> R C_ T )
111		ssfi 8180	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
112	20, 110, 111	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> R e. Fin )
113	112	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> R e. Fin )
114		zssre 11384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ZZ C_ RR
115	6, 114	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 0 ... J ) C_ RR
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( 0 ... J ) C_ RR )
117	49	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
118	76	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> r e. ( R u. { Z } ) )
119	117, 118	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. ( 0 ... J ) )
120	116, 119	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. RR )
121	120	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> ( c ` r ) e. RR )
122		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` r ) e. ( 0 ... J ) -> 0 <_ ( c ` r ) )
123	119, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> 0 <_ ( c ` r ) )
124	123	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> 0 <_ ( c ` r ) )
125		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( r = t -> ( c ` r ) = ( c ` t ) )
126		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. R )
127	113, 121, 124, 125, 126	fsumge1 14529	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ sum_ r e. R ( c ` r ) )
128	112	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
129	120	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. CC )
130	128, 129	fsumcl 14464	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) e. CC )
131	63	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. CC )
132	130, 131	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . . 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 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F/ r ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
134		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F/_ r ( c ` Z )
135	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
136		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> -. Z e. R )
137	136	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
138		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( r = Z -> ( c ` r ) = ( c ` Z ) )
139	133, 134, 128, 135, 137, 129, 138, 131	fsumsplitsn 14474	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
140	139	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
141	125	cbvsumv 14426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- sum_ r e. ( R u. { Z } ) ( c ` r ) = sum_ t e. ( R u. { Z } ) ( c ` t )
142	141	a1i 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 ) )
143	41	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
144	46, 143	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
146	144, 145	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
147	146	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = J )
148	142, 147	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = J )
149	140, 148	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = J )
150	149	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) - ( c ` Z ) ) = ( J - ( c ` Z ) ) )
151	132, 150	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
152	151	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
153	127, 152	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ ( J - ( c ` Z ) ) )
154	107, 109, 153	jca32 558	. . . . . . . . . . . . . . . . . . . 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 12333	. . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
156	154, 155	sylibr 224	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
157	99, 156	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
158	157	ex 450	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
159	97, 158	ralrimi 2957	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
160	78, 159	jca 554	. . . . . . . . . . . . . . 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 6388	. . . . . . . . . . . . . . 15 |- ( ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) <-> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
162	160, 161	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) )
163		ovexd 6680	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... ( J - ( c ` Z ) ) ) e. _V )
164	20, 110	ssexd 4805	. . . . . . . . . . . . . . . 16 |- ( ph -> R e. _V )
165	164	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. _V )
166	163, 165	elmapd 7871	. . . . . . . . . . . . . 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 ) ) ) ) )
167	162, 166	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
168	98	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) ) )
169	97, 168	ralrimi 2957	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) = ( c ` t ) )
170	169	sumeq2d 14432	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = sum_ t e. R ( c ` t ) )
171	125	cbvsumv 14426	. . . . . . . . . . . . . . . 16 |- sum_ r e. R ( c ` r ) = sum_ t e. R ( c ` t )
172	171	eqcomi 2631	. . . . . . . . . . . . . . 15 |- sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r )
173	172	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r ) )
174	151	idi 2	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
175	170, 173, 174	3eqtrd 2660	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) )
176	167, 175	jca 554	. . . . . . . . . . . 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 ) ) ) )
177		eqidd 2623	. . . . . . . . . . . . . . 15 |- ( e = ( c |` R ) -> R = R )
178		simpl 473	. . . . . . . . . . . . . . . 16 |- ( ( e = ( c |` R ) /\ t e. R ) -> e = ( c |` R ) )
179	178	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ( e = ( c |` R ) /\ t e. R ) -> ( e ` t ) = ( ( c |` R ) ` t ) )
180	177, 179	sumeq12rdv 14438	. . . . . . . . . . . . . 14 |- ( e = ( c |` R ) -> sum_ t e. R ( e ` t ) = sum_ t e. R ( ( c |` R ) ` t ) )
181	180	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( e = ( c |` R ) -> ( sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) <-> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
182	181	elrab 3363	. . . . . . . . . . . 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 ) ) ) )
183	176, 182	sylibr 224	. . . . . . . . . . 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 ) ) } )
184		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
185		rabeq 3192	. . . . . . . . . . . . . . . . . . . 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 } )
186	184, 185	syl 17	. . . . . . . . . . . . . . . . . . 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 } )
187		sumeq1 14419	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
188	187	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . 20 |- ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
189	188	rabbidv 3189	. . . . . . . . . . . . . . . . . . 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 } )
190	186, 189	eqtrd 2656	. . . . . . . . . . . . . . . . . 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 } )
191	190	mpteq2dv 4745	. . . . . . . . . . . . . . . . 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 } ) )
192	191	adantl 482	. . . . . . . . . . . . . . . 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 } ) )
193		elpwg 4166	. . . . . . . . . . . . . . . . . 18 |- ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
194	164, 193	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( R e. ~P T <-> R C_ T ) )
195	110, 194	mpbird 247	. . . . . . . . . . . . . . . 16 |- ( ph -> R e. ~P T )
196	26	mptex 6486	. . . . . . . . . . . . . . . . 17 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
197	196	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
198	9, 192, 195, 197	fvmptd 6288	. . . . . . . . . . . . . . 15 |- ( ph -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
199	198	adantr 481	. . . . . . . . . . . . . 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 } ) )
200		oveq2 6658	. . . . . . . . . . . . . . . . . . 19 |- ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
201	200	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) )
202		rabeq 3192	. . . . . . . . . . . . . . . . . 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 } )
203	201, 202	syl 17	. . . . . . . . . . . . . . . . 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 } )
204		eqeq2 2633	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = m ) )
205	204	rabbidv 3189	. . . . . . . . . . . . . . . . 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 } )
206	203, 205	eqtrd 2656	. . . . . . . . . . . . . . . 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 } )
207	206	cbvmptv 4750	. . . . . . . . . . . . . . 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 } )
208	207	a1i 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 } ) )
209	199, 208	eqtrd 2656	. . . . . . . . . . . . 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 } ) )
210		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 |- ( c = e -> ( c ` t ) = ( e ` t ) )
211	210	sumeq2ad 14434	. . . . . . . . . . . . . . . . . 18 |- ( c = e -> sum_ t e. R ( c ` t ) = sum_ t e. R ( e ` t ) )
212	211	eqeq1d 2624	. . . . . . . . . . . . . . . . 17 |- ( c = e -> ( sum_ t e. R ( c ` t ) = m <-> sum_ t e. R ( e ` t ) = m ) )
213	212	cbvrabv 3199	. . . . . . . . . . . . . . . 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 }
214	213	a1i 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 } )
215		oveq2 6658	. . . . . . . . . . . . . . . . 17 |- ( m = ( J - ( c ` Z ) ) -> ( 0 ... m ) = ( 0 ... ( J - ( c ` Z ) ) ) )
216	215	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( m = ( J - ( c ` Z ) ) -> ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
217		rabeq 3192	. . . . . . . . . . . . . . . 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 } )
218	216, 217	syl 17	. . . . . . . . . . . . . . 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 } )
219		eqeq2 2633	. . . . . . . . . . . . . . . 16 |- ( m = ( J - ( c ` Z ) ) -> ( sum_ t e. R ( e ` t ) = m <-> sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) ) )
220	219	rabbidv 3189	. . . . . . . . . . . . . . 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 ) ) } )
221	214, 218, 220	3eqtrd 2660	. . . . . . . . . . . . . 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 ) ) } )
222	221	adantl 482	. . . . . . . . . . . . 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 ) ) } )
223	58, 65	jca 554	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
224		elnn0z 11390	. . . . . . . . . . . . . 14 |- ( ( J - ( c ` Z ) ) e. NN0 <-> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
225	223, 224	sylibr 224	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. NN0 )
226		ovex 6678	. . . . . . . . . . . . . . 15 |- ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) e. _V
227	226	rabex 4813	. . . . . . . . . . . . . 14 |- { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } e. _V
228	227	a1i 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 )
229	209, 222, 225, 228	fvmptd 6288	. . . . . . . . . . . 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 ) ) } )
230	229	eqcomd 2628	. . . . . . . . . . 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 ) ) ) )
231	183, 230	eleqtrd 2703	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
232	72, 231	jca 554	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
233	1, 232	jca 554	. . . . . . . 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 ) ) ) ) ) )
234		ovexd 6680	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. _V )
235		vex 3203	. . . . . . . . . . 11 |- c e. _V
236	235	resex 5443	. . . . . . . . . 10 |- ( c |` R ) e. _V
237	236	a1i 11	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. _V )
238		opeq12 4404	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> <. k , d >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
239	238	eqeq2d 2632	. . . . . . . . . . 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 ) >. ) )
240		eleq1 2689	. . . . . . . . . . . . 13 |- ( k = ( J - ( c ` Z ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
241	240	adantr 481	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
242		simpr 477	. . . . . . . . . . . . 13 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> d = ( c |` R ) )
243		fveq2 6191	. . . . . . . . . . . . . 14 |- ( k = ( J - ( c ` Z ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
244	243	adantr 481	. . . . . . . . . . . . 13 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
245	242, 244	eleq12d 2695	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( d e. ( ( C ` R ) ` k ) <-> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
246	241, 245	anbi12d 747	. . . . . . . . . . 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 ) ) ) ) ) )
247	239, 246	anbi12d 747	. . . . . . . . . 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 ) ) ) ) ) ) )
248	247	spc2egv 3295	. . . . . . . . 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 ) ) ) ) )
249	234, 237, 248	syl2anc 693	. . . . . . . 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 ) ) ) ) )
250	233, 249	mpd 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 ) ) ) )
251		eliunxp 5259	. . . . . . 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 ) ) ) )
252	250, 251	sylibr 224	. . . . . 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 ) ) )
253		dvnprodlem1.d	. . . . . 6 |- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
254	252, 253	fmptd 6385	. . . . 5 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
255	95	nfcri 2758	. . . . . . . . . . . 12 |- F/ t e e. ( ( C ` ( R u. { Z } ) ) ` J )
256	96, 255	nfan 1828	. . . . . . . . . . 11 |- F/ t ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
257	79, 256	nfan 1828	. . . . . . . . . 10 |- F/ t ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
258		nfv 1843	. . . . . . . . . 10 |- F/ t ( D ` c ) = ( D ` e )
259	257, 258	nfan 1828	. . . . . . . . 9 |- F/ t ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) )
260	99	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
261	260	adantlrr 757	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
262	261	adantlr 751	. . . . . . . . . . . . 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 ) )
263	253	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
264		opex 4932	. . . . . . . . . . . . . . . . . . . 20 |- <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V
265	264	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V )
266	263, 265	fvmpt2d 6293	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
267	266	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
268	267	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) )
269		ovex 6678	. . . . . . . . . . . . . . . . . . 19 |- ( J - ( c ` Z ) ) e. _V
270	269, 236	op2nd 7177	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( c |` R )
271	270	fveq1i 6192	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t )
272	271	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t ) )
273	268, 272	eqtr2d 2657	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
274	273	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
275	274	ad2antrr 762	. . . . . . . . . . . . 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 ) )
276		simpr 477	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = ( D ` e ) )
277	253	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
278		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c = e -> ( c ` Z ) = ( e ` Z ) )
279	278	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( J - ( c ` Z ) ) = ( J - ( e ` Z ) ) )
280		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( c |` R ) = ( e |` R ) )
281	279, 280	opeq12d 4410	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = e -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
282	281	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ c = e ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
283		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
284		opex 4932	. . . . . . . . . . . . . . . . . . . . . . 23 |- <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V
285	284	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V )
286	277, 282, 283, 285	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
287	286	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
288	276, 287	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
289	288	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
290	289	adantlrl 756	. . . . . . . . . . . . . . . . 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 ) >. ) )
291	290	adantr 481	. . . . . . . . . . . . . . . 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 ) >. ) )
292		ovex 6678	. . . . . . . . . . . . . . . . . 18 |- ( J - ( e ` Z ) ) e. _V
293		vex 3203	. . . . . . . . . . . . . . . . . . 19 |- e e. _V
294	293	resex 5443	. . . . . . . . . . . . . . . . . 18 |- ( e |` R ) e. _V
295	292, 294	op2nd 7177	. . . . . . . . . . . . . . . . 17 |- ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( e |` R )
296	295	a1i 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 ) )
297	291, 296	eqtrd 2656	. . . . . . . . . . . . . . 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 ) )
298	297	fveq1d 6193	. . . . . . . . . . . . . 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 ) )
299		fvres 6207	. . . . . . . . . . . . . . 15 |- ( t e. R -> ( ( e |` R ) ` t ) = ( e ` t ) )
300	299	adantl 482	. . . . . . . . . . . . . 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 ) )
301	298, 300	eqtrd 2656	. . . . . . . . . . . . 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 ) )
302	262, 275, 301	3eqtrd 2660	. . . . . . . . . . . 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 ) )
303	302	adantlr 751	. . . . . . . . . . 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 ) )
304		simpl 473	. . . . . . . . . . . 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 } ) ) )
305		elunnel1 3754	. . . . . . . . . . . . . 14 |- ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t e. { Z } )
306		elsni 4194	. . . . . . . . . . . . . 14 |- ( t e. { Z } -> t = Z )
307	305, 306	syl 17	. . . . . . . . . . . . 13 |- ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t = Z )
308	307	adantll 750	. . . . . . . . . . . 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 )
309		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> t = Z )
310	309	fveq2d 6195	. . . . . . . . . . . . . 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 ) )
311	3	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> J e. CC )
312	311	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
313	312, 131	nncand 10397	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( c ` Z ) )
314	313	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
315	314	adantrr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
316	315	adantr 481	. . . . . . . . . . . . . . . 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 ) ) ) )
317	266	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
318	269, 236	op1st 7176	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) )
319	318	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) ) )
320	317, 319	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) = ( 1st ` ( D ` c ) ) )
321	320	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
322	321	adantrr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
323	322	adantr 481	. . . . . . . . . . . . . . . 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 ) ) ) )
324		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` c ) = ( D ` e ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
325	324	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
326	286	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
327	326	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
328	292, 294	op1st 7176	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) )
329	328	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) ) )
330	325, 327, 329	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( J - ( e ` Z ) ) )
331	330	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( J - ( J - ( e ` Z ) ) ) )
332	311	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
333		zsscn 11385	. . . . . . . . . . . . . . . . . . . . . . 23 |- ZZ C_ CC
334	6, 333	sstri 3612	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 ... J ) C_ CC
335	334	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... J ) C_ CC )
336		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c = e -> ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) <-> e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
337	336	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) <-> ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) )
338		feq1 6026	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( c : ( R u. { Z } ) --> ( 0 ... J ) <-> e : ( R u. { Z } ) --> ( 0 ... J ) ) )
339	337, 338	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
340	339, 49	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) )
341	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
342	340, 341	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. ( 0 ... J ) )
343	335, 342	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. CC )
344	332, 343	nncand 10397	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
345	344	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
346		eqidd 2623	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( e ` Z ) = ( e ` Z ) )
347	331, 345, 346	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
348	347	adantlrl 756	. . . . . . . . . . . . . . . 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 ) )
349	316, 323, 348	3eqtrd 2660	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c ` Z ) = ( e ` Z ) )
350	349	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
351		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( t = Z -> ( e ` t ) = ( e ` Z ) )
352	351	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( t = Z -> ( e ` Z ) = ( e ` t ) )
353	352	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
354	310, 350, 353	3eqtrd 2660	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
355	354	adantlr 751	. . . . . . . . . . . 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 = Z ) -> ( c ` t ) = ( e ` t ) )
356	304, 308, 355	syl2anc 693	. . . . . . . . . . 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 ) )
357	303, 356	pm2.61dan 832	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
358	357	ex 450	. . . . . . . . 9 |- ( ( ( 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 ) ) )
359	259, 358	ralrimi 2957	. . . . . . . 8 |- ( ( ( 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 ) )
360	74	adantrr 753	. . . . . . . . . 10 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> c Fn ( R u. { Z } ) )
361	360	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> c Fn ( R u. { Z } ) )
362		ffn 6045	. . . . . . . . . . . 12 |- ( e : ( R u. { Z } ) --> ( 0 ... J ) -> e Fn ( R u. { Z } ) )
363	340, 362	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e Fn ( R u. { Z } ) )
364	363	adantrl 752	. . . . . . . . . 10 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> e Fn ( R u. { Z } ) )
365	364	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> e Fn ( R u. { Z } ) )
366		eqfnfv 6311	. . . . . . . . 9 |- ( ( c Fn ( R u. { Z } ) /\ e Fn ( R u. { Z } ) ) -> ( c = e <-> A. t e. ( R u. { Z } ) ( c ` t ) = ( e ` t ) ) )
367	361, 365, 366	syl2anc 693	. . . . . . . 8 |- ( ( ( 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 ) ) )
368	359, 367	mpbird 247	. . . . . . 7 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> c = e )
369	368	ex 450	. . . . . 6 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( D ` c ) = ( D ` e ) -> c = e ) )
370	369	ralrimivva 2971	. . . . 5 |- ( ph -> A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) )
371	254, 370	jca 554	. . . 4 |- ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. c e. ( ( C ` ( R u. { Z } ) ) ` J ) A. e e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( D ` c ) = ( D ` e ) -> c = e ) ) )
372		dff13 6512	. . . 4 |- ( 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 ) ) )
373	371, 372	sylibr 224	. . 3 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
374		eliun 4524	. . . . . . . . . . 11 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
375	374	biimpi 206	. . . . . . . . . 10 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
376	375	adantl 482	. . . . . . . . 9 |- ( ( 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 ) ) )
377		nfv 1843	. . . . . . . . . . 11 |- F/ k ph
378		nfcv 2764	. . . . . . . . . . . 12 |- F/_ k p
379		nfiu1 4550	. . . . . . . . . . . 12 |- F/_ k U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
380	378, 379	nfel 2777	. . . . . . . . . . 11 |- F/ k p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
381	377, 380	nfan 1828	. . . . . . . . . 10 |- F/ k ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
382		nfv 1843	. . . . . . . . . 10 |- 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 }
383		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ t k e. ( 0 ... J )
384		nfcv 2764	. . . . . . . . . . . . . . . . . 18 |- F/_ t p
385		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ t { k }
386		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t R
387	91, 386	nffv 6198	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t ( C ` R )
388		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t k
389	387, 388	nffv 6198	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( ( C ` R ) ` k )
390	385, 389	nfxp 5142	. . . . . . . . . . . . . . . . . 18 |- F/_ t ( { k } X. ( ( C ` R ) ` k ) )
391	384, 390	nfel 2777	. . . . . . . . . . . . . . . . 17 |- F/ t p e. ( { k } X. ( ( C ` R ) ` k ) )
392	79, 383, 391	nf3an 1831	. . . . . . . . . . . . . . . 16 |- F/ t ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) )
393		0zd 11389	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> 0 e. ZZ )
394	4	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
395	394	3ad2antl1 1223	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> J e. ZZ )
396		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. R -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( ( 2nd ` p ) ` t ) )
397	396	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) )
398		fzssz 12343	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 ... k ) C_ ZZ
399	398	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( 0 ... k ) C_ ZZ )
400		simp1 1061	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ph )
401		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
402		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
403	402	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
404	198	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
405		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
406	405	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
407		rabeq 3192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
408	406, 407	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
409		eqeq2 2633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
410	409	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
411	408, 410	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 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 } )
412	411	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ n = k ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
413		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( k e. ( 0 ... J ) -> k e. NN0 )
414	413	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
415		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 0 ... k ) ^m R ) e. _V
416	415	rabex 4813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V
417	416	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
418	404, 412, 414, 417	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
419	418	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 } )
420	403, 419	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 } )
421		elrabi 3359	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
422	421	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... J ) /\ ( 2nd ` p ) e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
423	400, 401, 420, 422	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) )
424		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 2nd ` p ) e. ( ( 0 ... k ) ^m R ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
425	423, 424	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
426	425	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( 2nd ` p ) : R --> ( 0 ... k ) )
427	426	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) )
428	399, 427	sseldd 3604	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
429	397, 428	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 )
430		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) )
431	307	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> t = Z )
432		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ t = Z ) -> t = Z )
433	136	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ t = Z ) -> -. Z e. R )
434	432, 433	eqneltrd 2720	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t = Z ) -> -. t e. R )
435	434	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
436	435	3ad2antl1 1223	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) )
437	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t = Z ) -> J e. ZZ )
438	437	3ad2antl1 1223	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> J e. ZZ )
439		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. { k } )
440		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 1st ` p ) e. { k } -> ( 1st ` p ) = k )
441	439, 440	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) = k )
442	441	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
443	6	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k e. ( 0 ... J ) -> k e. ZZ )
444	443	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ZZ )
445	442, 444	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
446	445	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
447	446	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( 1st ` p ) e. ZZ )
448	438, 447	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) e. ZZ )
449	436, 448	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 )
450	449	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
451	430, 431, 450	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 )
452	429, 451	pm2.61dan 832	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 )
453	393, 395, 452	3jca 1242	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( 0 e. ZZ /\ J e. ZZ /\ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ ) )
454	425	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) )
455		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
456	454, 455	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> 0 <_ ( ( 2nd ` p ) ` t ) )
457	396	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. R -> ( ( 2nd ` p ) ` t ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
458	457	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) )
459	456, 458	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
460	459	adantlr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
461		simpll 790	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) )
462		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( 0 ... J ) -> k <_ J )
463		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k e. ( 0 ... J ) -> J e. ZZ )
464	463	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( 0 ... J ) -> J e. RR )
465	115	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( 0 ... J ) -> k e. RR )
466	464, 465	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( 0 ... J ) -> ( 0 <_ ( J - k ) <-> k <_ J ) )
467	462, 466	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... J ) -> 0 <_ ( J - k ) )
468	467	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( k e. ( 0 ... J ) /\ t = Z ) -> 0 <_ ( J - k ) )
469	468	3ad2antl2 1224	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> 0 <_ ( J - k ) )
470	400, 434	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> -. t e. R )
471	470	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 ) ) )
472	442	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
473	472	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
474	473	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - ( 1st ` p ) ) = ( J - k ) )
475	471, 474	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) )
476	469, 475	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
477	461, 431, 476	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) ) ) )
478	460, 477	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
479		simpl2 1065	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> k e. ( 0 ... J ) )
480	398	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
481	480	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) e. RR )
482	481	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) e. RR )
483	465	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k e. RR )
484	464	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> J e. RR )
485		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) -> ( ( 2nd ` p ) ` t ) <_ k )
486	485	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ k )
487	462	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> k <_ J )
488	482, 483, 484, 486, 487	letrd 10194	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 2nd ` p ) ` t ) e. ( 0 ... k ) /\ k e. ( 0 ... J ) ) -> ( ( 2nd ` p ) ` t ) <_ J )
489	454, 479, 488	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) <_ J )
490	489	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) <_ J )
491	397, 490	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
492	475	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = ( J - k ) )
493	414	nn0ge0d 11354	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. ( 0 ... J ) ) -> 0 <_ k )
494	464	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J e. RR )
495	465	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. RR )
496	494, 495	subge02d 10619	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 <_ k <-> ( J - k ) <_ J ) )
497	493, 496	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J - k ) <_ J )
498	497	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ t = Z ) -> ( J - k ) <_ J )
499	498	3adantl3 1219	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t = Z ) -> ( J - k ) <_ J )
500	492, 499	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 )
501	461, 431, 500	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
502	491, 501	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 )
503	453, 478, 502	jca32 558	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ ) /\ ( 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) /\ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J ) ) )
504		elfz2 12333	. . . . . . . . . . . . . . . . 17 |- ( if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ( 0 ... J ) <-> ( ( 0 e. ZZ /\ J e. ZZ /\ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) e. ZZ ) /\ ( 0 <_ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) /\ if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) <_ J ) ) )
505	503, 504	sylibr 224	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
506		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
507	392, 505, 506	fmptdf 6387	. . . . . . . . . . . . . . 15 |- ( ( 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 ) )
508		ovexd 6680	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 0 ... J ) e. _V )
509	400, 22	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( R u. { Z } ) e. _V )
510	508, 509	elmapd 7871	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) <-> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) : ( R u. { Z } ) --> ( 0 ... J ) ) )
511	507, 510	mpbird 247	. . . . . . . . . . . . . 14 |- ( ( 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 } ) ) )
512		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) ) )
513		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21 |- ( r = t -> ( r e. R <-> t e. R ) )
514		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( r = t -> ( ( 2nd ` p ) ` r ) = ( ( 2nd ` p ) ` t ) )
515	513, 514	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . 20 |- ( r = t -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
516	515	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) /\ r = t ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) )
517		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. ( R u. { Z } ) ) -> t e. ( R u. { Z } ) )
518	512, 516, 517, 452	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
519	518	ex 450	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) ) )
520	392, 519	ralrimi 2957	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
521	520	sumeq2d 14432	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
522		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ t if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) )
523	400, 112	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> R e. Fin )
524	400, 50	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> Z e. T )
525	400, 136	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
526	396	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
527	454, 480	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ZZ )
528	527	zcnd 11483	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. CC )
529	526, 528	eqeltrd 2701	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
530		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( t = Z -> ( t e. R <-> Z e. R ) )
531		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( t = Z -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` Z ) )
532	530, 531	ifbieq1d 4109	. . . . . . . . . . . . . . . 16 |- ( t = Z -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) )
533	136	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> -. Z e. R )
534	533	iffalsed 4097	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
535	534	3adant2 1080	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
536	4	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. ZZ )
537	536, 446	zsubcld 11487	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ZZ )
538	537	zcnd 11483	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. CC )
539	535, 538	eqeltrd 2701	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) e. CC )
540	392, 522, 523, 524, 525, 529, 532, 539	fsumsplitsn 14474	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) )
541	396	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) )
542	392, 541	ralrimi 2957	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) )
543	542	sumeq2d 14432	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) )
544		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = ( 2nd ` p ) -> R = R )
545		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( c = ( 2nd ` p ) /\ t e. R ) -> c = ( 2nd ` p ) )
546	545	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( c = ( 2nd ` p ) /\ t e. R ) -> ( c ` t ) = ( ( 2nd ` p ) ` t ) )
547	544, 546	sumeq12rdv 14438	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c = ( 2nd ` p ) -> sum_ t e. R ( c ` t ) = sum_ t e. R ( ( 2nd ` p ) ` t ) )
548	547	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21 |- ( c = ( 2nd ` p ) -> ( sum_ t e. R ( c ` t ) = k <-> sum_ t e. R ( ( 2nd ` p ) ` t ) = k ) )
549	548	elrab 3363	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) )
550	420, 549	sylib 208	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) )
551	550	simprd 479	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> sum_ t e. R ( ( 2nd ` p ) ` t ) = k )
552	543, 551	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( 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 )
553	525	iffalsed 4097	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) )
554	553, 473	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> if ( Z e. R , ( ( 2nd ` p ) ` Z ) , ( J - ( 1st ` p ) ) ) = ( J - k ) )
555	552, 554	oveq12d 6668	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
556	334	sseli 3599	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0 ... J ) -> k e. CC )
557	556	3ad2ant2 1083	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. CC )
558	400, 311	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. CC )
559	557, 558	pncan3d 10395	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( k + ( J - k ) ) = J )
560	555, 559	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( 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 )
561	521, 540, 560	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ( 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 )
562	511, 561	jca 554	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J ) )
563		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 |- ( t = r -> ( t e. R <-> r e. R ) )
564		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( t = r -> ( ( 2nd ` p ) ` t ) = ( ( 2nd ` p ) ` r ) )
565	563, 564	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . 19 |- ( t = r -> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) = if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) )
566	565	cbvmptv 4750	. . . . . . . . . . . . . . . . . 18 |- ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) )
567	566	eqeq2i 2634	. . . . . . . . . . . . . . . . 17 |- ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) <-> c = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
568	567	biimpi 206	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
569		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( 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 ) )
570	569	sumeq2ad 14434	. . . . . . . . . . . . . . . 16 |- ( 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 ) )
571	568, 570	syl 17	. . . . . . . . . . . . . . 15 |- ( 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 ) )
572	571	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( 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 ) )
573	572	elrab 3363	. . . . . . . . . . . . 13 |- ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } <-> ( ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) ` t ) = J ) )
574	562, 573	sylibr 224	. . . . . . . . . . . 12 |- ( ( 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 } )
575	574	3exp 1264	. . . . . . . . . . 11 |- ( 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 } ) ) )
576	575	adantr 481	. . . . . . . . . 10 |- ( ( 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 } ) ) )
577	381, 382, 576	rexlimd 3026	. . . . . . . . 9 |- ( ( 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 } ) )
578	376, 577	mpd 15	. . . . . . . 8 |- ( ( 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 } )
579	41	eqcomd 2628	. . . . . . . . 9 |- ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } = ( ( C ` ( R u. { Z } ) ) ` J ) )
580	579	adantr 481	. . . . . . . 8 |- ( ( 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 ) )
581	578, 580	eleqtrd 2703	. . . . . . 7 |- ( ( 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 ) )
582	253	a1i 11	. . . . . . . . 9 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
583		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) )
584	566	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( r e. ( R u. { Z } ) |-> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) ) )
585	583, 584	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) )
586		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ r = Z ) -> r = Z )
587	136	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ r = Z ) -> -. Z e. R )
588	586, 587	eqneltrd 2720	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ r = Z ) -> -. r e. R )
589	588	iffalsed 4097	. . . . . . . . . . . . . . 15 |- ( ( ph /\ r = Z ) -> if ( r e. R , ( ( 2nd ` p ) ` r ) , ( J - ( 1st ` p ) ) ) = ( J - ( 1st ` p ) ) )
590	589	adantlr 751	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
591	54	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> Z e. ( R u. { Z } ) )
592		ovexd 6680	. . . . . . . . . . . . . 14 |- ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( 1st ` p ) ) e. _V )
593	585, 590, 591, 592	fvmptd 6288	. . . . . . . . . . . . 13 |- ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( c ` Z ) = ( J - ( 1st ` p ) ) )
594	593	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ph /\ c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) -> ( J - ( c ` Z ) ) = ( J - ( J - ( 1st ` p ) ) ) )
595	594	adantlr 751	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
596	311	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( 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 )
597		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ k ( 1st ` p ) e. ( 0 ... J )
598		simpl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
599		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> ( 1st ` p ) = k )
600		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> k e. ( 0 ... J ) )
601	599, 600	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. ( 0 ... J ) /\ ( 1st ` p ) = k ) -> ( 1st ` p ) e. ( 0 ... J ) )
602	598, 442, 601	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
603	602	ex 450	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) )
604	603	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) )
605	380, 597, 604	rexlimd 3026	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
606	375, 605	mpd 15	. . . . . . . . . . . . . . 15 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
607	6	sseli 3599	. . . . . . . . . . . . . . 15 |- ( ( 1st ` p ) e. ( 0 ... J ) -> ( 1st ` p ) e. ZZ )
608	606, 607	syl 17	. . . . . . . . . . . . . 14 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ZZ )
609	608	zcnd 11483	. . . . . . . . . . . . 13 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. CC )
610	609	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( 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 )
611	596, 610	nncand 10397	. . . . . . . . . . 11 |- ( ( ( 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 ) )
612	595, 611	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( 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 ) )
613		reseq1 5390	. . . . . . . . . . . 12 |- ( 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 ) )
614	613	adantl 482	. . . . . . . . . . 11 |- ( ( ( 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 ) )
615	75	a1i 11	. . . . . . . . . . . 12 |- ( ( ( 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 } ) )
616	615	resmptd 5452	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) )
617		nfv 1843	. . . . . . . . . . . . . 14 |- F/ k ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( 2nd ` p )
618	396	mpteq2ia 4740	. . . . . . . . . . . . . . . . . 18 |- ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) )
619	618	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( t e. R |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) ) )
620	425	feqmptd 6249	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) = ( t e. R |-> ( ( 2nd ` p ) ` t ) ) )
621	619, 620	eqtr4d 2659	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
622	621	3exp 1264	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
623	622	adantr 481	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
624	381, 617, 623	rexlimd 3026	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
625	376, 624	mpd 15	. . . . . . . . . . . 12 |- ( ( 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 ) )
626	625	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 ) )
627	614, 616, 626	3eqtrd 2660	. . . . . . . . . 10 |- ( ( ( 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 ) )
628	612, 627	opeq12d 4410	. . . . . . . . 9 |- ( ( ( 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 ) >. )
629		opex 4932	. . . . . . . . . 10 |- <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V
630	629	a1i 11	. . . . . . . . 9 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. e. _V )
631	582, 628, 581, 630	fvmptd 6288	. . . . . . . 8 |- ( ( 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 ) >. )
632		nfv 1843	. . . . . . . . . 10 |- F/ k <. ( 1st ` p ) , ( 2nd ` p ) >. = p
633		1st2nd2 7205	. . . . . . . . . . . . 13 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
634	633	eqcomd 2628	. . . . . . . . . . . 12 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
635	634	a1i 11	. . . . . . . . . . 11 |- ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p ) )
636	635	a1i 11	. . . . . . . . . 10 |- ( ( 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 ) ) )
637	381, 632, 636	rexlimd 3026	. . . . . . . . 9 |- ( ( 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 ) )
638	376, 637	mpd 15	. . . . . . . 8 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = p )
639	631, 638	eqtr2d 2657	. . . . . . 7 |- ( ( 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 ) ) ) ) ) )
640		fveq2 6191	. . . . . . . . 9 |- ( 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 ) ) ) ) ) )
641	640	eqeq2d 2632	. . . . . . . 8 |- ( c = ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) -> ( p = ( D ` c ) <-> p = ( D ` ( t e. ( R u. { Z } ) |-> if ( t e. R , ( ( 2nd ` p ) ` t ) , ( J - ( 1st ` p ) ) ) ) ) ) )
642	641	rspcev 3309	. . . . . . 7 |- ( ( ( 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 ) )
643	581, 639, 642	syl2anc 693	. . . . . 6 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) )
644	643	ralrimiva 2966	. . . . 5 |- ( 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 ) )
645	254, 644	jca 554	. . . 4 |- ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ A. p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) E. c e. ( ( C ` ( R u. { Z } ) ) ` J ) p = ( D ` c ) ) )
646		dffo3 6374	. . . 4 |- ( 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 ) ) )
647	645, 646	sylibr 224	. . 3 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
648	373, 647	jca 554	. 2 |- ( ph -> ( D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) /\ D : ( ( C ` ( R u. { Z } ) ) ` J ) -onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) )
649		df-f1o 5895	. 2 |- ( 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 ) ) ) )
650	648, 649	sylibr 224	1 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   u. cun 3572   C_ wss 3574   ifcif 4086   ~Pcpw 4158   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   |` cres 5116   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   + caddc 9939   <_ cle 10075   - cmin 10266   NN0cn0 11292   ZZcz 11377   ...cfz 12326   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417

This theorem is referenced by:  dvnprodlem2  40162