Theorem fprod2dlem 27655

Description: Lemma for fprod2d 27656- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)

Hypotheses

Ref	Expression
fprod2d.1	|- ( z = <. j , k >. -> D = C )
fprod2d.2	|- ( ph -> A e. Fin )
fprod2d.3	|- ( ( ph /\ j e. A ) -> B e. Fin )
fprod2d.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
fprod2d.5	|- ( ph -> -. y e. x )
fprod2d.6	|- ( ph -> ( x u. { y } ) C_ A )
fprod2d.7	|- ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )

Assertion

Ref	Expression
fprod2dlem	|- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )

Distinct variable groups:   A, j, k   B, k, z   z, C   D, j, k   ph, j   x, j   y, j, z   ph, k   x, k   y, k, z   ph, z   x, z   y, z

Allowed substitution hints:   ph( x, y)   ps( x, y, z, j, k)   A( x, y, z)   B( x, y, j)   C( x, y, j, k)   D( x, y, z)

Proof of Theorem fprod2dlem

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 461	. . . 4 |- ( ( ph /\ ps ) -> ps )
2		fprod2d.7	. . . 4 |- ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
3	1, 2	sylib 196	. . 3 |- ( ( ph /\ ps ) -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
4		nfcv 2616	. . . . . 6 |- F/_ m prod_ k e. B C
5		nfcsb1v 3414	. . . . . . 7 |- F/_ j [_ m / j ]_ B
6		nfcsb1v 3414	. . . . . . 7 |- F/_ j [_ m / j ]_ C
7	5, 6	nfcprod 27588	. . . . . 6 |- F/_ j prod_ k e. [_ m / j ]_ B [_ m / j ]_ C
8		csbeq1a 3407	. . . . . . 7 |- ( j = m -> B = [_ m / j ]_ B )
9		csbeq1a 3407	. . . . . . . 8 |- ( j = m -> C = [_ m / j ]_ C )
10	9	adantr 465	. . . . . . 7 |- ( ( j = m /\ k e. B ) -> C = [_ m / j ]_ C )
11	8, 10	prodeq12dv 27603	. . . . . 6 |- ( j = m -> prod_ k e. B C = prod_ k e. [_ m / j ]_ B [_ m / j ]_ C )
12	4, 7, 11	cbvprodi 27594	. . . . 5 |- prod_ j e. { y } prod_ k e. B C = prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C
13		fprod2d.6	. . . . . . . . 9 |- ( ph -> ( x u. { y } ) C_ A )
14	13	unssbd 3645	. . . . . . . 8 |- ( ph -> { y } C_ A )
15		vex 3081	. . . . . . . . 9 |- y e. _V
16	15	snss 4110	. . . . . . . 8 |- ( y e. A <-> { y } C_ A )
17	14, 16	sylibr 212	. . . . . . 7 |- ( ph -> y e. A )
18		fprod2d.3	. . . . . . . . . 10 |- ( ( ph /\ j e. A ) -> B e. Fin )
19	18	ralrimiva 2830	. . . . . . . . 9 |- ( ph -> A. j e. A B e. Fin )
20		nfcsb1v 3414	. . . . . . . . . . 11 |- F/_ j [_ y / j ]_ B
21	20	nfel1 2632	. . . . . . . . . 10 |- F/ j [_ y / j ]_ B e. Fin
22		csbeq1a 3407	. . . . . . . . . . 11 |- ( j = y -> B = [_ y / j ]_ B )
23	22	eleq1d 2523	. . . . . . . . . 10 |- ( j = y -> ( B e. Fin <-> [_ y / j ]_ B e. Fin ) )
24	21, 23	rspc 3173	. . . . . . . . 9 |- ( y e. A -> ( A. j e. A B e. Fin -> [_ y / j ]_ B e. Fin ) )
25	17, 19, 24	sylc 60	. . . . . . . 8 |- ( ph -> [_ y / j ]_ B e. Fin )
26		fprod2d.4	. . . . . . . . . . 11 |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
27	26	ralrimivva 2914	. . . . . . . . . 10 |- ( ph -> A. j e. A A. k e. B C e. CC )
28		nfcsb1v 3414	. . . . . . . . . . . . 13 |- F/_ j [_ y / j ]_ C
29	28	nfel1 2632	. . . . . . . . . . . 12 |- F/ j [_ y / j ]_ C e. CC
30	20, 29	nfral 2888	. . . . . . . . . . 11 |- F/ j A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC
31		csbeq1a 3407	. . . . . . . . . . . . 13 |- ( j = y -> C = [_ y / j ]_ C )
32	31	eleq1d 2523	. . . . . . . . . . . 12 |- ( j = y -> ( C e. CC <-> [_ y / j ]_ C e. CC ) )
33	22, 32	raleqbidv 3037	. . . . . . . . . . 11 |- ( j = y -> ( A. k e. B C e. CC <-> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
34	30, 33	rspc 3173	. . . . . . . . . 10 |- ( y e. A -> ( A. j e. A A. k e. B C e. CC -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
35	17, 27, 34	sylc 60	. . . . . . . . 9 |- ( ph -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
36	35	r19.21bi 2920	. . . . . . . 8 |- ( ( ph /\ k e. [_ y / j ]_ B ) -> [_ y / j ]_ C e. CC )
37	25, 36	fprodcl 27629	. . . . . . 7 |- ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
38		csbeq1 3401	. . . . . . . . 9 |- ( m = y -> [_ m / j ]_ B = [_ y / j ]_ B )
39		csbeq1 3401	. . . . . . . . . 10 |- ( m = y -> [_ m / j ]_ C = [_ y / j ]_ C )
40	39	adantr 465	. . . . . . . . 9 |- ( ( m = y /\ k e. [_ m / j ]_ B ) -> [_ m / j ]_ C = [_ y / j ]_ C )
41	38, 40	prodeq12dv 27603	. . . . . . . 8 |- ( m = y -> prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
42	41	prodsn 27637	. . . . . . 7 |- ( ( y e. A /\ prod_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
43	17, 37, 42	syl2anc 661	. . . . . 6 |- ( ph -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
44		nfcv 2616	. . . . . . . 8 |- F/_ m [_ y / j ]_ C
45		nfcsb1v 3414	. . . . . . . 8 |- F/_ k [_ m / k ]_ [_ y / j ]_ C
46		csbeq1a 3407	. . . . . . . 8 |- ( k = m -> [_ y / j ]_ C = [_ m / k ]_ [_ y / j ]_ C )
47	44, 45, 46	cbvprodi 27594	. . . . . . 7 |- prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C
48		csbeq1 3401	. . . . . . . . 9 |- ( m = ( 2nd ` z ) -> [_ m / k ]_ [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
49		snfi 7503	. . . . . . . . . 10 |- { y } e. Fin
50		xpfi 7697	. . . . . . . . . 10 |- ( ( { y } e. Fin /\ [_ y / j ]_ B e. Fin ) -> ( { y } X. [_ y / j ]_ B ) e. Fin )
51	49, 25, 50	sylancr 663	. . . . . . . . 9 |- ( ph -> ( { y } X. [_ y / j ]_ B ) e. Fin )
52		2ndconst 6775	. . . . . . . . . 10 |- ( y e. A -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
53	17, 52	syl 16	. . . . . . . . 9 |- ( ph -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
54		fvres 5816	. . . . . . . . . 10 |- ( z e. ( { y } X. [_ y / j ]_ B ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
55	54	adantl 466	. . . . . . . . 9 |- ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
56	45	nfel1 2632	. . . . . . . . . . 11 |- F/ k [_ m / k ]_ [_ y / j ]_ C e. CC
57	46	eleq1d 2523	. . . . . . . . . . 11 |- ( k = m -> ( [_ y / j ]_ C e. CC <-> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
58	56, 57	rspc 3173	. . . . . . . . . 10 |- ( m e. [_ y / j ]_ B -> ( A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC -> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
59	35, 58	mpan9 469	. . . . . . . . 9 |- ( ( ph /\ m e. [_ y / j ]_ B ) -> [_ m / k ]_ [_ y / j ]_ C e. CC )
60	48, 51, 53, 55, 59	fprodf1o 27623	. . . . . . . 8 |- ( ph -> prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
61		elxp 4968	. . . . . . . . . . . 12 |- ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) )
62		nfv 1674	. . . . . . . . . . . . . . 15 |- F/ j z = <. m , k >.
63		nfv 1674	. . . . . . . . . . . . . . . 16 |- F/ j m e. { y }
64	20	nfcri 2609	. . . . . . . . . . . . . . . 16 |- F/ j k e. [_ y / j ]_ B
65	63, 64	nfan 1866	. . . . . . . . . . . . . . 15 |- F/ j ( m e. { y } /\ k e. [_ y / j ]_ B )
66	62, 65	nfan 1866	. . . . . . . . . . . . . 14 |- F/ j ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
67	66	nfex 1886	. . . . . . . . . . . . 13 |- F/ j E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
68		nfv 1674	. . . . . . . . . . . . 13 |- F/ m E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) )
69		opeq1 4170	. . . . . . . . . . . . . . . 16 |- ( m = j -> <. m , k >. = <. j , k >. )
70	69	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( m = j -> ( z = <. m , k >. <-> z = <. j , k >. ) )
71		eleq1 2526	. . . . . . . . . . . . . . . . . 18 |- ( m = j -> ( m e. { y } <-> j e. { y } ) )
72		elsn 4002	. . . . . . . . . . . . . . . . . 18 |- ( j e. { y } <-> j = y )
73	71, 72	syl6bb 261	. . . . . . . . . . . . . . . . 17 |- ( m = j -> ( m e. { y } <-> j = y ) )
74	73	anbi1d 704	. . . . . . . . . . . . . . . 16 |- ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. [_ y / j ]_ B ) ) )
75	22	eleq2d 2524	. . . . . . . . . . . . . . . . . 18 |- ( j = y -> ( k e. B <-> k e. [_ y / j ]_ B ) )
76	75	pm5.32i 637	. . . . . . . . . . . . . . . . 17 |- ( ( j = y /\ k e. B ) <-> ( j = y /\ k e. [_ y / j ]_ B ) )
77	76	bicomi 202	. . . . . . . . . . . . . . . 16 |- ( ( j = y /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. B ) )
78	74, 77	syl6bb 261	. . . . . . . . . . . . . . 15 |- ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. B ) ) )
79	70, 78	anbi12d 710	. . . . . . . . . . . . . 14 |- ( m = j -> ( ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
80	79	exbidv 1681	. . . . . . . . . . . . 13 |- ( m = j -> ( E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
81	67, 68, 80	cbvex 1982	. . . . . . . . . . . 12 |- ( E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
82	61, 81	bitri 249	. . . . . . . . . . 11 |- ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
83		nfv 1674	. . . . . . . . . . . 12 |- F/ j ph
84		nfcv 2616	. . . . . . . . . . . . . 14 |- F/_ j ( 2nd ` z )
85	84, 28	nfcsb 3416	. . . . . . . . . . . . 13 |- F/_ j [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
86	85	nfeq2 2633	. . . . . . . . . . . 12 |- F/ j D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
87		nfv 1674	. . . . . . . . . . . . 13 |- F/ k ph
88		nfcsb1v 3414	. . . . . . . . . . . . . 14 |- F/_ k [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
89	88	nfeq2 2633	. . . . . . . . . . . . 13 |- F/ k D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
90		fprod2d.1	. . . . . . . . . . . . . . . 16 |- ( z = <. j , k >. -> D = C )
91	90	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = C )
92	31	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> C = [_ y / j ]_ C )
93		fveq2 5802	. . . . . . . . . . . . . . . . . 18 |- ( z = <. j , k >. -> ( 2nd ` z ) = ( 2nd ` <. j , k >. ) )
94		vex 3081	. . . . . . . . . . . . . . . . . . 19 |- j e. _V
95		vex 3081	. . . . . . . . . . . . . . . . . . 19 |- k e. _V
96	94, 95	op2nd 6699	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` <. j , k >. ) = k
97	93, 96	syl6req 2512	. . . . . . . . . . . . . . . . 17 |- ( z = <. j , k >. -> k = ( 2nd ` z ) )
98	97	ad2antlr 726	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> k = ( 2nd ` z ) )
99		csbeq1a 3407	. . . . . . . . . . . . . . . 16 |- ( k = ( 2nd ` z ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
100	98, 99	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
101	91, 92, 100	3eqtrd 2499	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
102	101	expl 618	. . . . . . . . . . . . 13 |- ( ph -> ( ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
103	87, 89, 102	exlimd 1852	. . . . . . . . . . . 12 |- ( ph -> ( E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
104	83, 86, 103	exlimd 1852	. . . . . . . . . . 11 |- ( ph -> ( E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
105	82, 104	syl5bi 217	. . . . . . . . . 10 |- ( ph -> ( z e. ( { y } X. [_ y / j ]_ B ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
106	105	imp 429	. . . . . . . . 9 |- ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
107	106	prodeq2dv 27600	. . . . . . . 8 |- ( ph -> prod_ z e. ( { y } X. [_ y / j ]_ B ) D = prod_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
108	60, 107	eqtr4d 2498	. . . . . . 7 |- ( ph -> prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
109	47, 108	syl5eq 2507	. . . . . 6 |- ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
110	43, 109	eqtrd 2495	. . . . 5 |- ( ph -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
111	12, 110	syl5eq 2507	. . . 4 |- ( ph -> prod_ j e. { y } prod_ k e. B C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
112	111	adantr 465	. . 3 |- ( ( ph /\ ps ) -> prod_ j e. { y } prod_ k e. B C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
113	3, 112	oveq12d 6221	. 2 |- ( ( ph /\ ps ) -> ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
114		fprod2d.5	. . . . 5 |- ( ph -> -. y e. x )
115		disjsn 4047	. . . . 5 |- ( ( x i^i { y } ) = (/) <-> -. y e. x )
116	114, 115	sylibr 212	. . . 4 |- ( ph -> ( x i^i { y } ) = (/) )
117		eqidd 2455	. . . 4 |- ( ph -> ( x u. { y } ) = ( x u. { y } ) )
118		fprod2d.2	. . . . 5 |- ( ph -> A e. Fin )
119		ssfi 7647	. . . . 5 |- ( ( A e. Fin /\ ( x u. { y } ) C_ A ) -> ( x u. { y } ) e. Fin )
120	118, 13, 119	syl2anc 661	. . . 4 |- ( ph -> ( x u. { y } ) e. Fin )
121	13	sselda 3467	. . . . 5 |- ( ( ph /\ j e. ( x u. { y } ) ) -> j e. A )
122	26	anassrs 648	. . . . . 6 |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. CC )
123	18, 122	fprodcl 27629	. . . . 5 |- ( ( ph /\ j e. A ) -> prod_ k e. B C e. CC )
124	121, 123	syldan 470	. . . 4 |- ( ( ph /\ j e. ( x u. { y } ) ) -> prod_ k e. B C e. CC )
125	116, 117, 120, 124	fprodsplit 27640	. . 3 |- ( ph -> prod_ j e. ( x u. { y } ) prod_ k e. B C = ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) )
126	125	adantr 465	. 2 |- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) )
127		eliun 4286	. . . . . . . . . 10 |- ( z e. U_ j e. x ( { j } X. B ) <-> E. j e. x z e. ( { j } X. B ) )
128		xp1st 6719	. . . . . . . . . . . . . . 15 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
129		elsni 4013	. . . . . . . . . . . . . . 15 |- ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j )
130	128, 129	syl 16	. . . . . . . . . . . . . 14 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
131	130	eleq1d 2523	. . . . . . . . . . . . 13 |- ( z e. ( { j } X. B ) -> ( ( 1st ` z ) e. x <-> j e. x ) )
132	131	biimprd 223	. . . . . . . . . . . 12 |- ( z e. ( { j } X. B ) -> ( j e. x -> ( 1st ` z ) e. x ) )
133	132	impcom 430	. . . . . . . . . . 11 |- ( ( j e. x /\ z e. ( { j } X. B ) ) -> ( 1st ` z ) e. x )
134	133	rexlimiva 2942	. . . . . . . . . 10 |- ( E. j e. x z e. ( { j } X. B ) -> ( 1st ` z ) e. x )
135	127, 134	sylbi 195	. . . . . . . . 9 |- ( z e. U_ j e. x ( { j } X. B ) -> ( 1st ` z ) e. x )
136		xp1st 6719	. . . . . . . . 9 |- ( z e. ( { y } X. [_ y / j ]_ B ) -> ( 1st ` z ) e. { y } )
137	135, 136	anim12i 566	. . . . . . . 8 |- ( ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
138		elin 3650	. . . . . . . 8 |- ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) <-> ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) )
139		elin 3650	. . . . . . . 8 |- ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
140	137, 138, 139	3imtr4i 266	. . . . . . 7 |- ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> ( 1st ` z ) e. ( x i^i { y } ) )
141	116	eleq2d 2524	. . . . . . . 8 |- ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( 1st ` z ) e. (/) ) )
142		noel 3752	. . . . . . . . 9 |- -. ( 1st ` z ) e. (/)
143	142	pm2.21i 131	. . . . . . . 8 |- ( ( 1st ` z ) e. (/) -> z e. (/) )
144	141, 143	syl6bi 228	. . . . . . 7 |- ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) -> z e. (/) ) )
145	140, 144	syl5 32	. . . . . 6 |- ( ph -> ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> z e. (/) ) )
146	145	ssrdv 3473	. . . . 5 |- ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) )
147		ss0 3779	. . . . 5 |- ( ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
148	146, 147	syl 16	. . . 4 |- ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
149		iunxun 4363	. . . . . 6 |- U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) )
150		nfcv 2616	. . . . . . . . 9 |- F/_ m ( { j } X. B )
151		nfcv 2616	. . . . . . . . . 10 |- F/_ j { m }
152	151, 5	nfxp 4977	. . . . . . . . 9 |- F/_ j ( { m } X. [_ m / j ]_ B )
153		sneq 3998	. . . . . . . . . 10 |- ( j = m -> { j } = { m } )
154	153, 8	xpeq12d 4976	. . . . . . . . 9 |- ( j = m -> ( { j } X. B ) = ( { m } X. [_ m / j ]_ B ) )
155	150, 152, 154	cbviun 4318	. . . . . . . 8 |- U_ j e. { y } ( { j } X. B ) = U_ m e. { y } ( { m } X. [_ m / j ]_ B )
156		sneq 3998	. . . . . . . . . 10 |- ( m = y -> { m } = { y } )
157	156, 38	xpeq12d 4976	. . . . . . . . 9 |- ( m = y -> ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B ) )
158	15, 157	iunxsn 4361	. . . . . . . 8 |- U_ m e. { y } ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B )
159	155, 158	eqtri 2483	. . . . . . 7 |- U_ j e. { y } ( { j } X. B ) = ( { y } X. [_ y / j ]_ B )
160	159	uneq2i 3618	. . . . . 6 |- ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
161	149, 160	eqtri 2483	. . . . 5 |- U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
162	161	a1i 11	. . . 4 |- ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) ) )
163		snfi 7503	. . . . . . 7 |- { j } e. Fin
164	121, 18	syldan 470	. . . . . . 7 |- ( ( ph /\ j e. ( x u. { y } ) ) -> B e. Fin )
165		xpfi 7697	. . . . . . 7 |- ( ( { j } e. Fin /\ B e. Fin ) -> ( { j } X. B ) e. Fin )
166	163, 164, 165	sylancr 663	. . . . . 6 |- ( ( ph /\ j e. ( x u. { y } ) ) -> ( { j } X. B ) e. Fin )
167	166	ralrimiva 2830	. . . . 5 |- ( ph -> A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
168		iunfi 7713	. . . . 5 |- ( ( ( x u. { y } ) e. Fin /\ A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin ) -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
169	120, 167, 168	syl2anc 661	. . . 4 |- ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
170		eliun 4286	. . . . . 6 |- ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) <-> E. j e. ( x u. { y } ) z e. ( { j } X. B ) )
171		elxp 4968	. . . . . . . 8 |- ( z e. ( { j } X. B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) )
172		simprl 755	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. m , k >. )
173		simprrl 763	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m e. { j } )
174		elsni 4013	. . . . . . . . . . . . . . 15 |- ( m e. { j } -> m = j )
175	173, 174	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m = j )
176	175	opeq1d 4176	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> <. m , k >. = <. j , k >. )
177	172, 176	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. j , k >. )
178	177, 90	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D = C )
179		simpll 753	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> ph )
180	121	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> j e. A )
181		simprrr 764	. . . . . . . . . . . 12 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> k e. B )
182	179, 180, 181, 26	syl12anc 1217	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> C e. CC )
183	178, 182	eqeltrd 2542	. . . . . . . . . 10 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D e. CC )
184	183	ex 434	. . . . . . . . 9 |- ( ( ph /\ j e. ( x u. { y } ) ) -> ( ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
185	184	exlimdvv 1692	. . . . . . . 8 |- ( ( ph /\ j e. ( x u. { y } ) ) -> ( E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
186	171, 185	syl5bi 217	. . . . . . 7 |- ( ( ph /\ j e. ( x u. { y } ) ) -> ( z e. ( { j } X. B ) -> D e. CC ) )
187	186	rexlimdva 2947	. . . . . 6 |- ( ph -> ( E. j e. ( x u. { y } ) z e. ( { j } X. B ) -> D e. CC ) )
188	170, 187	syl5bi 217	. . . . 5 |- ( ph -> ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) -> D e. CC ) )
189	188	imp 429	. . . 4 |- ( ( ph /\ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) ) -> D e. CC )
190	148, 162, 169, 189	fprodsplit 27640	. . 3 |- ( ph -> prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
191	190	adantr 465	. 2 |- ( ( ph /\ ps ) -> prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
192	113, 126, 191	3eqtr4d 2505	1 |- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   E.wex 1587   e. wcel 1758   A.wral 2799   E.wrex 2800   [_csb 3398   u. cun 3437   i^i cin 3438   C_ wss 3439   (/)c0 3748   {csn 3988   <.cop 3994   U_ciun 4282   X. cxp 4949   |` cres 4953   -1-1-onto->wf1o 5528   ` cfv 5529  (class class class)co 6203   1stc1st 6688   2ndc2nd 6689   Fincfn 7423   CCcc 9394   x. cmul 9401   prod_cprod 27582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-inf2 7961  ax-cnex 9452  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473  ax-pre-sup 9474

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-om 6590  df-1st 6690  df-2nd 6691  df-recs 6945  df-rdg 6979  df-1o 7033  df-oadd 7037  df-er 7214  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-sup 7805  df-oi 7838  df-card 8223  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-div 10108  df-nn 10437  df-2 10494  df-3 10495  df-n0 10694  df-z 10761  df-uz 10976  df-rp 11106  df-fz 11558  df-fzo 11669  df-seq 11927  df-exp 11986  df-hash 12224  df-cj 12709  df-re 12710  df-im 12711  df-sqr 12845  df-abs 12846  df-clim 13087  df-prod 27583

This theorem is referenced by:  fprod2d  27656