fsum2cn

Description: Version of fsumcn for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014)

	Ref	Expression
Hypotheses	fsumcn.3	$⊢ K = TopOpen (ℂ_{fld})$
	fsumcn.4	$⊢ φ \to J \in TopOn (X)$
	fsumcn.5	$⊢ φ \to A \in Fin$
	fsum2cn.7	$⊢ φ \to L \in TopOn (Y)$
	fsum2cn.8	$⊢ (φ \land k \in A) \to (x \in X, y \in Y ⟼ B) \in ((J \times_{t} L) Cn K)$
Assertion	fsum2cn	$⊢ φ \to (x \in X, y \in Y ⟼ \sum_{k \in A} B) \in ((J \times_{t} L) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		fsumcn.3	$⊢ K = TopOpen (ℂ_{fld})$
2		fsumcn.4	$⊢ φ \to J \in TopOn (X)$
3		fsumcn.5	$⊢ φ \to A \in Fin$
4		fsum2cn.7	$⊢ φ \to L \in TopOn (Y)$
5		fsum2cn.8	$⊢ (φ \land k \in A) \to (x \in X, y \in Y ⟼ B) \in ((J \times_{t} L) Cn K)$
6		nfcv	$⊢ \underline{Ⅎ} u \sum_{k \in A} B$
7		nfcv	$⊢ \underline{Ⅎ} v \sum_{k \in A} B$
8		nfcv	$⊢ \underline{Ⅎ} x A$
9		nfcv	$⊢ \underline{Ⅎ} x v$
10		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ u / x ⦌ B$
11	9 10	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ v / y ⦌ ⦋ u / x ⦌ B$
12	8 11	nfsum	$⊢ \underline{Ⅎ} x \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B$
13		nfcv	$⊢ \underline{Ⅎ} y A$
14		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ v / y ⦌ ⦋ u / x ⦌ B$
15	13 14	nfsum	$⊢ \underline{Ⅎ} y \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B$
16		csbeq1a	$⊢ x = u \to B = ⦋ u / x ⦌ B$
17		csbeq1a	$⊢ y = v \to ⦋ u / x ⦌ B = ⦋ v / y ⦌ ⦋ u / x ⦌ B$
18	16 17	sylan9eq	$⊢ (x = u \land y = v) \to B = ⦋ v / y ⦌ ⦋ u / x ⦌ B$
19	18	sumeq2sdv	$⊢ (x = u \land y = v) \to \sum_{k \in A} B = \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B$
20	6 7 12 15 19	cbvmpo	$⊢ (x \in X, y \in Y ⟼ \sum_{k \in A} B) = (u \in X, v \in Y ⟼ \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B)$
21		vex	$⊢ u \in V$
22		vex	$⊢ v \in V$
23	21 22	op2ndd	$⊢ z = ⟨u, v⟩ \to 2^{nd} (z) = v$
24	23	csbeq1d	$⊢ z = ⟨u, v⟩ \to ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B = ⦋ v / y ⦌ ⦋ 1^{st} (z) / x ⦌ B$
25	21 22	op1std	$⊢ z = ⟨u, v⟩ \to 1^{st} (z) = u$
26	25	csbeq1d	$⊢ z = ⟨u, v⟩ \to ⦋ 1^{st} (z) / x ⦌ B = ⦋ u / x ⦌ B$
27	26	csbeq2dv	$⊢ z = ⟨u, v⟩ \to ⦋ v / y ⦌ ⦋ 1^{st} (z) / x ⦌ B = ⦋ v / y ⦌ ⦋ u / x ⦌ B$
28	24 27	eqtrd	$⊢ z = ⟨u, v⟩ \to ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B = ⦋ v / y ⦌ ⦋ u / x ⦌ B$
29	28	sumeq2sdv	$⊢ z = ⟨u, v⟩ \to \sum_{k \in A} ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B = \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B$
30	29	mpompt	$⊢ (z \in (X \times Y) ⟼ \sum_{k \in A} ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B) = (u \in X, v \in Y ⟼ \sum_{k \in A} ⦋ v / y ⦌ ⦋ u / x ⦌ B)$
31	20 30	eqtr4i	$⊢ (x \in X, y \in Y ⟼ \sum_{k \in A} B) = (z \in (X \times Y) ⟼ \sum_{k \in A} ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B)$
32		txtopon	$⊢ (J \in TopOn (X) \land L \in TopOn (Y)) \to J \times_{t} L \in TopOn (X \times Y)$
33	2 4 32	syl2anc	$⊢ φ \to J \times_{t} L \in TopOn (X \times Y)$
34		nfcv	$⊢ \underline{Ⅎ} u B$
35		nfcv	$⊢ \underline{Ⅎ} v B$
36	34 35 11 14 18	cbvmpo	$⊢ (x \in X, y \in Y ⟼ B) = (u \in X, v \in Y ⟼ ⦋ v / y ⦌ ⦋ u / x ⦌ B)$
37	28	mpompt	$⊢ (z \in (X \times Y) ⟼ ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B) = (u \in X, v \in Y ⟼ ⦋ v / y ⦌ ⦋ u / x ⦌ B)$
38	36 37	eqtr4i	$⊢ (x \in X, y \in Y ⟼ B) = (z \in (X \times Y) ⟼ ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B)$
39	38 5	eqeltrrid	$⊢ (φ \land k \in A) \to (z \in (X \times Y) ⟼ ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B) \in ((J \times_{t} L) Cn K)$
40	1 33 3 39	fsumcn	$⊢ φ \to (z \in (X \times Y) ⟼ \sum_{k \in A} ⦋ 2^{nd} (z) / y ⦌ ⦋ 1^{st} (z) / x ⦌ B) \in ((J \times_{t} L) Cn K)$
41	31 40	eqeltrid	$⊢ φ \to (x \in X, y \in Y ⟼ \sum_{k \in A} B) \in ((J \times_{t} L) Cn K)$

Metamath Proof Explorer

Theorem fsum2cn

Proof