fprodcom2

Description: Interchange order of multiplication. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018) (Proof shortened by JJ, 2-Aug-2021)

	Ref	Expression
Hypotheses	fprodcom2.1	$⊢ φ \to A \in Fin$
	fprodcom2.2	$⊢ φ \to C \in Fin$
	fprodcom2.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fprodcom2.4	$⊢ φ \to ((j \in A \land k \in B) \leftrightarrow (k \in C \land j \in D))$
	fprodcom2.5	$⊢ (φ \land (j \in A \land k \in B)) \to E \in ℂ$
Assertion	fprodcom2	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} E = \prod_{k \in C} \prod_{j \in D} E$

Proof

Step	Hyp	Ref	Expression
1		fprodcom2.1	$⊢ φ \to A \in Fin$
2		fprodcom2.2	$⊢ φ \to C \in Fin$
3		fprodcom2.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fprodcom2.4	$⊢ φ \to ((j \in A \land k \in B) \leftrightarrow (k \in C \land j \in D))$
5		fprodcom2.5	$⊢ (φ \land (j \in A \land k \in B)) \to E \in ℂ$
6		relxp	$⊢ Rel (\{j\} \times B)$
7	6	rgenw	$⊢ \forall j \in A Rel (\{j\} \times B)$
8		reliun	$⊢ Rel ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \forall j \in A Rel (\{j\} \times B)$
9	7 8	mpbir	$⊢ Rel ⋃_{j \in A} (\{j\} \times B)$
10		relcnv	$⊢ Rel {⋃_{k \in C} (\{k\} \times D)}^{-1}$
11		ancom	$⊢ (x = j \land y = k) \leftrightarrow (y = k \land x = j)$
12		vex	$⊢ x \in V$
13		vex	$⊢ y \in V$
14	12 13	opth	$⊢ ⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow (x = j \land y = k)$
15	13 12	opth	$⊢ ⟨y, x⟩ = ⟨k, j⟩ \leftrightarrow (y = k \land x = j)$
16	11 14 15	3bitr4i	$⊢ ⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow ⟨y, x⟩ = ⟨k, j⟩$
17	16	a1i	$⊢ φ \to (⟨x, y⟩ = ⟨j, k⟩ \leftrightarrow ⟨y, x⟩ = ⟨k, j⟩)$
18	17 4	anbi12d	$⊢ φ \to ((⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B)) \leftrightarrow (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)))$
19	18	2exbidv	$⊢ φ \to (\exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B)) \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)))$
20		eliunxp	$⊢ ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \exists k (⟨x, y⟩ = ⟨j, k⟩ \land (j \in A \land k \in B))$
21	12 13	opelcnv	$⊢ ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1} \leftrightarrow ⟨y, x⟩ \in ⋃_{k \in C} (\{k\} \times D)$
22		eliunxp	$⊢ ⟨y, x⟩ \in ⋃_{k \in C} (\{k\} \times D) \leftrightarrow \exists k \exists j (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
23		excom	$⊢ \exists k \exists j (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D)) \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
24	21 22 23	3bitri	$⊢ ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1} \leftrightarrow \exists j \exists k (⟨y, x⟩ = ⟨k, j⟩ \land (k \in C \land j \in D))$
25	19 20 24	3bitr4g	$⊢ φ \to (⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1})$
26	9 10 25	eqrelrdv	$⊢ φ \to ⋃_{j \in A} (\{j\} \times B) = {⋃_{k \in C} (\{k\} \times D)}^{-1}$
27		nfcv	$⊢ \underline{Ⅎ} x (\{j\} \times B)$
28		nfcv	$⊢ \underline{Ⅎ} j \{x\}$
29		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ x / j ⦌ B$
30	28 29	nfxp	$⊢ \underline{Ⅎ} j (\{x\} \times ⦋ x / j ⦌ B)$
31		sneq	$⊢ j = x \to \{j\} = \{x\}$
32		csbeq1a	$⊢ j = x \to B = ⦋ x / j ⦌ B$
33	31 32	xpeq12d	$⊢ j = x \to \{j\} \times B = \{x\} \times ⦋ x / j ⦌ B$
34	27 30 33	cbviun	$⊢ ⋃_{j \in A} (\{j\} \times B) = ⋃_{x \in A} (\{x\} \times ⦋ x / j ⦌ B)$
35		nfcv	$⊢ \underline{Ⅎ} y (\{k\} \times D)$
36		nfcv	$⊢ \underline{Ⅎ} k \{y\}$
37		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ D$
38	36 37	nfxp	$⊢ \underline{Ⅎ} k (\{y\} \times ⦋ y / k ⦌ D)$
39		sneq	$⊢ k = y \to \{k\} = \{y\}$
40		csbeq1a	$⊢ k = y \to D = ⦋ y / k ⦌ D$
41	39 40	xpeq12d	$⊢ k = y \to \{k\} \times D = \{y\} \times ⦋ y / k ⦌ D$
42	35 38 41	cbviun	$⊢ ⋃_{k \in C} (\{k\} \times D) = ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
43	42	cnveqi	$⊢ {⋃_{k \in C} (\{k\} \times D)}^{-1} = {⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)}^{-1}$
44	26 34 43	3eqtr3g	$⊢ φ \to ⋃_{x \in A} (\{x\} \times ⦋ x / j ⦌ B) = {⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)}^{-1}$
45	44	prodeq1d	$⊢ φ \to \prod_{z \in ⋃_{x \in A} (\{x\} \times ⦋ x / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = \prod_{z \in {⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)}^{-1}} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
46	13 12	op1std	$⊢ w = ⟨y, x⟩ \to 1^{st} (w) = y$
47	46	csbeq1d	$⊢ w = ⟨y, x⟩ \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ y / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
48	13 12	op2ndd	$⊢ w = ⟨y, x⟩ \to 2^{nd} (w) = x$
49	48	csbeq1d	$⊢ w = ⟨y, x⟩ \to ⦋ 2^{nd} (w) / j ⦌ E = ⦋ x / j ⦌ E$
50	49	csbeq2dv	$⊢ w = ⟨y, x⟩ \to ⦋ y / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
51	47 50	eqtrd	$⊢ w = ⟨y, x⟩ \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
52	12 13	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
53	52	csbeq1d	$⊢ z = ⟨x, y⟩ \to ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ y / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
54	12 13	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
55	54	csbeq1d	$⊢ z = ⟨x, y⟩ \to ⦋ 1^{st} (z) / j ⦌ E = ⦋ x / j ⦌ E$
56	55	csbeq2dv	$⊢ z = ⟨x, y⟩ \to ⦋ y / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
57	53 56	eqtrd	$⊢ z = ⟨x, y⟩ \to ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
58		snfi	$⊢ \{y\} \in Fin$
59	1	adantr	$⊢ (φ \land y \in C) \to A \in Fin$
60	37 40	opeliunxp2f	$⊢ ⟨y, x⟩ \in ⋃_{k \in C} (\{k\} \times D) \leftrightarrow (y \in C \land x \in ⦋ y / k ⦌ D)$
61	21 60	sylbbr	$⊢ (y \in C \land x \in ⦋ y / k ⦌ D) \to ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1}$
62	61	adantl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to ⟨x, y⟩ \in {⋃_{k \in C} (\{k\} \times D)}^{-1}$
63	26	adantr	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to ⋃_{j \in A} (\{j\} \times B) = {⋃_{k \in C} (\{k\} \times D)}^{-1}$
64	62 63	eleqtrrd	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B)$
65		eliun	$⊢ ⟨x, y⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A ⟨x, y⟩ \in (\{j\} \times B)$
66	64 65	sylib	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to \exists j \in A ⟨x, y⟩ \in (\{j\} \times B)$
67		opelxp	$⊢ ⟨x, y⟩ \in (\{j\} \times B) \leftrightarrow (x \in \{j\} \land y \in B)$
68	67	bilani	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to (x \in \{j\} \land y \in B)$
69	68	simpld	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x \in \{j\}$
70		elsni	$⊢ x \in \{j\} \to x = j$
71	69 70	syl	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x = j$
72		simpl	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to j \in A$
73	71 72	eqeltrd	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x \in A$
74	73	rexlimiva	$⊢ \exists j \in A ⟨x, y⟩ \in (\{j\} \times B) \to x \in A$
75	66 74	syl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to x \in A$
76	75	expr	$⊢ (φ \land y \in C) \to (x \in ⦋ y / k ⦌ D \to x \in A)$
77	76	ssrdv	$⊢ (φ \land y \in C) \to ⦋ y / k ⦌ D \subseteq A$
78	59 77	ssfid	$⊢ (φ \land y \in C) \to ⦋ y / k ⦌ D \in Fin$
79		xpfi	$⊢ (\{y\} \in Fin \land ⦋ y / k ⦌ D \in Fin) \to \{y\} \times ⦋ y / k ⦌ D \in Fin$
80	58 78 79	sylancr	$⊢ (φ \land y \in C) \to \{y\} \times ⦋ y / k ⦌ D \in Fin$
81	80	ralrimiva	$⊢ φ \to \forall y \in C \{y\} \times ⦋ y / k ⦌ D \in Fin$
82		iunfi	$⊢ (C \in Fin \land \forall y \in C \{y\} \times ⦋ y / k ⦌ D \in Fin) \to ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \in Fin$
83	2 81 82	syl2anc	$⊢ φ \to ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \in Fin$
84		reliun	$⊢ Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \leftrightarrow \forall y \in C Rel (\{y\} \times ⦋ y / k ⦌ D)$
85		relxp	$⊢ Rel (\{y\} \times ⦋ y / k ⦌ D)$
86	85	a1i	$⊢ y \in C \to Rel (\{y\} \times ⦋ y / k ⦌ D)$
87	84 86	mprgbir	$⊢ Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
88	87	a1i	$⊢ φ \to Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
89		csbeq1	$⊢ x = 2^{nd} (w) \to ⦋ x / j ⦌ E = ⦋ 2^{nd} (w) / j ⦌ E$
90	89	csbeq2dv	$⊢ x = 2^{nd} (w) \to ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
91	90	eleq1d	$⊢ x = 2^{nd} (w) \to (⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ)$
92		csbeq1	$⊢ y = 1^{st} (w) \to ⦋ y / k ⦌ D = ⦋ 1^{st} (w) / k ⦌ D$
93		csbeq1	$⊢ y = 1^{st} (w) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E$
94	93	eleq1d	$⊢ y = 1^{st} (w) \to (⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
95	92 94	raleqbidv	$⊢ y = 1^{st} (w) \to (\forall x \in ⦋ y / k ⦌ D ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ \leftrightarrow \forall x \in ⦋ 1^{st} (w) / k ⦌ D ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
96		simpl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to φ$
97	29	nfcri	$⊢ Ⅎ j y \in ⦋ x / j ⦌ B$
98	70	equcomd	$⊢ x \in \{j\} \to j = x$
99	98 32	syl	$⊢ x \in \{j\} \to B = ⦋ x / j ⦌ B$
100	99	eleq2d	$⊢ x \in \{j\} \to (y \in B \leftrightarrow y \in ⦋ x / j ⦌ B)$
101	100	biimpa	$⊢ (x \in \{j\} \land y \in B) \to y \in ⦋ x / j ⦌ B$
102	67 101	sylbi	$⊢ ⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B$
103	102	a1i	$⊢ j \in A \to (⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B)$
104	97 103	rexlimi	$⊢ \exists j \in A ⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B$
105	66 104	syl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to y \in ⦋ x / j ⦌ B$
106	5	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B E \in ℂ$
107		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ x / j ⦌ E$
108	107	nfel1	$⊢ Ⅎ j ⦋ x / j ⦌ E \in ℂ$
109	29 108	nfralw	$⊢ Ⅎ j \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ$
110		csbeq1a	$⊢ j = x \to E = ⦋ x / j ⦌ E$
111	110	eleq1d	$⊢ j = x \to (E \in ℂ \leftrightarrow ⦋ x / j ⦌ E \in ℂ)$
112	32 111	raleqbidv	$⊢ j = x \to (\forall k \in B E \in ℂ \leftrightarrow \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ)$
113	109 112	rspc	$⊢ x \in A \to (\forall j \in A \forall k \in B E \in ℂ \to \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ)$
114	106 113	mpan9	$⊢ (φ \land x \in A) \to \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ$
115		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ ⦋ x / j ⦌ E$
116	115	nfel1	$⊢ Ⅎ k ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
117		csbeq1a	$⊢ k = y \to ⦋ x / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
118	117	eleq1d	$⊢ k = y \to (⦋ x / j ⦌ E \in ℂ \leftrightarrow ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
119	116 118	rspc	$⊢ y \in ⦋ x / j ⦌ B \to (\forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
120	114 119	syl5com	$⊢ (φ \land x \in A) \to (y \in ⦋ x / j ⦌ B \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
121	120	impr	$⊢ (φ \land (x \in A \land y \in ⦋ x / j ⦌ B)) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
122	96 75 105 121	syl12anc	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
123	122	ralrimivva	$⊢ φ \to \forall y \in C \forall x \in ⦋ y / k ⦌ D ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
124	123	adantr	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to \forall y \in C \forall x \in ⦋ y / k ⦌ D ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
125		eliun	$⊢ w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \leftrightarrow \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D)$
126	125	bilani	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D)$
127		xp1st	$⊢ w \in (\{y\} \times ⦋ y / k ⦌ D) \to 1^{st} (w) \in \{y\}$
128	127	adantl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in \{y\}$
129		elsni	$⊢ 1^{st} (w) \in \{y\} \to 1^{st} (w) = y$
130	128 129	syl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) = y$
131		simpl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to y \in C$
132	130 131	eqeltrd	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in C$
133	132	rexlimiva	$⊢ \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D) \to 1^{st} (w) \in C$
134	126 133	syl	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in C$
135	95 124 134	rspcdva	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to \forall x \in ⦋ 1^{st} (w) / k ⦌ D ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E \in ℂ$
136		xp2nd	$⊢ w \in (\{y\} \times ⦋ y / k ⦌ D) \to 2^{nd} (w) \in ⦋ y / k ⦌ D$
137	136	adantl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ y / k ⦌ D$
138	130	csbeq1d	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ D = ⦋ y / k ⦌ D$
139	137 138	eleqtrrd	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
140	139	rexlimiva	$⊢ \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
141	126 140	syl	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
142	91 135 141	rspcdva	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ$
143	51 57 83 88 142	fprodcnv	$⊢ φ \to \prod_{w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E = \prod_{z \in {⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)}^{-1}} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
144	45 143	eqtr4d	$⊢ φ \to \prod_{z \in ⋃_{x \in A} (\{x\} \times ⦋ x / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E = \prod_{w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
145	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
146	29	nfel1	$⊢ Ⅎ j ⦋ x / j ⦌ B \in Fin$
147	32	eleq1d	$⊢ j = x \to (B \in Fin \leftrightarrow ⦋ x / j ⦌ B \in Fin)$
148	146 147	rspc	$⊢ x \in A \to (\forall j \in A B \in Fin \to ⦋ x / j ⦌ B \in Fin)$
149	145 148	mpan9	$⊢ (φ \land x \in A) \to ⦋ x / j ⦌ B \in Fin$
150	57 1 149 121	fprod2d	$⊢ φ \to \prod_{x \in A} \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E = \prod_{z \in ⋃_{x \in A} (\{x\} \times ⦋ x / j ⦌ B)} ⦋ 2^{nd} (z) / k ⦌ ⦋ 1^{st} (z) / j ⦌ E$
151	51 2 78 122	fprod2d	$⊢ φ \to \prod_{y \in C} \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E = \prod_{w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)} ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
152	144 150 151	3eqtr4d	$⊢ φ \to \prod_{x \in A} \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E = \prod_{y \in C} \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
153		nfcv	$⊢ \underline{Ⅎ} x \prod_{k \in B} E$
154		nfcv	$⊢ \underline{Ⅎ} j y$
155	154 107	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ y / k ⦌ ⦋ x / j ⦌ E$
156	29 155	nfcprod	$⊢ \underline{Ⅎ} j \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
157		nfcv	$⊢ \underline{Ⅎ} y E$
158		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ E$
159		csbeq1a	$⊢ k = y \to E = ⦋ y / k ⦌ E$
160	157 158 159	cbvprodi	$⊢ \prod_{k \in B} E = \prod_{y \in B} ⦋ y / k ⦌ E$
161	110	csbeq2dv	$⊢ j = x \to ⦋ y / k ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
162	161	adantr	$⊢ (j = x \land y \in B) \to ⦋ y / k ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
163	32 162	prodeq12dv	$⊢ j = x \to \prod_{y \in B} ⦋ y / k ⦌ E = \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
164	160 163	eqtrid	$⊢ j = x \to \prod_{k \in B} E = \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
165	153 156 164	cbvprodi	$⊢ \prod_{j \in A} \prod_{k \in B} E = \prod_{x \in A} \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
166		nfcv	$⊢ \underline{Ⅎ} y \prod_{j \in D} E$
167	37 115	nfcprod	$⊢ \underline{Ⅎ} k \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
168		nfcv	$⊢ \underline{Ⅎ} x E$
169	168 107 110	cbvprodi	$⊢ \prod_{j \in D} E = \prod_{x \in D} ⦋ x / j ⦌ E$
170	117	adantr	$⊢ (k = y \land x \in D) \to ⦋ x / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
171	40 170	prodeq12dv	$⊢ k = y \to \prod_{x \in D} ⦋ x / j ⦌ E = \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
172	169 171	eqtrid	$⊢ k = y \to \prod_{j \in D} E = \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
173	166 167 172	cbvprodi	$⊢ \prod_{k \in C} \prod_{j \in D} E = \prod_{y \in C} \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
174	152 165 173	3eqtr4g	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} E = \prod_{k \in C} \prod_{j \in D} E$

Metamath Proof Explorer

Theorem fprodcom2

Proof