Theorem dvnprodlem1 31982

Description: D is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypotheses

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

Assertion

Ref	Expression
dvnprodlem1	|- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )

Distinct variable groups:   C, c, k   D, c, t   J, c, k, n, t   R, c, k, n, t   R, s, c, n, t   t, T, s   Z, c, k, n, t   Z, s   ph, c, n, t, k   ph, s

Allowed substitution hints:   C( t, n, s)   D( k, n, s)   T( k, n, c)   J( s)

Proof of Theorem dvnprodlem1

Dummy variables d e m p r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2455	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
2		0zd 10872	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 e. ZZ )
3		dvnprodlem1.j	. . . . . . . . . . . . . . 15 |- ( ph -> J e. NN0 )
4	3	nn0zd 10963	. . . . . . . . . . . . . 14 |- ( ph -> J e. ZZ )
5	4	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. ZZ )
6		fzssz 31706	. . . . . . . . . . . . . . . 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 6278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = ( R u. { Z } ) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) )
11		rabeq 3100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } )
12	10, 11	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } )
13		sumeq1 13593	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = ( R u. { Z } ) -> sum_ t e. s ( c ` t ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
14	13	eqeq1d 2456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = ( R u. { Z } ) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = n ) )
15	14	rabbidv 3098	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
16	12, 15	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s = ( R u. { Z } ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
17	16	mpteq2dv 4526	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s = ( R u. { Z } ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) )
18	17	adantl 464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ s = ( R u. { Z } ) ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) )
19		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( R u. { Z } ) C_ T )
20		dvnprodlem1.t	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> T e. Fin )
21		ssexg 4583	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( R u. { Z } ) C_ T /\ T e. Fin ) -> ( R u. { Z } ) e. _V )
22	19, 20, 21	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( R u. { Z } ) e. _V )
23		elpwg 4007	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( R u. { Z } ) e. _V -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
25	19, 24	mpbird 232	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( R u. { Z } ) e. ~P T )
26		nn0ex 10797	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
27	26	mptex 6118	. . . . . . . . . . . . . . . . . . . . . . 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 5936	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( C ` ( R u. { Z } ) ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) )
30		oveq2 6278	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = J -> ( 0 ... n ) = ( 0 ... J ) )
31	30	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = J -> ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
32		rabeq 3100	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
33	31, 32	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = J -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } )
34		eqeq2 2469	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = J -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
35	34	rabbidv 3098	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = J -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
36	33, 35	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = J -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
37	36	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ n = J ) -> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
38		ovex 6298	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. _V
39	38	rabex 4588	. . . . . . . . . . . . . . . . . . . . . 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 5936	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
42		ssrab2 3571	. . . . . . . . . . . . . . . . . . . . 21 |- { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } C_ ( ( 0 ... J ) ^m ( R u. { Z } ) )
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 3523	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
45	44	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` ( R u. { Z } ) ) ` J ) C_ ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
46		simpr 459	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
47	45, 46	sseldd 3490	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
48		elmapi 7433	. . . . . . . . . . . . . . . . 17 |- ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
49	47, 48	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
50		dvnprodlem1.z	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> Z e. T )
51		snidg 4042	. . . . . . . . . . . . . . . . . . 19 |- ( Z e. T -> Z e. { Z } )
52	50, 51	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Z e. { Z } )
53		elun2 3658	. . . . . . . . . . . . . . . . . 18 |- ( Z e. { Z } -> Z e. ( R u. { Z } ) )
54	52, 53	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> Z e. ( R u. { Z } ) )
55	54	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
56	49, 55	ffvelrnd 6008	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... J ) )
57	7, 56	sseldd 3490	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ZZ )
58	5, 57	zsubcld 10970	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ZZ )
59	2, 5, 58	3jca 1174	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) )
60		elfzle2 11693	. . . . . . . . . . . . . 14 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) <_ J )
61	56, 60	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) <_ J )
62	5	zred 10965	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. RR )
63	57	zred 10965	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. RR )
64	62, 63	subge0d 10138	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( J - ( c ` Z ) ) <-> ( c ` Z ) <_ J ) )
65	61, 64	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( J - ( c ` Z ) ) )
66		elfzle1 11692	. . . . . . . . . . . . . 14 |- ( ( c ` Z ) e. ( 0 ... J ) -> 0 <_ ( c ` Z ) )
67	56, 66	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> 0 <_ ( c ` Z ) )
68	62, 63	subge02d 10140	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 <_ ( c ` Z ) <-> ( J - ( c ` Z ) ) <_ J ) )
69	67, 68	mpbid 210	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) <_ J )
70	59, 65, 69	jca32 533	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) /\ ( 0 <_ ( J - ( c ` Z ) ) /\ ( J - ( c ` Z ) ) <_ J ) ) )
71		elfz2 11682	. . . . . . . . . . 11 |- ( ( J - ( c ` Z ) ) e. ( 0 ... J ) <-> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) /\ ( 0 <_ ( J - ( c ` Z ) ) /\ ( J - ( c ` Z ) ) <_ J ) ) )
72	70, 71	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
73		elmapfn 7434	. . . . . . . . . . . . . . . . . 18 |- ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c Fn ( R u. { Z } ) )
74	47, 73	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c Fn ( R u. { Z } ) )
75		ssun1 3653	. . . . . . . . . . . . . . . . . 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 5676	. . . . . . . . . . . . . . . . 17 |- ( ( c Fn ( R u. { Z } ) /\ R C_ ( R u. { Z } ) ) -> ( c |` R ) Fn R )
78	74, 76, 77	syl2anc 659	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) Fn R )
79		nfv 1712	. . . . . . . . . . . . . . . . . 18 |- F/ t ph
80		nfcv 2616	. . . . . . . . . . . . . . . . . . 19 |- F/_ t c
81		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ~P T
82		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t NN0
83		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F/_ t s
84	83	nfsum1 13594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ t sum_ t e. s ( c ` t )
85		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ t n
86	84, 85	nfeq 2627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ t sum_ t e. s ( c ` t ) = n
87		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ t ( ( 0 ... n ) ^m s )
88	86, 87	nfrab 3036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ t { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n }
89	82, 88	nfmpt 4527	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ t ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } )
90	81, 89	nfmpt 4527	. . . . . . . . . . . . . . . . . . . . . 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 2614	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t C
92		nfcv 2616	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ t ( R u. { Z } )
93	91, 92	nffv 5855	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t ( C ` ( R u. { Z } ) )
94		nfcv 2616	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t J
95	93, 94	nffv 5855	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ( ( C ` ( R u. { Z } ) ) ` J )
96	80, 95	nfel 2629	. . . . . . . . . . . . . . . . . 18 |- F/ t c e. ( ( C ` ( R u. { Z } ) ) ` J )
97	79, 96	nfan 1933	. . . . . . . . . . . . . . . . 17 |- F/ t ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
98		fvres 5862	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) )
99	98	adantl 464	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( c ` t ) )
100	2	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 e. ZZ )
101	58	adantr 463	. . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
104	76	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. ( R u. { Z } ) )
105	103, 104	ffvelrnd 6008	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... J ) )
106	102, 105	sseldd 3490	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ZZ )
107	100, 101, 106	3jca 1174	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( 0 e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ /\ ( c ` t ) e. ZZ ) )
108		elfzle1 11692	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( c ` t ) e. ( 0 ... J ) -> 0 <_ ( c ` t ) )
109	105, 108	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> 0 <_ ( c ` t ) )
110	19	unssad 3667	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> R C_ T )
111		ssfi 7733	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
112	20, 110, 111	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> R e. Fin )
113	112	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> R e. Fin )
114		zssre 10867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ZZ C_ RR
115	6, 114	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
118	76	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> r e. ( R u. { Z } ) )
119	117, 118	ffvelrnd 6008	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. ( 0 ... J ) )
120	116, 119	sseldd 3490	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. RR )
121	120	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> ( c ` r ) e. RR )
122		elfzle1 11692	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` r ) e. ( 0 ... J ) -> 0 <_ ( c ` r ) )
123	119, 122	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> 0 <_ ( c ` r ) )
124	123	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) /\ r e. R ) -> 0 <_ ( c ` r ) )
125		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( r = t -> ( c ` r ) = ( c ` t ) )
126		simpr 459	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. R )
127	113, 121, 124, 125, 126	fsumge1 13693	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ sum_ r e. R ( c ` r ) )
128	112	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
129	120	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ r e. R ) -> ( c ` r ) e. CC )
130	128, 129	fsumcl 13637	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) e. CC )
131	63	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. CC )
132	130, 131	pncand 9923	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) - ( c ` Z ) ) = sum_ r e. R ( c ` r ) )
133		nfv 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F/ r ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
134		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- F/_ r ( c ` Z )
135	50	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
136		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> -. Z e. R )
137	136	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
138		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( r = Z -> ( c ` r ) = ( c ` Z ) )
139	133, 134, 128, 135, 137, 129, 138, 131	fsumsplitsn 31810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) )
140	139	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = sum_ r e. ( R u. { Z } ) ( c ` r ) )
141	125	cbvsumv 13600	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
144	46, 143	eleqtrd 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
145		rabid 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( c e. { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } <-> ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
146	144, 145	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) /\ sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
147	146	simprd 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. ( R u. { Z } ) ( c ` t ) = J )
148	142, 147	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. ( R u. { Z } ) ( c ` r ) = J )
149	140, 148	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( sum_ r e. R ( c ` r ) + ( c ` Z ) ) = J )
150	149	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . 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 2497	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
152	151	adantr 463	. . . . . . . . . . . . . . . . . . . . . 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 4463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) <_ ( J - ( c ` Z ) ) )
154	107, 109, 153	jca32 533	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( 0 e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ /\ ( c ` t ) e. ZZ ) /\ ( 0 <_ ( c ` t ) /\ ( c ` t ) <_ ( J - ( c ` Z ) ) ) ) )
155		elfz2 11682	. . . . . . . . . . . . . . . . . . . 20 |- ( ( c ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) <-> ( ( 0 e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ /\ ( c ` t ) e. ZZ ) /\ ( 0 <_ ( c ` t ) /\ ( c ` t ) <_ ( J - ( c ` Z ) ) ) ) )
156	154, 155	sylibr 212	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
157	99, 156	eqeltrd 2542	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) )
158	157	ex 432	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
159	97, 158	ralrimi 2854	. . . . . . . . . . . . . . . 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 530	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
161		ffnfv 6033	. . . . . . . . . . . . . . 15 |- ( ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) <-> ( ( c |` R ) Fn R /\ A. t e. R ( ( c |` R ) ` t ) e. ( 0 ... ( J - ( c ` Z ) ) ) ) )
162	160, 161	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) )
163		ovex 6298	. . . . . . . . . . . . . . . 16 |- ( 0 ... ( J - ( c ` Z ) ) ) e. _V
164	163	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... ( J - ( c ` Z ) ) ) e. _V )
165	20, 110	ssexd 4584	. . . . . . . . . . . . . . . 16 |- ( ph -> R e. _V )
166	165	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. _V )
167	164, 166	elmapd 7426	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) <-> ( c |` R ) : R --> ( 0 ... ( J - ( c ` Z ) ) ) ) )
168	162, 167	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
169	98	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) ) )
170	97, 169	ralrimi 2854	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> A. t e. R ( ( c |` R ) ` t ) = ( c ` t ) )
171	170	sumeq2d 13606	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = sum_ t e. R ( c ` t ) )
172	125	cbvsumv 13600	. . . . . . . . . . . . . . . 16 |- sum_ r e. R ( c ` r ) = sum_ t e. R ( c ` t )
173	172	eqcomi 2467	. . . . . . . . . . . . . . 15 |- sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r )
174	173	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( c ` t ) = sum_ r e. R ( c ` r ) )
175	151	idi 2	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ r e. R ( c ` r ) = ( J - ( c ` Z ) ) )
176	171, 174, 175	3eqtrd 2499	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) )
177	168, 176	jca 530	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) /\ sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
178		eqidd 2455	. . . . . . . . . . . . . . 15 |- ( e = ( c |` R ) -> R = R )
179		simpl 455	. . . . . . . . . . . . . . . 16 |- ( ( e = ( c |` R ) /\ t e. R ) -> e = ( c |` R ) )
180	179	fveq1d 5850	. . . . . . . . . . . . . . 15 |- ( ( e = ( c |` R ) /\ t e. R ) -> ( e ` t ) = ( ( c |` R ) ` t ) )
181	178, 180	sumeq12rdv 13611	. . . . . . . . . . . . . 14 |- ( e = ( c |` R ) -> sum_ t e. R ( e ` t ) = sum_ t e. R ( ( c |` R ) ` t ) )
182	181	eqeq1d 2456	. . . . . . . . . . . . 13 |- ( e = ( c |` R ) -> ( sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) <-> sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
183	182	elrab 3254	. . . . . . . . . . . 12 |- ( ( c |` R ) e. { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } <-> ( ( c |` R ) e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) /\ sum_ t e. R ( ( c |` R ) ` t ) = ( J - ( c ` Z ) ) ) )
184	177, 183	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
185		oveq2 6278	. . . . . . . . . . . . . . . . . . . 20 |- ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
186		rabeq 3100	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
187	185, 186	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
188		sumeq1 13593	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
189	188	eqeq1d 2456	. . . . . . . . . . . . . . . . . . . 20 |- ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
190	189	rabbidv 3098	. . . . . . . . . . . . . . . . . . 19 |- ( s = R -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
191	187, 190	eqtrd 2495	. . . . . . . . . . . . . . . . . 18 |- ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
192	191	mpteq2dv 4526	. . . . . . . . . . . . . . . . 17 |- ( s = R -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
193	192	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ s = R ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
194		elpwg 4007	. . . . . . . . . . . . . . . . . 18 |- ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
195	165, 194	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( R e. ~P T <-> R C_ T ) )
196	110, 195	mpbird 232	. . . . . . . . . . . . . . . 16 |- ( ph -> R e. ~P T )
197	26	mptex 6118	. . . . . . . . . . . . . . . . 17 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
198	197	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
199	9, 193, 196, 198	fvmptd 5936	. . . . . . . . . . . . . . 15 |- ( ph -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
200	199	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
201		oveq2 6278	. . . . . . . . . . . . . . . . . . 19 |- ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
202	201	oveq1d 6285	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) )
203		rabeq 3100	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 0 ... n ) ^m R ) = ( ( 0 ... m ) ^m R ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
204	202, 203	syl 16	. . . . . . . . . . . . . . . . 17 |- ( n = m -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
205		eqeq2 2469	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = m ) )
206	205	rabbidv 3098	. . . . . . . . . . . . . . . . 17 |- ( n = m -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
207	204, 206	eqtrd 2495	. . . . . . . . . . . . . . . 16 |- ( n = m -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
208	207	cbvmptv 4530	. . . . . . . . . . . . . . 15 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) = ( m e. NN0 |-> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } )
209	208	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 } ) )
210	200, 209	eqtrd 2495	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( C ` R ) = ( m e. NN0 |-> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } ) )
211		fveq1 5847	. . . . . . . . . . . . . . . . . . 19 |- ( c = e -> ( c ` t ) = ( e ` t ) )
212	211	sumeq2ad 31805	. . . . . . . . . . . . . . . . . 18 |- ( c = e -> sum_ t e. R ( c ` t ) = sum_ t e. R ( e ` t ) )
213	212	eqeq1d 2456	. . . . . . . . . . . . . . . . 17 |- ( c = e -> ( sum_ t e. R ( c ` t ) = m <-> sum_ t e. R ( e ` t ) = m ) )
214	213	cbvrabv 3105	. . . . . . . . . . . . . . . 16 |- { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m }
215	214	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 } )
216		oveq2 6278	. . . . . . . . . . . . . . . . 17 |- ( m = ( J - ( c ` Z ) ) -> ( 0 ... m ) = ( 0 ... ( J - ( c ` Z ) ) ) )
217	216	oveq1d 6285	. . . . . . . . . . . . . . . 16 |- ( m = ( J - ( c ` Z ) ) -> ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) )
218		rabeq 3100	. . . . . . . . . . . . . . . 16 |- ( ( ( 0 ... m ) ^m R ) = ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) -> { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } )
219	217, 218	syl 16	. . . . . . . . . . . . . . 15 |- ( m = ( J - ( c ` Z ) ) -> { e e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } )
220		eqeq2 2469	. . . . . . . . . . . . . . . 16 |- ( m = ( J - ( c ` Z ) ) -> ( sum_ t e. R ( e ` t ) = m <-> sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) ) )
221	220	rabbidv 3098	. . . . . . . . . . . . . . 15 |- ( m = ( J - ( c ` Z ) ) -> { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
222	215, 219, 221	3eqtrd 2499	. . . . . . . . . . . . . 14 |- ( m = ( J - ( c ` Z ) ) -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
223	222	adantl 464	. . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ m = ( J - ( c ` Z ) ) ) -> { c e. ( ( 0 ... m ) ^m R ) | sum_ t e. R ( c ` t ) = m } = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
224	58, 65	jca 530	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
225		elnn0z 10873	. . . . . . . . . . . . . 14 |- ( ( J - ( c ` Z ) ) e. NN0 <-> ( ( J - ( c ` Z ) ) e. ZZ /\ 0 <_ ( J - ( c ` Z ) ) ) )
226	224, 225	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. NN0 )
227		ovex 6298	. . . . . . . . . . . . . . 15 |- ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) e. _V
228	227	rabex 4588	. . . . . . . . . . . . . 14 |- { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } e. _V
229	228	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 )
230	210, 223, 226, 229	fvmptd 5936	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( C ` R ) ` ( J - ( c ` Z ) ) ) = { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } )
231	230	eqcomd 2462	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> { e e. ( ( 0 ... ( J - ( c ` Z ) ) ) ^m R ) | sum_ t e. R ( e ` t ) = ( J - ( c ` Z ) ) } = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
232	184, 231	eleqtrd 2544	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
233	72, 232	jca 530	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
234	1, 233	jca 530	. . . . . . . 8 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) )
235	232	elfvexd 5876	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. _V )
236		vex 3109	. . . . . . . . . . 11 |- c e. _V
237	236	resex 5305	. . . . . . . . . 10 |- ( c |` R ) e. _V
238	237	a1i 11	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c |` R ) e. _V )
239		opeq12 4205	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> <. k , d >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
240	239	eqeq2d 2468	. . . . . . . . . . 11 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. <-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
241		eleq1 2526	. . . . . . . . . . . . 13 |- ( k = ( J - ( c ` Z ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
242	241	adantr 463	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( k e. ( 0 ... J ) <-> ( J - ( c ` Z ) ) e. ( 0 ... J ) ) )
243		simpr 459	. . . . . . . . . . . . 13 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> d = ( c |` R ) )
244		fveq2 5848	. . . . . . . . . . . . . 14 |- ( k = ( J - ( c ` Z ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
245	244	adantr 463	. . . . . . . . . . . . 13 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( C ` R ) ` k ) = ( ( C ` R ) ` ( J - ( c ` Z ) ) ) )
246	243, 245	eleq12d 2536	. . . . . . . . . . . 12 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( d e. ( ( C ` R ) ` k ) <-> ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) )
247	242, 246	anbi12d 708	. . . . . . . . . . 11 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) <-> ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) )
248	240, 247	anbi12d 708	. . . . . . . . . 10 |- ( ( k = ( J - ( c ` Z ) ) /\ d = ( c |` R ) ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) <-> ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) ) )
249	248	spc2egv 3193	. . . . . . . . 9 |- ( ( ( J - ( c ` Z ) ) e. _V /\ ( c |` R ) e. _V ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) -> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) ) )
250	235, 238, 249	syl2anc 659	. . . . . . . 8 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( c ` Z ) ) , ( c |` R ) >. /\ ( ( J - ( c ` Z ) ) e. ( 0 ... J ) /\ ( c |` R ) e. ( ( C ` R ) ` ( J - ( c ` Z ) ) ) ) ) -> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) ) )
251	234, 250	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 ) ) ) )
252		eliunxp 5129	. . . . . . 7 |- ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> E. k E. d ( <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. k , d >. /\ ( k e. ( 0 ... J ) /\ d e. ( ( C ` R ) ` k ) ) ) )
253	251, 252	sylibr 212	. . . . . 6 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
254		dvnprodlem1.d	. . . . . 6 |- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
255	253, 254	fmptd 6031	. . . . 5 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) --> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
256	95	nfcri 2609	. . . . . . . . . . . 12 |- F/ t e e. ( ( C ` ( R u. { Z } ) ) ` J )
257	96, 256	nfan 1933	. . . . . . . . . . 11 |- F/ t ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
258	79, 257	nfan 1933	. . . . . . . . . 10 |- F/ t ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
259		nfv 1712	. . . . . . . . . 10 |- F/ t ( D ` c ) = ( D ` e )
260	258, 259	nfan 1933	. . . . . . . . 9 |- F/ t ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) )
261	99	eqcomd 2462	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
262	261	adantlrr 718	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
263	262	adantlr 712	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( c ` t ) = ( ( c |` R ) ` t ) )
264	254	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
265		opex 4701	. . . . . . . . . . . . . . . . . . . 20 |- <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V
266	265	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V )
267	264, 266	fvmpt2d 5941	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
268	267	fveq2d 5852	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
269	268	fveq1d 5850	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) )
270		ovex 6298	. . . . . . . . . . . . . . . . . . 19 |- ( J - ( c ` Z ) ) e. _V
271	270, 237	op2nd 6782	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( c |` R )
272	271	fveq1i 5849	. . . . . . . . . . . . . . . . 17 |- ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t )
273	272	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( 2nd ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) ` t ) = ( ( c |` R ) ` t ) )
274	269, 273	eqtr2d 2496	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
275	274	adantrr 714	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
276	275	ad2antrr 723	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( c |` R ) ` t ) = ( ( 2nd ` ( D ` c ) ) ` t ) )
277		simpr 459	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = ( D ` e ) )
278	254	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
279		fveq1 5847	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c = e -> ( c ` Z ) = ( e ` Z ) )
280	279	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( J - ( c ` Z ) ) = ( J - ( e ` Z ) ) )
281		reseq1 5256	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( c |` R ) = ( e |` R ) )
282	280, 281	opeq12d 4211	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = e -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
283	282	adantl 464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ c = e ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
284		simpr 459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e e. ( ( C ` ( R u. { Z } ) ) ` J ) )
285		opex 4701	. . . . . . . . . . . . . . . . . . . . . . 23 |- <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V
286	285	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( e ` Z ) ) , ( e |` R ) >. e. _V )
287	278, 283, 284, 286	fvmptd 5936	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
288	287	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` e ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
289	277, 288	eqtrd 2495	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( D ` c ) = <. ( J - ( e ` Z ) ) , ( e |` R ) >. )
290	289	fveq2d 5852	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
291	290	adantlrl 717	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
292	291	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( 2nd ` ( D ` c ) ) = ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
293		ovex 6298	. . . . . . . . . . . . . . . . . 18 |- ( J - ( e ` Z ) ) e. _V
294		vex 3109	. . . . . . . . . . . . . . . . . . 19 |- e e. _V
295	294	resex 5305	. . . . . . . . . . . . . . . . . 18 |- ( e |` R ) e. _V
296	293, 295	op2nd 6782	. . . . . . . . . . . . . . . . 17 |- ( 2nd ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( e |` R )
297	296	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 ) )
298	292, 297	eqtrd 2495	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( 2nd ` ( D ` c ) ) = ( e |` R ) )
299	298	fveq1d 5850	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( ( e |` R ) ` t ) )
300		fvres 5862	. . . . . . . . . . . . . . 15 |- ( t e. R -> ( ( e |` R ) ` t ) = ( e ` t ) )
301	300	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( e |` R ) ` t ) = ( e ` t ) )
302	299, 301	eqtrd 2495	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( ( 2nd ` ( D ` c ) ) ` t ) = ( e ` t ) )
303	263, 276, 302	3eqtrd 2499	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. R ) -> ( c ` t ) = ( e ` t ) )
304	303	adantlr 712	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ t e. R ) -> ( c ` t ) = ( e ` t ) )
305		simpl 455	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) )
306		elunnel1 31654	. . . . . . . . . . . . . 14 |- ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t e. { Z } )
307		elsni 4041	. . . . . . . . . . . . . 14 |- ( t e. { Z } -> t = Z )
308	306, 307	syl 16	. . . . . . . . . . . . 13 |- ( ( t e. ( R u. { Z } ) /\ -. t e. R ) -> t = Z )
309	308	adantll 711	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t e. ( R u. { Z } ) ) /\ -. t e. R ) -> t = Z )
310		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> t = Z )
311	310	fveq2d 5852	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) /\ t = Z ) -> ( c ` t ) = ( c ` Z ) )
312	3	nn0cnd 10850	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> J e. CC )
313	312	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
314	313, 131	nncand 9927	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( c ` Z ) )
315	314	eqcomd 2462	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
316	315	adantrr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
317	316	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( c ` Z ) = ( J - ( J - ( c ` Z ) ) ) )
318	267	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) )
319	270, 237	op1st 6781	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) )
320	319	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` <. ( J - ( c ` Z ) ) , ( c |` R ) >. ) = ( J - ( c ` Z ) ) )
321	318, 320	eqtr2d 2496	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) = ( 1st ` ( D ` c ) ) )
322	321	oveq2d 6286	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
323	322	adantrr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
324	323	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( J - ( 1st ` ( D ` c ) ) ) )
325		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` c ) = ( D ` e ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
326	325	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( 1st ` ( D ` e ) ) )
327	287	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
328	327	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` e ) ) = ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) )
329	293, 295	op1st 6781	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) )
330	329	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` <. ( J - ( e ` Z ) ) , ( e |` R ) >. ) = ( J - ( e ` Z ) ) )
331	326, 328, 330	3eqtrd 2499	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( 1st ` ( D ` c ) ) = ( J - ( e ` Z ) ) )
332	331	oveq2d 6286	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( J - ( J - ( e ` Z ) ) ) )
333	312	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
334		zsscn 10868	. . . . . . . . . . . . . . . . . . . . . . 23 |- ZZ C_ CC
335	6, 334	sstri 3498	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 ... J ) C_ CC
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... J ) C_ CC )
337		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c = e -> ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) <-> e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) )
338	337	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) <-> ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) )
339		feq1 5695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( c = e -> ( c : ( R u. { Z } ) --> ( 0 ... J ) <-> e : ( R u. { Z } ) --> ( 0 ... J ) ) )
340	338, 339	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = e -> ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) ) <-> ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) ) ) )
341	340, 49	chvarv 2019	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> e : ( R u. { Z } ) --> ( 0 ... J ) )
342	54	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
343	341, 342	ffvelrnd 6008	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. ( 0 ... J ) )
344	336, 343	sseldd 3490	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( e ` Z ) e. CC )
345	333, 344	nncand 9927	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
346	345	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( J - ( e ` Z ) ) ) = ( e ` Z ) )
347		eqidd 2455	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( e ` Z ) = ( e ` Z ) )
348	332, 346, 347	3eqtrd 2499	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
349	348	adantlrl 717	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ e e. ( ( C ` ( R u. { Z } ) ) ` J ) ) ) /\ ( D ` c ) = ( D ` e ) ) -> ( J - ( 1st ` ( D ` c ) ) ) = ( e ` Z ) )
350	317, 324, 349	3eqtrd 2499	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( c e. (