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