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		simpr	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to ⟨x, y⟩ \in (\{j\} \times B)$
68		opelxp	$⊢ ⟨x, y⟩ \in (\{j\} \times B) \leftrightarrow (x \in \{j\} \land y \in B)$
69	67 68	sylib	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to (x \in \{j\} \land y \in B)$
70	69	simpld	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x \in \{j\}$
71		elsni	$⊢ x \in \{j\} \to x = j$
72	70 71	syl	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x = j$
73		simpl	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to j \in A$
74	72 73	eqeltrd	$⊢ (j \in A \land ⟨x, y⟩ \in (\{j\} \times B)) \to x \in A$
75	74	rexlimiva	$⊢ \exists j \in A ⟨x, y⟩ \in (\{j\} \times B) \to x \in A$
76	66 75	syl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to x \in A$
77	76	expr	$⊢ (φ \land y \in C) \to (x \in ⦋ y / k ⦌ D \to x \in A)$
78	77	ssrdv	$⊢ (φ \land y \in C) \to ⦋ y / k ⦌ D \subseteq A$
79	59 78	ssfid	$⊢ (φ \land y \in C) \to ⦋ y / k ⦌ D \in Fin$
80		xpfi	$⊢ (\{y\} \in Fin \land ⦋ y / k ⦌ D \in Fin) \to \{y\} \times ⦋ y / k ⦌ D \in Fin$
81	58 79 80	sylancr	$⊢ (φ \land y \in C) \to \{y\} \times ⦋ y / k ⦌ D \in Fin$
82	81	ralrimiva	$⊢ φ \to \forall y \in C \{y\} \times ⦋ y / k ⦌ D \in Fin$
83		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$
84	2 82 83	syl2anc	$⊢ φ \to ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \in Fin$
85		reliun	$⊢ Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \leftrightarrow \forall y \in C Rel (\{y\} \times ⦋ y / k ⦌ D)$
86		relxp	$⊢ Rel (\{y\} \times ⦋ y / k ⦌ D)$
87	86	a1i	$⊢ y \in C \to Rel (\{y\} \times ⦋ y / k ⦌ D)$
88	85 87	mprgbir	$⊢ Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
89	88	a1i	$⊢ φ \to Rel ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
90		csbeq1	$⊢ x = 2^{nd} (w) \to ⦋ x / j ⦌ E = ⦋ 2^{nd} (w) / j ⦌ E$
91	90	csbeq2dv	$⊢ x = 2^{nd} (w) \to ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E$
92	91	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 ℂ)$
93		csbeq1	$⊢ y = 1^{st} (w) \to ⦋ y / k ⦌ D = ⦋ 1^{st} (w) / k ⦌ D$
94		csbeq1	$⊢ y = 1^{st} (w) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E = ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E$
95	94	eleq1d	$⊢ y = 1^{st} (w) \to (⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ \leftrightarrow ⦋ 1^{st} (w) / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
96	93 95	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 ℂ)$
97		simpl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to φ$
98	29	nfcri	$⊢ Ⅎ j y \in ⦋ x / j ⦌ B$
99	71	equcomd	$⊢ x \in \{j\} \to j = x$
100	99 32	syl	$⊢ x \in \{j\} \to B = ⦋ x / j ⦌ B$
101	100	eleq2d	$⊢ x \in \{j\} \to (y \in B \leftrightarrow y \in ⦋ x / j ⦌ B)$
102	101	biimpa	$⊢ (x \in \{j\} \land y \in B) \to y \in ⦋ x / j ⦌ B$
103	68 102	sylbi	$⊢ ⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B$
104	103	a1i	$⊢ j \in A \to (⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B)$
105	98 104	rexlimi	$⊢ \exists j \in A ⟨x, y⟩ \in (\{j\} \times B) \to y \in ⦋ x / j ⦌ B$
106	66 105	syl	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to y \in ⦋ x / j ⦌ B$
107	5	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B E \in ℂ$
108		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ x / j ⦌ E$
109	108	nfel1	$⊢ Ⅎ j ⦋ x / j ⦌ E \in ℂ$
110	29 109	nfralw	$⊢ Ⅎ j \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ$
111		csbeq1a	$⊢ j = x \to E = ⦋ x / j ⦌ E$
112	111	eleq1d	$⊢ j = x \to (E \in ℂ \leftrightarrow ⦋ x / j ⦌ E \in ℂ)$
113	32 112	raleqbidv	$⊢ j = x \to (\forall k \in B E \in ℂ \leftrightarrow \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ)$
114	110 113	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 ℂ)$
115	107 114	mpan9	$⊢ (φ \land x \in A) \to \forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ$
116		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ ⦋ x / j ⦌ E$
117	116	nfel1	$⊢ Ⅎ k ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
118		csbeq1a	$⊢ k = y \to ⦋ x / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
119	118	eleq1d	$⊢ k = y \to (⦋ x / j ⦌ E \in ℂ \leftrightarrow ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
120	117 119	rspc	$⊢ y \in ⦋ x / j ⦌ B \to (\forall k \in ⦋ x / j ⦌ B ⦋ x / j ⦌ E \in ℂ \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
121	115 120	syl5com	$⊢ (φ \land x \in A) \to (y \in ⦋ x / j ⦌ B \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ)$
122	121	impr	$⊢ (φ \land (x \in A \land y \in ⦋ x / j ⦌ B)) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
123	97 76 106 122	syl12anc	$⊢ (φ \land (y \in C \land x \in ⦋ y / k ⦌ D)) \to ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
124	123	ralrimivva	$⊢ φ \to \forall y \in C \forall x \in ⦋ y / k ⦌ D ⦋ y / k ⦌ ⦋ x / j ⦌ E \in ℂ$
125	124	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 ℂ$
126		simpr	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)$
127		eliun	$⊢ w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D) \leftrightarrow \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D)$
128	126 127	sylib	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D)$
129		xp1st	$⊢ w \in (\{y\} \times ⦋ y / k ⦌ D) \to 1^{st} (w) \in \{y\}$
130	129	adantl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in \{y\}$
131		elsni	$⊢ 1^{st} (w) \in \{y\} \to 1^{st} (w) = y$
132	130 131	syl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) = y$
133		simpl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to y \in C$
134	132 133	eqeltrd	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in C$
135	134	rexlimiva	$⊢ \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D) \to 1^{st} (w) \in C$
136	128 135	syl	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to 1^{st} (w) \in C$
137	96 125 136	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 ℂ$
138		xp2nd	$⊢ w \in (\{y\} \times ⦋ y / k ⦌ D) \to 2^{nd} (w) \in ⦋ y / k ⦌ D$
139	138	adantl	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ y / k ⦌ D$
140	132	csbeq1d	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ D = ⦋ y / k ⦌ D$
141	139 140	eleqtrrd	$⊢ (y \in C \land w \in (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
142	141	rexlimiva	$⊢ \exists y \in C w \in (\{y\} \times ⦋ y / k ⦌ D) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
143	128 142	syl	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to 2^{nd} (w) \in ⦋ 1^{st} (w) / k ⦌ D$
144	92 137 143	rspcdva	$⊢ (φ \land w \in ⋃_{y \in C} (\{y\} \times ⦋ y / k ⦌ D)) \to ⦋ 1^{st} (w) / k ⦌ ⦋ 2^{nd} (w) / j ⦌ E \in ℂ$
145	51 57 84 89 144	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$
146	45 145	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$
147	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
148	29	nfel1	$⊢ Ⅎ j ⦋ x / j ⦌ B \in Fin$
149	32	eleq1d	$⊢ j = x \to (B \in Fin \leftrightarrow ⦋ x / j ⦌ B \in Fin)$
150	148 149	rspc	$⊢ x \in A \to (\forall j \in A B \in Fin \to ⦋ x / j ⦌ B \in Fin)$
151	147 150	mpan9	$⊢ (φ \land x \in A) \to ⦋ x / j ⦌ B \in Fin$
152	57 1 151 122	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$
153	51 2 79 123	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$
154	146 152 153	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$
155		nfcv	$⊢ \underline{Ⅎ} x \prod_{k \in B} E$
156		nfcv	$⊢ \underline{Ⅎ} j y$
157	156 108	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ y / k ⦌ ⦋ x / j ⦌ E$
158	29 157	nfcprod	$⊢ \underline{Ⅎ} j \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
159		nfcv	$⊢ \underline{Ⅎ} y E$
160		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ E$
161		csbeq1a	$⊢ k = y \to E = ⦋ y / k ⦌ E$
162	159 160 161	cbvprodi	$⊢ \prod_{k \in B} E = \prod_{y \in B} ⦋ y / k ⦌ E$
163	111	csbeq2dv	$⊢ j = x \to ⦋ y / k ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
164	163	adantr	$⊢ (j = x \land y \in B) \to ⦋ y / k ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
165	32 164	prodeq12dv	$⊢ j = x \to \prod_{y \in B} ⦋ y / k ⦌ E = \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
166	162 165	syl5eq	$⊢ j = x \to \prod_{k \in B} E = \prod_{y \in ⦋ x / j ⦌ B} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
167	155 158 166	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$
168		nfcv	$⊢ \underline{Ⅎ} y \prod_{j \in D} E$
169	37 116	nfcprod	$⊢ \underline{Ⅎ} k \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
170		nfcv	$⊢ \underline{Ⅎ} x E$
171	170 108 111	cbvprodi	$⊢ \prod_{j \in D} E = \prod_{x \in D} ⦋ x / j ⦌ E$
172	118	adantr	$⊢ (k = y \land x \in D) \to ⦋ x / j ⦌ E = ⦋ y / k ⦌ ⦋ x / j ⦌ E$
173	40 172	prodeq12dv	$⊢ k = y \to \prod_{x \in D} ⦋ x / j ⦌ E = \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
174	171 173	syl5eq	$⊢ k = y \to \prod_{j \in D} E = \prod_{x \in ⦋ y / k ⦌ D} ⦋ y / k ⦌ ⦋ x / j ⦌ E$
175	168 169 174	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$
176	154 167 175	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