Theorem dvnprodlem2 31983

Description: Induction step for dvnprodlem2 31983. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypotheses

Ref	Expression
dvnprodlem2.s	|- ( ph -> S e. { RR , CC } )
dvnprodlem2.x	|- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
dvnprodlem2.t	|- ( ph -> T e. Fin )
dvnprodlem2.h	|- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
dvnprodlem2.n	|- ( ph -> N e. NN0 )
dvnprodlem2.dvnh	|- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
dvnprodlem2.c	|- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
dvnprodlem2.r	|- ( ph -> R C_ T )
dvnprodlem2.z	|- ( ph -> Z e. ( T \ R ) )
dvnprodlem2.ind	|- ( ph -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
dvnprodlem2.j	|- ( ph -> J e. ( 0 ... N ) )
dvnprodlem2.d	|- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )

Assertion

Ref	Expression
dvnprodlem2	|- ( ph -> ( ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) ` J ) = ( x e. X |-> sum_ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( ( ! ` J ) / prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( R u. { Z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )

Distinct variable groups:   C, c, k, t   D, c, t   H, c, j, k, t   x, H, c, k, t   J, c, j, k, t   n, J, s, c, k, t   x, J   j, N, t   R, c, k, n, s, t   x, R   S, c, j, k, t   x, S   T, j, t   T, s   X, c, j, k, t   x, X   Z, c, j, k, t   n, Z, s   x, Z   ph, c, j, k, t   ph, n, s   ph, x

Allowed substitution hints:   C( x, j, n, s)   D( x, j, k, n, s)   R( j)   S( n, s)   T( x, k, n, c)   H( n, s)   N( x, k, n, s, c)   X( n, s)

Proof of Theorem dvnprodlem2

Dummy variables p y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1712	. . . . . 6 |- F/ t ( ph /\ x e. X )
2		nfcv 2616	. . . . . 6 |- F/_ t ( ( H ` Z ) ` x )
3		dvnprodlem2.t	. . . . . . . 8 |- ( ph -> T e. Fin )
4		dvnprodlem2.r	. . . . . . . 8 |- ( ph -> R C_ T )
5		ssfi 7733	. . . . . . . 8 |- ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
6	3, 4, 5	syl2anc 659	. . . . . . 7 |- ( ph -> R e. Fin )
7	6	adantr 463	. . . . . 6 |- ( ( ph /\ x e. X ) -> R e. Fin )
8		dvnprodlem2.z	. . . . . . 7 |- ( ph -> Z e. ( T \ R ) )
9	8	adantr 463	. . . . . 6 |- ( ( ph /\ x e. X ) -> Z e. ( T \ R ) )
10	8	eldifbd 3474	. . . . . . 7 |- ( ph -> -. Z e. R )
11	10	adantr 463	. . . . . 6 |- ( ( ph /\ x e. X ) -> -. Z e. R )
12		simpl 455	. . . . . . . . 9 |- ( ( ph /\ t e. R ) -> ph )
13	4	sselda 3489	. . . . . . . . 9 |- ( ( ph /\ t e. R ) -> t e. T )
14		dvnprodlem2.h	. . . . . . . . 9 |- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
15	12, 13, 14	syl2anc 659	. . . . . . . 8 |- ( ( ph /\ t e. R ) -> ( H ` t ) : X --> CC )
16	15	adantlr 712	. . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( H ` t ) : X --> CC )
17		simplr 753	. . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> x e. X )
18	16, 17	ffvelrnd 6008	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( ( H ` t ) ` x ) e. CC )
19		fveq2 5848	. . . . . . 7 |- ( t = Z -> ( H ` t ) = ( H ` Z ) )
20	19	fveq1d 5850	. . . . . 6 |- ( t = Z -> ( ( H ` t ) ` x ) = ( ( H ` Z ) ` x ) )
21		id 22	. . . . . . . . 9 |- ( ph -> ph )
22		eldifi 3612	. . . . . . . . . 10 |- ( Z e. ( T \ R ) -> Z e. T )
23	8, 22	syl 16	. . . . . . . . 9 |- ( ph -> Z e. T )
24		simpr 459	. . . . . . . . . 10 |- ( ( ph /\ Z e. T ) -> Z e. T )
25		id 22	. . . . . . . . . 10 |- ( ( ph /\ Z e. T ) -> ( ph /\ Z e. T ) )
26		eleq1 2526	. . . . . . . . . . . . 13 |- ( t = Z -> ( t e. T <-> Z e. T ) )
27	26	anbi2d 701	. . . . . . . . . . . 12 |- ( t = Z -> ( ( ph /\ t e. T ) <-> ( ph /\ Z e. T ) ) )
28	19	feq1d 5699	. . . . . . . . . . . 12 |- ( t = Z -> ( ( H ` t ) : X --> CC <-> ( H ` Z ) : X --> CC ) )
29	27, 28	imbi12d 318	. . . . . . . . . . 11 |- ( t = Z -> ( ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC ) <-> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) ) )
30	29, 14	vtoclg 3164	. . . . . . . . . 10 |- ( Z e. T -> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) )
31	24, 25, 30	sylc 60	. . . . . . . . 9 |- ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC )
32	21, 23, 31	syl2anc 659	. . . . . . . 8 |- ( ph -> ( H ` Z ) : X --> CC )
33	32	adantr 463	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( H ` Z ) : X --> CC )
34		simpr 459	. . . . . . 7 |- ( ( ph /\ x e. X ) -> x e. X )
35	33, 34	ffvelrnd 6008	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( H ` Z ) ` x ) e. CC )
36	1, 2, 7, 9, 11, 18, 20, 35	fprodsplitsn 31831	. . . . 5 |- ( ( ph /\ x e. X ) -> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) = ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) )
37	36	mpteq2dva 4525	. . . 4 |- ( ph -> ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) = ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) )
38	37	oveq2d 6286	. . 3 |- ( ph -> ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) = ( S Dn ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) ) )
39	38	fveq1d 5850	. 2 |- ( ph -> ( ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) ` J ) = ( ( S Dn ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) ) ` J ) )
40		dvnprodlem2.s	. . 3 |- ( ph -> S e. { RR , CC } )
41		dvnprodlem2.x	. . 3 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
42	1, 7, 18	fprodclf 31834	. . 3 |- ( ( ph /\ x e. X ) -> prod_ t e. R ( ( H ` t ) ` x ) e. CC )
43		dvnprodlem2.j	. . . 4 |- ( ph -> J e. ( 0 ... N ) )
44		elfznn0 11775	. . . 4 |- ( J e. ( 0 ... N ) -> J e. NN0 )
45	43, 44	syl 16	. . 3 |- ( ph -> J e. NN0 )
46		eqid 2454	. . 3 |- ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) )
47		eqid 2454	. . 3 |- ( x e. X |-> ( ( H ` Z ) ` x ) ) = ( x e. X |-> ( ( H ` Z ) ` x ) )
48		dvnprodlem2.c	. . . . . . . . . . 11 |- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
49	48	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) ) )
50		oveq2 6278	. . . . . . . . . . . . . 14 |- ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
51		rabeq 3100	. . . . . . . . . . . . . 14 |- ( ( ( 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 } )
52	50, 51	syl 16	. . . . . . . . . . . . 13 |- ( 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 } )
53		sumeq1 13593	. . . . . . . . . . . . . . 15 |- ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
54	53	eqeq1d 2456	. . . . . . . . . . . . . 14 |- ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
55	54	rabbidv 3098	. . . . . . . . . . . . 13 |- ( 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 } )
56	52, 55	eqtrd 2495	. . . . . . . . . . . 12 |- ( 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 } )
57	56	mpteq2dv 4526	. . . . . . . . . . 11 |- ( 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 } ) )
58	57	adantl 464	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ 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 } ) )
59		ssexg 4583	. . . . . . . . . . . . . 14 |- ( ( R C_ T /\ T e. Fin ) -> R e. _V )
60	4, 3, 59	syl2anc 659	. . . . . . . . . . . . 13 |- ( ph -> R e. _V )
61		elpwg 4007	. . . . . . . . . . . . 13 |- ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
62	60, 61	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( R e. ~P T <-> R C_ T ) )
63	4, 62	mpbird 232	. . . . . . . . . . 11 |- ( ph -> R e. ~P T )
64	63	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> R e. ~P T )
65		nn0ex 10797	. . . . . . . . . . . 12 |- NN0 e. _V
66	65	mptex 6118	. . . . . . . . . . 11 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
67	66	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
68	49, 58, 64, 67	fvmptd 5936	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
69		oveq2 6278	. . . . . . . . . . . . 13 |- ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
70	69	oveq1d 6285	. . . . . . . . . . . 12 |- ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
71		rabeq 3100	. . . . . . . . . . . 12 |- ( ( ( 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 } )
72	70, 71	syl 16	. . . . . . . . . . 11 |- ( 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 } )
73		eqeq2 2469	. . . . . . . . . . . 12 |- ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
74	73	rabbidv 3098	. . . . . . . . . . 11 |- ( 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 } )
75	72, 74	eqtrd 2495	. . . . . . . . . 10 |- ( 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 } )
76	75	adantl 464	. . . . . . . . 9 |- ( ( ( 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 } )
77		elfznn0 11775	. . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k e. NN0 )
78	77	adantl 464	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
79		fzfid 12065	. . . . . . . . . . . 12 |- ( ph -> ( 0 ... k ) e. Fin )
80		mapfi 7808	. . . . . . . . . . . 12 |- ( ( ( 0 ... k ) e. Fin /\ R e. Fin ) -> ( ( 0 ... k ) ^m R ) e. Fin )
81	79, 6, 80	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( ( 0 ... k ) ^m R ) e. Fin )
82	81	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 ... k ) ^m R ) e. Fin )
83		ssrab2 3571	. . . . . . . . . . 11 |- { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R )
84	83	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R ) )
85	82, 84	ssexd 4584	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
86	68, 76, 78, 85	fvmptd 5936	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
87		ssfi 7733	. . . . . . . . . 10 |- ( ( ( ( 0 ... k ) ^m R ) e. Fin /\ { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
88	81, 83, 87	sylancl 660	. . . . . . . . 9 |- ( ph -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
89	88	adantr 463	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
90	86, 89	eqeltrd 2542	. . . . . . 7 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) e. Fin )
91	90	adantr 463	. . . . . 6 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) -> ( ( C ` R ) ` k ) e. Fin )
92	77	faccld 31755	. . . . . . . . . . 11 |- ( k e. ( 0 ... J ) -> ( ! ` k ) e. NN )
93	92	nncnd 10547	. . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> ( ! ` k ) e. CC )
94	93	ad2antlr 724	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ! ` k ) e. CC )
95	6	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
96	95	adantlr 712	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
97		elfznn0 11775	. . . . . . . . . . . . . . 15 |- ( z e. ( 0 ... k ) -> z e. NN0 )
98	97	ssriv 3493	. . . . . . . . . . . . . 14 |- ( 0 ... k ) C_ NN0
99	98	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ NN0 )
100		simpr 459	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( C ` R ) ` k ) )
101	86	eleq2d 2524	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( c e. ( ( C ` R ) ` k ) <-> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) )
102	101	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( c e. ( ( C ` R ) ` k ) <-> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) )
103	100, 102	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
104	83	sseli 3485	. . . . . . . . . . . . . . . . 17 |- ( c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> c e. ( ( 0 ... k ) ^m R ) )
105	103, 104	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( 0 ... k ) ^m R ) )
106		elmapi 7433	. . . . . . . . . . . . . . . 16 |- ( c e. ( ( 0 ... k ) ^m R ) -> c : R --> ( 0 ... k ) )
107	105, 106	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c : R --> ( 0 ... k ) )
108	107	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> c : R --> ( 0 ... k ) )
109		simpr 459	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. R )
110	108, 109	ffvelrnd 6008	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... k ) )
111	99, 110	sseldd 3490	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. NN0 )
112	111	faccld 31755	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. NN )
113	112	nncnd 10547	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. CC )
114	96, 113	fprodcl 13841	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. CC )
115	112	nnne0d 10576	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) =/= 0 )
116	96, 113, 115	fprodn0 13865	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
117	94, 114, 116	divcld 10316	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
118	117	adantlr 712	. . . . . . 7 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
119	96	adantlr 712	. . . . . . . 8 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
120	21	ad4antr 729	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ph )
121	120, 13	sylancom 665	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. T )
122		elfzuz3 11688	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> J e. ( ZZ>= ` k ) )
123		fzss2 11727	. . . . . . . . . . . . . . . 16 |- ( J e. ( ZZ>= ` k ) -> ( 0 ... k ) C_ ( 0 ... J ) )
124	122, 123	syl 16	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 ... k ) C_ ( 0 ... J ) )
125	124	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... J ) )
126	45	nn0zd 10963	. . . . . . . . . . . . . . . . . 18 |- ( ph -> J e. ZZ )
127		dvnprodlem2.n	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. NN0 )
128	127	nn0zd 10963	. . . . . . . . . . . . . . . . . 18 |- ( ph -> N e. ZZ )
129		elfzle2 11693	. . . . . . . . . . . . . . . . . . 19 |- ( J e. ( 0 ... N ) -> J <_ N )
130	43, 129	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> J <_ N )
131	126, 128, 130	3jca 1174	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
132		eluz2 11088	. . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` J ) <-> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
133	131, 132	sylibr 212	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. ( ZZ>= ` J ) )
134		fzss2 11727	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` J ) -> ( 0 ... J ) C_ ( 0 ... N ) )
135	133, 134	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( 0 ... J ) C_ ( 0 ... N ) )
136	135	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... J ) C_ ( 0 ... N ) )
137	125, 136	sstrd 3499	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... N ) )
138	137	ad2antrr 723	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ ( 0 ... N ) )
139	138, 110	sseldd 3490	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
140	139	adantllr 716	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
141		fvex 5858	. . . . . . . . . . 11 |- ( c ` t ) e. _V
142		eleq1 2526	. . . . . . . . . . . . 13 |- ( j = ( c ` t ) -> ( j e. ( 0 ... N ) <-> ( c ` t ) e. ( 0 ... N ) ) )
143	142	3anbi3d 1303	. . . . . . . . . . . 12 |- ( j = ( c ` t ) -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) ) )
144		fveq2 5848	. . . . . . . . . . . . 13 |- ( j = ( c ` t ) -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
145	144	feq1d 5699	. . . . . . . . . . . 12 |- ( j = ( c ` t ) -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC ) )
146	143, 145	imbi12d 318	. . . . . . . . . . 11 |- ( j = ( c ` t ) -> ( ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC ) <-> ( ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC ) ) )
147		dvnprodlem2.dvnh	. . . . . . . . . . 11 |- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
148	141, 146, 147	vtocl 3158	. . . . . . . . . 10 |- ( ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
149	120, 121, 140, 148	syl3anc 1226	. . . . . . . . 9 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
150		simpllr 758	. . . . . . . . 9 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> x e. X )
151	149, 150	ffvelrnd 6008	. . . . . . . 8 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
152	119, 151	fprodcl 13841	. . . . . . 7 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
153	118, 152	mulcld 9605	. . . . . 6 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
154	91, 153	fsumcl 13637	. . . . 5 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) -> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
155		eqid 2454	. . . . 5 |- ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
156	154, 155	fmptd 6031	. . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) : X --> CC )
157		dvnprodlem2.ind	. . . . . . 7 |- ( ph -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
158	157	adantr 463	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... J ) ) -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
159		0zd 10872	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> 0 e. ZZ )
160	128	adantr 463	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> N e. ZZ )
161		elfzelz 11691	. . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k e. ZZ )
162	161	adantl 464	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. ZZ )
163	159, 160, 162	3jca 1174	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
164		elfzle1 11692	. . . . . . . . 9 |- ( k e. ( 0 ... J ) -> 0 <_ k )
165	164	adantl 464	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> 0 <_ k )
166	162	zred 10965	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. RR )
167	45	nn0red 10849	. . . . . . . . . 10 |- ( ph -> J e. RR )
168	167	adantr 463	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J e. RR )
169	160	zred 10965	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> N e. RR )
170		elfzle2 11693	. . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k <_ J )
171	170	adantl 464	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k <_ J )
172	130	adantr 463	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J <_ N )
173	166, 168, 169, 171, 172	letrd 9728	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k <_ N )
174	163, 165, 173	jca32 533	. . . . . . 7 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
175		elfz2 11682	. . . . . . 7 |- ( k e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
176	174, 175	sylibr 212	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. ( 0 ... N ) )
177		rspa 2821	. . . . . 6 |- ( ( A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
178	158, 176, 177	syl2anc 659	. . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
179	178	feq1d 5699	. . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) : X --> CC <-> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) : X --> CC ) )
180	156, 179	mpbird 232	. . 3 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) : X --> CC )
181	23	adantr 463	. . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> Z e. T )
182		simpl 455	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ph )
183	182, 181, 176	3jca 1174	. . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) )
184	26	3anbi2d 1302	. . . . . . 7 |- ( t = Z -> ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) <-> ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) ) )
185	19	oveq2d 6286	. . . . . . . . 9 |- ( t = Z -> ( S Dn ( H ` t ) ) = ( S Dn ( H ` Z ) ) )
186	185	fveq1d 5850	. . . . . . . 8 |- ( t = Z -> ( ( S Dn ( H ` t ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
187	186	feq1d 5699	. . . . . . 7 |- ( t = Z -> ( ( ( S Dn ( H ` t ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
188	184, 187	imbi12d 318	. . . . . 6 |- ( t = Z -> ( ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC ) <-> ( ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) ) )
189		eleq1 2526	. . . . . . . . 9 |- ( j = k -> ( j e. ( 0 ... N ) <-> k e. ( 0 ... N ) ) )
190	189	3anbi3d 1303	. . . . . . . 8 |- ( j = k -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ k e. ( 0 ... N ) ) ) )
191		fveq2 5848	. . . . . . . . 9 |- ( j = k -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` k ) )
192	191	feq1d 5699	. . . . . . . 8 |- ( j = k -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC ) )
193	190, 192	imbi12d 318	. . . . . . 7 |- ( j = k -> ( ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC ) <-> ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC ) ) )
194	193, 147	chvarv 2019	. . . . . 6 |- ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC )
195	188, 194	vtoclg 3164	. . . . 5 |- ( Z e. T -> ( ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
196	181, 183, 195	sylc 60	. . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC )
197	32	feqmptd 5901	. . . . . . . . 9 |- ( ph -> ( H ` Z ) = ( x e. X |-> ( ( H ` Z ) ` x ) ) )
198	197	eqcomd 2462	. . . . . . . 8 |- ( ph -> ( x e. X |-> ( ( H ` Z ) ` x ) ) = ( H ` Z ) )
199	198	oveq2d 6286	. . . . . . 7 |- ( ph -> ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) = ( S Dn ( H ` Z ) ) )
200	199	fveq1d 5850	. . . . . 6 |- ( ph -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
201	200	adantr 463	. . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
202	201	feq1d 5699	. . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
203	196, 202	mpbird 232	. . 3 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) : X --> CC )
204		fveq2 5848	. . . . . . . 8 |- ( y = x -> ( ( H ` t ) ` y ) = ( ( H ` t ) ` x ) )
205	204	prodeq2ad 31829	. . . . . . 7 |- ( y = x -> prod_ t e. R ( ( H ` t ) ` y ) = prod_ t e. R ( ( H ` t ) ` x ) )
206	205	cbvmptv 4530	. . . . . 6 |- ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) = ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) )
207	206	oveq2i 6281	. . . . 5 |- ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) = ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) )
208	207	fveq1i 5849	. . . 4 |- ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) = ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k )
209	208	mpteq2i 4522	. . 3 |- ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) = ( k e. ( 0 ... J ) |-> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) )
210		fveq2 5848	. . . . . . 7 |- ( y = x -> ( ( H ` Z ) ` y ) = ( ( H ` Z ) ` x ) )
211	210	cbvmptv 4530	. . . . . 6 |- ( y e. X |-> ( ( H ` Z ) ` y ) ) = ( x e. X |-> ( ( H ` Z ) ` x ) )
212	211	oveq2i 6281	. . . . 5 |- ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) = ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) )
213	212	fveq1i 5849	. . . 4 |- ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k )
214	213	mpteq2i 4522	. . 3 |- ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( k e. ( 0 ... J ) |-> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) )
215	40, 41, 42, 35, 45, 46, 47, 180, 203, 209, 214	dvnmul 31979	. 2 |- ( ph -> ( ( S Dn ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) ) ` J ) = ( x e. X |-> sum_ k e. ( 0 ... J ) ( ( J _C k ) x. ( ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) x. ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) ) ) ) )
216	208	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) = ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) )
217	157	r19.21bi 2823	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
218	182, 176, 217	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
219	216, 218	eqtrd 2495	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
220	219	mpteq2dva 4525	. . . . . . . . . . . 12 |- ( ph -> ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) = ( k e. ( 0 ... J ) |-> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ) )
221		mptexg 6117	. . . . . . . . . . . . . 14 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) e. _V )
222	41, 221	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) e. _V )
223	222	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) e. _V )
224	220, 223	fvmpt2d 5941	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
225	224	adantlr 712	. . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
226	225	fveq1d 5850	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) = ( ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ` x ) )
227	34	adantr 463	. . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> x e. X )
228	154	an32s 802	. . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
229	155	fvmpt2 5939	. . . . . . . . . 10 |- ( ( x e. X /\ sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC ) -> ( ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ` x ) = sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
230	227, 228, 229	syl2anc 659	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ` x ) = sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
231	226, 230	eqtrd 2495	. . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) = sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
232		fveq2 5848	. . . . . . . . . . . . . . 15 |- ( k = j -> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) = ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) )
233	232	cbvmptv 4530	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) )
234	233	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) ) )
235	212, 199	syl5eq 2507	. . . . . . . . . . . . . . 15 |- ( ph -> ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) = ( S Dn ( H ` Z ) ) )
236	235	fveq1d 5850	. . . . . . . . . . . . . 14 |- ( ph -> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` j ) )
237	236	mpteq2dv 4526	. . . . . . . . . . . . 13 |- ( ph -> ( j e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( H ` Z ) ) ` j ) ) )
238	234, 237	eqtrd 2495	. . . . . . . . . . . 12 |- ( ph -> ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( H ` Z ) ) ` j ) ) )
239	238	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( H ` Z ) ) ` j ) ) )
240		fveq2 5848	. . . . . . . . . . . 12 |- ( j = ( J - k ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
241	240	adantl 464	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ j = ( J - k ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
242		0zd 10872	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> 0 e. ZZ )
243		elfzel2 11689	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> J e. ZZ )
244	243, 161	zsubcld 10970	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( J - k ) e. ZZ )
245	242, 243, 244	3jca 1174	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) )
246	243	zred 10965	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> J e. RR )
247	77	nn0red 10849	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> k e. RR )
248	246, 247	subge0d 10138	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 <_ ( J - k ) <-> k <_ J ) )
249	170, 248	mpbird 232	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> 0 <_ ( J - k ) )
250	246, 247	subge02d 10140	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 <_ k <-> ( J - k ) <_ J ) )
251	164, 250	mpbid 210	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> ( J - k ) <_ J )
252	245, 249, 251	jca32 533	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... J ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
253	252	adantl 464	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
254		elfz2 11682	. . . . . . . . . . . 12 |- ( ( J - k ) e. ( 0 ... J ) <-> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
255	253, 254	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J - k ) e. ( 0 ... J ) )
256		fvex 5858	. . . . . . . . . . . 12 |- ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) e. _V
257	256	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) e. _V )
258	239, 241, 255, 257	fvmptd 5936	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
259	258	adantlr 712	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
260	259	fveq1d 5850	. . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) )
261	231, 260	oveq12d 6288	. . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) x. ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) ) = ( sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) )
262	261	oveq2d 6286	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( J _C k ) x. ( ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) x. ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) ) ) = ( ( J _C k ) x. ( sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
263	90	adantlr 712	. . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) e. Fin )
264		ovex 6298	. . . . . . . . . . . 12 |- ( J - k ) e. _V
265		eleq1 2526	. . . . . . . . . . . . . 14 |- ( j = ( J - k ) -> ( j e. ( 0 ... J ) <-> ( J - k ) e. ( 0 ... J ) ) )
266	265	anbi2d 701	. . . . . . . . . . . . 13 |- ( j = ( J - k ) -> ( ( ph /\ j e. ( 0 ... J ) ) <-> ( ph /\ ( J - k ) e. ( 0 ... J ) ) ) )
267	240	feq1d 5699	. . . . . . . . . . . . 13 |- ( j = ( J - k ) -> ( ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC ) )
268	266, 267	imbi12d 318	. . . . . . . . . . . 12 |- ( j = ( J - k ) -> ( ( ( ph /\ j e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) <-> ( ( ph /\ ( J - k ) e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC ) ) )
269		eleq1 2526	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. ( 0 ... J ) <-> j e. ( 0 ... J ) ) )
270	269	anbi2d 701	. . . . . . . . . . . . . 14 |- ( k = j -> ( ( ph /\ k e. ( 0 ... J ) ) <-> ( ph /\ j e. ( 0 ... J ) ) ) )
271		fveq2 5848	. . . . . . . . . . . . . . 15 |- ( k = j -> ( ( S Dn ( H ` Z ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` j ) )
272	271	feq1d 5699	. . . . . . . . . . . . . 14 |- ( k = j -> ( ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) )
273	270, 272	imbi12d 318	. . . . . . . . . . . . 13 |- ( k = j -> ( ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) ) )
274	273, 196	chvarv 2019	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC )
275	264, 268, 274	vtocl 3158	. . . . . . . . . . 11 |- ( ( ph /\ ( J - k ) e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
276	182, 255, 275	syl2anc 659	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
277	276	adantlr 712	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
278	277, 227	ffvelrnd 6008	. . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) e. CC )
279		anass 647	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) <-> ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) )
280		ancom 448	. . . . . . . . . . . . . 14 |- ( ( k e. ( 0 ... J ) /\ x e. X ) <-> ( x e. X /\ k e. ( 0 ... J ) ) )
281	280	anbi2i 692	. . . . . . . . . . . . 13 |- ( ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) <-> ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) )
282		anass 647	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) <-> ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) )
283	282	bicomi 202	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
284	281, 283	bitri 249	. . . . . . . . . . . 12 |- ( ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
285	279, 284	bitri 249	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
286	285	anbi1i 693	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) <-> ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) )
287	286	imbi1i 323	. . . . . . . . 9 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC ) <-> ( ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC ) )
288	153, 287	mpbi 208	. . . . . . . 8 |- ( ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
289	263, 278, 288	fsummulc1 13682	. . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) = sum_ c e. ( ( C ` R ) ` k ) ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) )
290	289	oveq2d 6286	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( J _C k ) x. ( sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) = ( ( J _C k ) x. sum_ c e. ( ( C ` R ) ` k ) ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
291	182, 45	syl 16	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J e. NN0 )
292	291, 162	bccld 31759	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. NN0 )
293	292	nn0cnd 10850	. . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. CC )
294	293	adantlr 712	. . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. CC )
295	278	adantr 463	. . . . . . . 8 |- ( ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) e. CC )
296	288, 295	mulcld 9605	. . . . . . 7 |- ( ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) e. CC )
297	263, 294, 296	fsummulc2 13681	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( J _C k ) x. sum_ c e. ( ( C ` R ) ` k ) ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) = sum_ c e. ( ( C ` R ) ` k ) ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
298	262, 290, 297	3eqtrd 2499	. . . . 5 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( J _C k ) x. ( ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) x. ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) ) ) = sum_ c e. ( ( C ` R ) ` k ) ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
299	298	sumeq2dv 13607	. . . 4 |- ( ( ph /\ x e. X ) -> sum_ k e. ( 0 ... J ) ( ( J _C k ) x. ( ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) ` k ) ) ` k ) ` x ) x. ( ( ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) ` ( J - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... J ) sum_ c e. ( ( C ` R ) ` k ) ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
300		vex 3109	. . . . . . . 8 |- k e. _V
301		vex 3109	. . . . . . . 8 |- c e. _V
302	300, 301	op1std 6783	. . . . . . 7 |- ( p = <. k , c >. -> ( 1st ` p ) = k )
303	302	oveq2d 6286	. . . . . 6 |- ( p = <. k , c >. -> ( J _C ( 1st ` p ) ) = ( J _C k ) )
304	302	fveq2d 5852	. . . . . . . . 9 |- ( p = <. k , c >. -> ( ! ` ( 1st ` p ) ) = ( ! ` k ) )
305	300, 301	op2ndd 6784	. . . . . . . . . . . 12 |- ( p = <. k , c >. -> ( 2nd ` p ) = c )
306	305	fveq1d 5850	. . . . . . . . . . 11 |- ( p = <. k , c >. -> ( ( 2nd ` p ) ` t ) = ( c ` t ) )
307	306	fveq2d 5852	. . . . . . . . . 10 |- ( p = <. k , c >. -> ( ! ` ( ( 2nd ` p ) ` t ) ) = ( ! ` ( c ` t ) ) )
308	307	prodeq2ad 31829	. . . . . . . . 9 |- ( p = <. k , c >. -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) = prod_ t e. R ( ! ` ( c ` t ) ) )
309	304, 308	oveq12d 6288	. . . . . . . 8 |- ( p = <. k , c >. -> ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) = ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) )
310	306	fveq2d 5852	. . . . . . . . . 10 |- ( p = <. k , c >. -> ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
311	310	fveq1d 5850	. . . . . . . . 9 |- ( p = <. k , c >. -> ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
312	311	prodeq2ad 31829	. . . . . . . 8 |- ( p = <. k , c >. -> prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) = prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
313	309, 312	oveq12d 6288	. . . . . . 7 |- ( p = <. k , c >. -> ( ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) ) = ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
314	302	oveq2d 6286	. . . . . . . . 9 |- ( p = <. k , c >. -> ( J - ( 1st ` p ) ) = ( J - k ) )
315	314	fveq2d 5852	. . . . . . . 8 |- ( p = <. k , c >. -> ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
316	315	fveq1d 5850	. . . . . . 7 |- ( p = <. k , c >. -> ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) )
317	313, 316	oveq12d 6288	. . . . . 6 |- ( p = <. k , c >. -> ( ( ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) ) = ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) )
318	303, 317	oveq12d 6288	. . . . 5 |- ( p = <. k , c >. -> ( ( J _C ( 1st ` p ) ) x. ( ( ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) ) ) = ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) )
319		fzfid 12065	. . . . 5 |- ( ( ph /\ x e. X ) -> ( 0 ... J ) e. Fin )
320	294	adantrr 714	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ ( k e. ( 0 ... J ) /\ c e. ( ( C ` R ) ` k ) ) ) -> ( J _C k ) e. CC )
321	296	anasss 645	. . . . . 6 |- ( ( ( ph /\ x e. X ) /\ ( k e. ( 0 ... J ) /\ c e. ( ( C ` R ) ` k ) ) ) -> ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) e. CC )
322	320, 321	mulcld 9605	. . . . 5 |- ( ( ( ph /\ x e. X ) /\ ( k e. ( 0 ... J ) /\ c e. ( ( C ` R ) ` k ) ) ) -> ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) e. CC )
323	318, 319, 263, 322	fsum2d 13668	. . . 4 |- ( ( ph /\ x e. X ) -> sum_ k e. ( 0 ... J ) sum_ c e. ( ( C ` R ) ` k ) ( ( J _C k ) x. ( ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) ) ) = sum_ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ( ( J _C ( 1st ` p ) ) x. ( ( ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) ) x. ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) ) ) )
324		ovex 6298	. . . . . . . . 9 |- ( J - ( c ` Z ) ) e. _V
325	301	resex 5305	. . . . . . . . 9 |- ( c |`