fprod2d

Description: Write a double product as a product over a two-dimensional region. Compare fsum2d . (Contributed by Scott Fenton, 30-Jan-2018)

	Ref	Expression
Hypotheses	fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
	fprod2d.2	$⊢ φ \to A \in Fin$
	fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
Assertion	fprod2d	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D$

Proof

Step	Hyp	Ref	Expression
1		fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
2		fprod2d.2	$⊢ φ \to A \in Fin$
3		fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
5		ssid	$⊢ A \subseteq A$
6		sseq1	$⊢ w = \emptyset \to (w \subseteq A \leftrightarrow \emptyset \subseteq A)$
7		prodeq1	$⊢ w = \emptyset \to \prod_{j \in w} \prod_{k \in B} C = \prod_{j \in \emptyset} \prod_{k \in B} C$
8		iuneq1	$⊢ w = \emptyset \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in \emptyset} (\{j\} \times B)$
9		0iun	$⊢ ⋃_{j \in \emptyset} (\{j\} \times B) = \emptyset$
10	8 9	eqtrdi	$⊢ w = \emptyset \to ⋃_{j \in w} (\{j\} \times B) = \emptyset$
11	10	prodeq1d	$⊢ w = \emptyset \to \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \prod_{z \in \emptyset} D$
12	7 11	eqeq12d	$⊢ w = \emptyset \to (\prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \prod_{j \in \emptyset} \prod_{k \in B} C = \prod_{z \in \emptyset} D)$
13	6 12	imbi12d	$⊢ w = \emptyset \to ((w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (\emptyset \subseteq A \to \prod_{j \in \emptyset} \prod_{k \in B} C = \prod_{z \in \emptyset} D))$
14	13	imbi2d	$⊢ w = \emptyset \to ((φ \to (w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (\emptyset \subseteq A \to \prod_{j \in \emptyset} \prod_{k \in B} C = \prod_{z \in \emptyset} D)))$
15		sseq1	$⊢ w = x \to (w \subseteq A \leftrightarrow x \subseteq A)$
16		prodeq1	$⊢ w = x \to \prod_{j \in w} \prod_{k \in B} C = \prod_{j \in x} \prod_{k \in B} C$
17		iuneq1	$⊢ w = x \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B)$
18	17	prodeq1d	$⊢ w = x \to \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
19	16 18	eqeq12d	$⊢ w = x \to (\prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D)$
20	15 19	imbi12d	$⊢ w = x \to ((w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D))$
21	20	imbi2d	$⊢ w = x \to ((φ \to (w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D)))$
22		sseq1	$⊢ w = x \cup \{y\} \to (w \subseteq A \leftrightarrow x \cup \{y\} \subseteq A)$
23		prodeq1	$⊢ w = x \cup \{y\} \to \prod_{j \in w} \prod_{k \in B} C = \prod_{j \in x \cup \{y\}} \prod_{k \in B} C$
24		iuneq1	$⊢ w = x \cup \{y\} \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in x \cup \{y\}} (\{j\} \times B)$
25	24	prodeq1d	$⊢ w = x \cup \{y\} \to \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$
26	23 25	eqeq12d	$⊢ w = x \cup \{y\} \to (\prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)$
27	22 26	imbi12d	$⊢ w = x \cup \{y\} \to ((w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
28	27	imbi2d	$⊢ w = x \cup \{y\} \to ((φ \to (w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
29		sseq1	$⊢ w = A \to (w \subseteq A \leftrightarrow A \subseteq A)$
30		prodeq1	$⊢ w = A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{j \in A} \prod_{k \in B} C$
31		iuneq1	$⊢ w = A \to ⋃_{j \in w} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
32	31	prodeq1d	$⊢ w = A \to \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D$
33	30 32	eqeq12d	$⊢ w = A \to (\prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D \leftrightarrow \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D)$
34	29 33	imbi12d	$⊢ w = A \to ((w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D) \leftrightarrow (A \subseteq A \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D))$
35	34	imbi2d	$⊢ w = A \to ((φ \to (w \subseteq A \to \prod_{j \in w} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in w} (\{j\} \times B)} D)) \leftrightarrow (φ \to (A \subseteq A \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D)))$
36		prod0	$⊢ \prod_{j \in \emptyset} \prod_{k \in B} C = 1$
37		prod0	$⊢ \prod_{z \in \emptyset} D = 1$
38	36 37	eqtr4i	$⊢ \prod_{j \in \emptyset} \prod_{k \in B} C = \prod_{z \in \emptyset} D$
39	38	2a1i	$⊢ φ \to (\emptyset \subseteq A \to \prod_{j \in \emptyset} \prod_{k \in B} C = \prod_{z \in \emptyset} D)$
40		ssun1	$⊢ x \subseteq x \cup \{y\}$
41		sstr	$⊢ (x \subseteq x \cup \{y\} \land x \cup \{y\} \subseteq A) \to x \subseteq A$
42	40 41	mpan	$⊢ x \cup \{y\} \subseteq A \to x \subseteq A$
43	42	imim1i	$⊢ (x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D)$
44	2	ad2antrr	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to A \in Fin$
45	3	ad4ant14	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land j \in A) \to B \in Fin$
46	4	ad4ant14	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land (j \in A \land k \in B)) \to C \in ℂ$
47		simplr	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to \neg y \in x$
48		simpr	$⊢ ((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \to x \cup \{y\} \subseteq A$
49		biid	$⊢ \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
50	1 44 45 46 47 48 49	fprod2dlem	$⊢ (((φ \land \neg y \in x) \land x \cup \{y\} \subseteq A) \land \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$
51	50	exp31	$⊢ (φ \land \neg y \in x) \to (x \cup \{y\} \subseteq A \to (\prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
52	51	a2d	$⊢ (φ \land \neg y \in x) \to ((x \cup \{y\} \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
53	43 52	syl5	$⊢ (φ \land \neg y \in x) \to ((x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D))$
54	53	expcom	$⊢ \neg y \in x \to (φ \to ((x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D) \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
55	54	a2d	$⊢ \neg y \in x \to ((φ \to (x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D)) \to (φ \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
56	55	adantl	$⊢ (x \in Fin \land \neg y \in x) \to ((φ \to (x \subseteq A \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D)) \to (φ \to (x \cup \{y\} \subseteq A \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D)))$
57	14 21 28 35 39 56	findcard2s	$⊢ A \in Fin \to (φ \to (A \subseteq A \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D))$
58	2 57	mpcom	$⊢ φ \to (A \subseteq A \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D)$
59	5 58	mpi	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in A} (\{j\} \times B)} D$

Metamath Proof Explorer

Theorem fprod2d

Proof