Theorem fprod2dlem 29028

Description: Lemma for fprod2d 29029- 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 2629	. . . . . 6 |- F/_ m prod_ k e. B C
5		nfcsb1v 3456	. . . . . . 7 |- F/_ j [_ m / j ]_ B
6		nfcsb1v 3456	. . . . . . 7 |- F/_ j [_ m / j ]_ C
7	5, 6	nfcprod 28961	. . . . . 6 |- F/_ j prod_ k e. [_ m / j ]_ B [_ m / j ]_ C
8		csbeq1a 3449	. . . . . . 7 |- ( j = m -> B = [_ m / j ]_ B )
9		csbeq1a 3449	. . . . . . . 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 28976	. . . . . 6 |- ( j = m -> prod_ k e. B C = prod_ k e. [_ m / j ]_ B [_ m / j ]_ C )
12	4, 7, 11	cbvprodi 28967	. . . . 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 3687	. . . . . . . 8 |- ( ph -> { y } C_ A )
15		vex 3121	. . . . . . . . 9 |- y e. _V
16	15	snss 4157	. . . . . . . 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 2881	. . . . . . . . 9 |- ( ph -> A. j e. A B e. Fin )
20		nfcsb1v 3456	. . . . . . . . . . 11 |- F/_ j [_ y / j ]_ B
21	20	nfel1 2645	. . . . . . . . . 10 |- F/ j [_ y / j ]_ B e. Fin
22		csbeq1a 3449	. . . . . . . . . . 11 |- ( j = y -> B = [_ y / j ]_ B )
23	22	eleq1d 2536	. . . . . . . . . 10 |- ( j = y -> ( B e. Fin <-> [_ y / j ]_ B e. Fin ) )
24	21, 23	rspc 3213	. . . . . . . . 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 2888	. . . . . . . . . 10 |- ( ph -> A. j e. A A. k e. B C e. CC )
28		nfcsb1v 3456	. . . . . . . . . . . . 13 |- F/_ j [_ y / j ]_ C
29	28	nfel1 2645	. . . . . . . . . . . 12 |- F/ j [_ y / j ]_ C e. CC
30	20, 29	nfral 2853	. . . . . . . . . . 11 |- F/ j A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC
31		csbeq1a 3449	. . . . . . . . . . . . 13 |- ( j = y -> C = [_ y / j ]_ C )
32	31	eleq1d 2536	. . . . . . . . . . . 12 |- ( j = y -> ( C e. CC <-> [_ y / j ]_ C e. CC ) )
33	22, 32	raleqbidv 3077	. . . . . . . . . . 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 3213	. . . . . . . . . 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 2836	. . . . . . . 8 |- ( ( ph /\ k e. [_ y / j ]_ B ) -> [_ y / j ]_ C e. CC )
37	25, 36	fprodcl 29002	. . . . . . 7 |- ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
38		csbeq1 3443	. . . . . . . . 9 |- ( m = y -> [_ m / j ]_ B = [_ y / j ]_ B )
39		csbeq1 3443	. . . . . . . . . 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 28976	. . . . . . . 8 |- ( m = y -> prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
42	41	prodsn 29010	. . . . . . 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 2629	. . . . . . . 8 |- F/_ m [_ y / j ]_ C
45		nfcsb1v 3456	. . . . . . . 8 |- F/_ k [_ m / k ]_ [_ y / j ]_ C
46		csbeq1a 3449	. . . . . . . 8 |- ( k = m -> [_ y / j ]_ C = [_ m / k ]_ [_ y / j ]_ C )
47	44, 45, 46	cbvprodi 28967	. . . . . . 7 |- prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C
48		csbeq1 3443	. . . . . . . . 9 |- ( m = ( 2nd ` z ) -> [_ m / k ]_ [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
49		snfi 7608	. . . . . . . . . 10 |- { y } e. Fin
50		xpfi 7803	. . . . . . . . . 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 6884	. . . . . . . . . 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 5886	. . . . . . . . . 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 2645	. . . . . . . . . . 11 |- F/ k [_ m / k ]_ [_ y / j ]_ C e. CC
57	46	eleq1d 2536	. . . . . . . . . . 11 |- ( k = m -> ( [_ y / j ]_ C e. CC <-> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
58	56, 57	rspc 3213	. . . . . . . . . 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 28996	. . . . . . . 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 5022	. . . . . . . . . . . 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 1683	. . . . . . . . . . . . . . 15 |- F/ j z = <. m , k >.
63		nfv 1683	. . . . . . . . . . . . . . . 16 |- F/ j m e. { y }
64	20	nfcri 2622	. . . . . . . . . . . . . . . 16 |- F/ j k e. [_ y / j ]_ B
65	63, 64	nfan 1875	. . . . . . . . . . . . . . 15 |- F/ j ( m e. { y } /\ k e. [_ y / j ]_ B )
66	62, 65	nfan 1875	. . . . . . . . . . . . . 14 |- F/ j ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
67	66	nfex 1895	. . . . . . . . . . . . 13 |- F/ j E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
68		nfv 1683	. . . . . . . . . . . . 13 |- F/ m E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) )
69		opeq1 4219	. . . . . . . . . . . . . . . 16 |- ( m = j -> <. m , k >. = <. j , k >. )
70	69	eqeq2d 2481	. . . . . . . . . . . . . . 15 |- ( m = j -> ( z = <. m , k >. <-> z = <. j , k >. ) )
71		eleq1 2539	. . . . . . . . . . . . . . . . . 18 |- ( m = j -> ( m e. { y } <-> j e. { y } ) )
72		elsn 4047	. . . . . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . . 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 1690	. . . . . . . . . . . . 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 1995	. . . . . . . . . . . 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 1683	. . . . . . . . . . . 12 |- F/ j ph
84		nfcv 2629	. . . . . . . . . . . . . 14 |- F/_ j ( 2nd ` z )
85	84, 28	nfcsb 3458	. . . . . . . . . . . . 13 |- F/_ j [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
86	85	nfeq2 2646	. . . . . . . . . . . 12 |- F/ j D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
87		nfv 1683	. . . . . . . . . . . . 13 |- F/ k ph
88		nfcsb1v 3456	. . . . . . . . . . . . . 14 |- F/_ k [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
89	88	nfeq2 2646	. . . . . . . . . . . . 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 5872	. . . . . . . . . . . . . . . . . 18 |- ( z = <. j , k >. -> ( 2nd ` z ) = ( 2nd ` <. j , k >. ) )
94		vex 3121	. . . . . . . . . . . . . . . . . . 19 |- j e. _V
95		vex 3121	. . . . . . . . . . . . . . . . . . 19 |- k e. _V
96	94, 95	op2nd 6804	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` <. j , k >. ) = k
97	93, 96	syl6req 2525	. . . . . . . . . . . . . . . . 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 3449	. . . . . . . . . . . . . . . 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 2512	. . . . . . . . . . . . . 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 1861	. . . . . . . . . . . 12 |- ( ph -> ( E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
104	83, 86, 103	exlimd 1861	. . . . . . . . . . 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 28973	. . . . . . . 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 2511	. . . . . . 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 2520	. . . . . 6 |- ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
110	43, 109	eqtrd 2508	. . . . 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 2520	. . . 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 6313	. 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 4094	. . . . 5 |- ( ( x i^i { y } ) = (/) <-> -. y e. x )
116	114, 115	sylibr 212	. . . 4 |- ( ph -> ( x i^i { y } ) = (/) )
117		eqidd 2468	. . . 4 |- ( ph -> ( x u. { y } ) = ( x u. { y } ) )
118		fprod2d.2	. . . . 5 |- ( ph -> A e. Fin )
119		ssfi 7752	. . . . 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 3509	. . . . 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 29002	. . . . 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 29013	. . 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 4336	. . . . . . . . . 10 |- ( z e. U_ j e. x ( { j } X. B ) <-> E. j e. x z e. ( { j } X. B ) )
128		xp1st 6825	. . . . . . . . . . . . . . 15 |- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
129		elsni 4058	. . . . . . . . . . . . . . 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 2536	. . . . . . . . . . . . 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 2955	. . . . . . . . . 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 6825	. . . . . . . . 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 3692	. . . . . . . 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 3692	. . . . . . . 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 2537	. . . . . . . 8 |- ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( 1st ` z ) e. (/) ) )
142		noel 3794	. . . . . . . . 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 3515	. . . . 5 |- ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) )
147		ss0 3821	. . . . 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 4413	. . . . . 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 2629	. . . . . . . . 9 |- F/_ m ( { j } X. B )
151		nfcv 2629	. . . . . . . . . 10 |- F/_ j { m }
152	151, 5	nfxp 5032	. . . . . . . . 9 |- F/_ j ( { m } X. [_ m / j ]_ B )
153		sneq 4043	. . . . . . . . . 10 |- ( j = m -> { j } = { m } )
154	153, 8	xpeq12d 5030	. . . . . . . . 9 |- ( j = m -> ( { j } X. B ) = ( { m } X. [_ m / j ]_ B ) )
155	150, 152, 154	cbviun 4368	. . . . . . . 8 |- U_ j e. { y } ( { j } X. B ) = U_ m e. { y } ( { m } X. [_ m / j ]_ B )
156		sneq 4043	. . . . . . . . . 10 |- ( m = y -> { m } = { y } )
157	156, 38	xpeq12d 5030	. . . . . . . . 9 |- ( m = y -> ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B ) )
158	15, 157	iunxsn 4411	. . . . . . . 8 |- U_ m e. { y } ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B )
159	155, 158	eqtri 2496	. . . . . . 7 |- U_ j e. { y } ( { j } X. B ) = ( { y } X. [_ y / j ]_ B )
160	159	uneq2i 3660	. . . . . 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 2496	. . . . 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 7608	. . . . . . 7 |- { j } e. Fin
164	121, 18	syldan 470	. . . . . . 7 |- ( ( ph /\ j e. ( x u. { y } ) ) -> B e. Fin )
165		xpfi 7803	. . . . . . 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 2881	. . . . 5 |- ( ph -> A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
168		iunfi 7820	. . . . 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 4336	. . . . . 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 5022	. . . . . . . 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 4058	. . . . . . . . . . . . . . 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 4225	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> <. m , k >. = <. j , k >. )
177	172, 176	eqtrd 2508	. . . . . . . . . . . 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 1226	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> C e. CC )
183	178, 182	eqeltrd 2555	. . . . . . . . . 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 1701	. . . . . . . 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 2959	. . . . . 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 29013	. . 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 2518	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 1379   E.wex 1596   e. wcel 1767   A.wral 2817   E.wrex 2818   [_csb 3440   u. cun 3479   i^i cin 3480   C_ wss 3481   (/)c0 3790   {csn 4033   <.cop 4039   U_ciun 4331   X. cxp 5003   |` cres 5007   -1-1-onto->wf1o 5593   ` cfv 5594  (class class class)co 6295   1stc1st 6793   2ndc2nd 6794   Fincfn 7528   CCcc 9502   x. cmul 9509   prod_cprod 28955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-sup 7913  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-n0 10808  df-z 10877  df-uz 11095  df-rp 11233  df-fz 11685  df-fzo 11805  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-clim 13291  df-prod 28956

This theorem is referenced by:  fprod2d  29029