fsum2dlem

Description: Lemma for fsum2d - induction step. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsum2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
	fsum2d.2	$⊢ φ \to A \in Fin$
	fsum2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fsum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
	fsum2d.5	$⊢ φ \to \neg y \in x$
	fsum2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
	fsum2d.7	$⊢ ψ \leftrightarrow \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
Assertion	fsum2dlem	$⊢ (φ \land ψ) \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Proof

Step	Hyp	Ref	Expression
1		fsum2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
2		fsum2d.2	$⊢ φ \to A \in Fin$
3		fsum2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fsum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
5		fsum2d.5	$⊢ φ \to \neg y \in x$
6		fsum2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
7		fsum2d.7	$⊢ ψ \leftrightarrow \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
8	7	bilani	$⊢ (φ \land ψ) \to \sum_{j \in x} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
9		csbeq1a	$⊢ j = m \to B = ⦋ m / j ⦌ B$
10		csbeq1a	$⊢ j = m \to C = ⦋ m / j ⦌ C$
11	10	adantr	$⊢ (j = m \land k \in B) \to C = ⦋ m / j ⦌ C$
12	9 11	sumeq12dv	$⊢ j = m \to \sum_{k \in B} C = \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
13		nfcv	$⊢ \underline{Ⅎ} m \sum_{k \in B} C$
14		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ B$
15		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ C$
16	14 15	nfsum	$⊢ \underline{Ⅎ} j \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
17	12 13 16	cbvsum	$⊢ \sum_{j \in \{y\}} \sum_{k \in B} C = \sum_{m \in \{y\}} \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
18	6	unssbd	$⊢ φ \to \{y\} \subseteq A$
19		vex	$⊢ y \in V$
20	19	snss	$⊢ y \in A \leftrightarrow \{y\} \subseteq A$
21	18 20	sylibr	$⊢ φ \to y \in A$
22	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
23		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ B$
24	23	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ B \in Fin$
25		csbeq1a	$⊢ j = y \to B = ⦋ y / j ⦌ B$
26	25	eleq1d	$⊢ j = y \to (B \in Fin \leftrightarrow ⦋ y / j ⦌ B \in Fin)$
27	24 26	rspc	$⊢ y \in A \to (\forall j \in A B \in Fin \to ⦋ y / j ⦌ B \in Fin)$
28	21 22 27	sylc	$⊢ φ \to ⦋ y / j ⦌ B \in Fin$
29	4	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B C \in ℂ$
30		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ C$
31	30	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ C \in ℂ$
32	23 31	nfralw	$⊢ Ⅎ j \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
33		csbeq1a	$⊢ j = y \to C = ⦋ y / j ⦌ C$
34	33	eleq1d	$⊢ j = y \to (C \in ℂ \leftrightarrow ⦋ y / j ⦌ C \in ℂ)$
35	25 34	raleqbidv	$⊢ j = y \to (\forall k \in B C \in ℂ \leftrightarrow \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
36	32 35	rspc	$⊢ y \in A \to (\forall j \in A \forall k \in B C \in ℂ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
37	21 29 36	sylc	$⊢ φ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
38	37	r19.21bi	$⊢ (φ \land k \in ⦋ y / j ⦌ B) \to ⦋ y / j ⦌ C \in ℂ$
39	28 38	fsumcl	$⊢ φ \to \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ$
40		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ B = ⦋ y / j ⦌ B$
41		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
42	41	adantr	$⊢ (m = y \land k \in ⦋ m / j ⦌ B) \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
43	40 42	sumeq12dv	$⊢ m = y \to \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
44	43	sumsn	$⊢ (y \in A \land \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ) \to \sum_{m \in \{y\}} \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
45	21 39 44	syl2anc	$⊢ φ \to \sum_{m \in \{y\}} \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
46		csbeq1a	$⊢ k = m \to ⦋ y / j ⦌ C = ⦋ m / k ⦌ ⦋ y / j ⦌ C$
47		nfcv	$⊢ \underline{Ⅎ} m ⦋ y / j ⦌ C$
48		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ ⦋ y / j ⦌ C$
49	46 47 48	cbvsum	$⊢ \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \sum_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C$
50		csbeq1	$⊢ m = 2^{nd} (z) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
51		snfi	$⊢ \{y\} \in Fin$
52		xpfi	$⊢ (\{y\} \in Fin \land ⦋ y / j ⦌ B \in Fin) \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
53	51 28 52	sylancr	$⊢ φ \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
54		2ndconst	$⊢ y \in A \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
55	21 54	syl	$⊢ φ \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
56		fvres	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
57	56	adantl	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
58	48	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
59	46	eleq1d	$⊢ k = m \to (⦋ y / j ⦌ C \in ℂ \leftrightarrow ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
60	58 59	rspc	$⊢ m \in ⦋ y / j ⦌ B \to (\forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
61	37 60	mpan9	$⊢ (φ \land m \in ⦋ y / j ⦌ B) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
62	50 53 55 57 61	fsumf1o	$⊢ φ \to \sum_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
63		elxp	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
64		nfv	$⊢ Ⅎ j z = ⟨m, k⟩$
65		nfv	$⊢ Ⅎ j m \in \{y\}$
66	23	nfcri	$⊢ Ⅎ j k \in ⦋ y / j ⦌ B$
67	65 66	nfan	$⊢ Ⅎ j (m \in \{y\} \land k \in ⦋ y / j ⦌ B)$
68	64 67	nfan	$⊢ Ⅎ j (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
69	68	nfex	$⊢ Ⅎ j \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
70		nfv	$⊢ Ⅎ m \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
71		opeq1	$⊢ m = j \to ⟨m, k⟩ = ⟨j, k⟩$
72	71	eqeq2d	$⊢ m = j \to (z = ⟨m, k⟩ \leftrightarrow z = ⟨j, k⟩)$
73		velsn	$⊢ m \in \{y\} \leftrightarrow m = y$
74	73	anbi1i	$⊢ (m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (m = y \land k \in ⦋ y / j ⦌ B)$
75		eqtr2	$⊢ (m = j \land m = y) \to j = y$
76	75 25	syl	$⊢ (m = j \land m = y) \to B = ⦋ y / j ⦌ B$
77	76	eleq2d	$⊢ (m = j \land m = y) \to (k \in B \leftrightarrow k \in ⦋ y / j ⦌ B)$
78	77	pm5.32da	$⊢ m = j \to ((m = y \land k \in B) \leftrightarrow (m = y \land k \in ⦋ y / j ⦌ B))$
79	74 78	bitr4id	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (m = y \land k \in B))$
80		equequ1	$⊢ m = j \to (m = y \leftrightarrow j = y)$
81	80	anbi1d	$⊢ m = j \to ((m = y \land k \in B) \leftrightarrow (j = y \land k \in B))$
82	79 81	bitrd	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (j = y \land k \in B))$
83	72 82	anbi12d	$⊢ m = j \to ((z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
84	83	exbidv	$⊢ m = j \to (\exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
85	69 70 84	cbvexv1	$⊢ \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
86	63 85	bitri	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
87		nfv	$⊢ Ⅎ j φ$
88		nfcv	$⊢ \underline{Ⅎ} j 2^{nd} (z)$
89	88 30	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
90	89	nfeq2	$⊢ Ⅎ j D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
91		nfv	$⊢ Ⅎ k φ$
92		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
93	92	nfeq2	$⊢ Ⅎ k D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
94	1	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = C$
95	33	ad2antrl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to C = ⦋ y / j ⦌ C$
96		fveq2	$⊢ z = ⟨j, k⟩ \to 2^{nd} (z) = 2^{nd} (⟨j, k⟩)$
97		vex	$⊢ j \in V$
98		vex	$⊢ k \in V$
99	97 98	op2nd	$⊢ 2^{nd} (⟨j, k⟩) = k$
100	96 99	eqtr2di	$⊢ z = ⟨j, k⟩ \to k = 2^{nd} (z)$
101	100	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to k = 2^{nd} (z)$
102		csbeq1a	$⊢ k = 2^{nd} (z) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
103	101 102	syl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
104	94 95 103	3eqtrd	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
105	104	expl	$⊢ φ \to ((z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
106	91 93 105	exlimd	$⊢ φ \to (\exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
107	87 90 106	exlimd	$⊢ φ \to (\exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
108	86 107	biimtrid	$⊢ φ \to (z \in (\{y\} \times ⦋ y / j ⦌ B) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
109	108	imp	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
110	109	sumeq2dv	$⊢ φ \to \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
111	62 110	eqtr4d	$⊢ φ \to \sum_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
112	49 111	eqtrid	$⊢ φ \to \sum_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
113	45 112	eqtrd	$⊢ φ \to \sum_{m \in \{y\}} \sum_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
114	17 113	eqtrid	$⊢ φ \to \sum_{j \in \{y\}} \sum_{k \in B} C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
115	114	adantr	$⊢ (φ \land ψ) \to \sum_{j \in \{y\}} \sum_{k \in B} C = \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
116	8 115	oveq12d	$⊢ (φ \land ψ) \to \sum_{j \in x} \sum_{k \in B} C + \sum_{j \in \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D + \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
117		disjsn	$⊢ x \cap \{y\} = \emptyset \leftrightarrow \neg y \in x$
118	5 117	sylibr	$⊢ φ \to x \cap \{y\} = \emptyset$
119		eqidd	$⊢ φ \to x \cup \{y\} = x \cup \{y\}$
120	2 6	ssfid	$⊢ φ \to x \cup \{y\} \in Fin$
121	6	sselda	$⊢ (φ \land j \in (x \cup \{y\})) \to j \in A$
122	4	anassrs	$⊢ ((φ \land j \in A) \land k \in B) \to C \in ℂ$
123	3 122	fsumcl	$⊢ (φ \land j \in A) \to \sum_{k \in B} C \in ℂ$
124	121 123	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to \sum_{k \in B} C \in ℂ$
125	118 119 120 124	fsumsplit	$⊢ φ \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{j \in x} \sum_{k \in B} C + \sum_{j \in \{y\}} \sum_{k \in B} C$
126	125	adantr	$⊢ (φ \land ψ) \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{j \in x} \sum_{k \in B} C + \sum_{j \in \{y\}} \sum_{k \in B} C$
127		eliun	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \leftrightarrow \exists j \in x z \in (\{j\} \times B)$
128		xp1st	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) \in \{j\}$
129		elsni	$⊢ 1^{st} (z) \in \{j\} \to 1^{st} (z) = j$
130	128 129	syl	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) = j$
131	130	adantl	$⊢ (j \in x \land z \in (\{j\} \times B)) \to 1^{st} (z) = j$
132		simpl	$⊢ (j \in x \land z \in (\{j\} \times B)) \to j \in x$
133	131 132	eqeltrd	$⊢ (j \in x \land z \in (\{j\} \times B)) \to 1^{st} (z) \in x$
134	133	rexlimiva	$⊢ \exists j \in x z \in (\{j\} \times B) \to 1^{st} (z) \in x$
135	127 134	sylbi	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \to 1^{st} (z) \in x$
136		xp1st	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to 1^{st} (z) \in \{y\}$
137	135 136	anim12i	$⊢ (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
138		elin	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \leftrightarrow (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B))$
139		elin	$⊢ 1^{st} (z) \in (x \cap \{y\}) \leftrightarrow (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
140	137 138 139	3imtr4i	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to 1^{st} (z) \in (x \cap \{y\})$
141	118	eleq2d	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \leftrightarrow 1^{st} (z) \in \emptyset)$
142		noel	$⊢ \neg 1^{st} (z) \in \emptyset$
143	142	pm2.21i	$⊢ 1^{st} (z) \in \emptyset \to z \in \emptyset$
144	141 143	biimtrdi	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \to z \in \emptyset)$
145	140 144	syl5	$⊢ φ \to (z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to z \in \emptyset)$
146	145	ssrdv	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset$
147		ss0	$⊢ ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
148	146 147	syl	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
149		iunxun	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B)$
150		nfcv	$⊢ \underline{Ⅎ} m (\{j\} \times B)$
151		nfcv	$⊢ \underline{Ⅎ} j \{m\}$
152	151 14	nfxp	$⊢ \underline{Ⅎ} j (\{m\} \times ⦋ m / j ⦌ B)$
153		sneq	$⊢ j = m \to \{j\} = \{m\}$
154	153 9	xpeq12d	$⊢ j = m \to \{j\} \times B = \{m\} \times ⦋ m / j ⦌ B$
155	150 152 154	cbviun	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B)$
156		sneq	$⊢ m = y \to \{m\} = \{y\}$
157	156 40	xpeq12d	$⊢ m = y \to \{m\} \times ⦋ m / j ⦌ B = \{y\} \times ⦋ y / j ⦌ B$
158	19 157	iunxsn	$⊢ ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B) = \{y\} \times ⦋ y / j ⦌ B$
159	155 158	eqtri	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = \{y\} \times ⦋ y / j ⦌ B$
160	159	uneq2i	$⊢ ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
161	149 160	eqtri	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
162	161	a1i	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
163		snfi	$⊢ \{j\} \in Fin$
164	121 3	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to B \in Fin$
165		xpfi	$⊢ (\{j\} \in Fin \land B \in Fin) \to \{j\} \times B \in Fin$
166	163 164 165	sylancr	$⊢ (φ \land j \in (x \cup \{y\})) \to \{j\} \times B \in Fin$
167	166	ralrimiva	$⊢ φ \to \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin$
168		iunfi	$⊢ (x \cup \{y\} \in Fin \land \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin) \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
169	120 167 168	syl2anc	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
170		eliun	$⊢ z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \leftrightarrow \exists j \in (x \cup \{y\}) z \in (\{j\} \times B)$
171		elxp	$⊢ z \in (\{j\} \times B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))$
172		simprl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨m, k⟩$
173		simprrl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m \in \{j\}$
174		elsni	$⊢ m \in \{j\} \to m = j$
175	173 174	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m = j$
176	175	opeq1d	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to ⟨m, k⟩ = ⟨j, k⟩$
177	172 176	eqtrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨j, k⟩$
178	177 1	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D = C$
179		simpll	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to φ$
180	121	adantr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to j \in A$
181		simprrr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to k \in B$
182	179 180 181 4	syl12anc	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to C \in ℂ$
183	178 182	eqeltrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D \in ℂ$
184	183	ex	$⊢ (φ \land j \in (x \cup \{y\})) \to ((z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
185	184	exlimdvv	$⊢ (φ \land j \in (x \cup \{y\})) \to (\exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
186	171 185	biimtrid	$⊢ (φ \land j \in (x \cup \{y\})) \to (z \in (\{j\} \times B) \to D \in ℂ)$
187	186	rexlimdva	$⊢ φ \to (\exists j \in (x \cup \{y\}) z \in (\{j\} \times B) \to D \in ℂ)$
188	170 187	biimtrid	$⊢ φ \to (z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \to D \in ℂ)$
189	188	imp	$⊢ (φ \land z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)) \to D \in ℂ$
190	148 162 169 189	fsumsplit	$⊢ φ \to \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D + \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
191	190	adantr	$⊢ (φ \land ψ) \to \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \sum_{z \in ⋃_{j \in x} (\{j\} \times B)} D + \sum_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
192	116 126 191	3eqtr4d	$⊢ (φ \land ψ) \to \sum_{j \in x \cup \{y\}} \sum_{k \in B} C = \sum_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Metamath Proof Explorer

Theorem fsum2dlem

Proof