itgfsum

Description: Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014)

	Ref	Expression
Hypotheses	itgfsum.1	$⊢ φ \to A \in dom vol$
	itgfsum.2	$⊢ φ \to B \in Fin$
	itgfsum.3	$⊢ (φ \land (x \in A \land k \in B)) \to C \in V$
	itgfsum.4	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \in 𝐿^{1}$
Assertion	itgfsum	$⊢ φ \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x)$

Proof

Step	Hyp	Ref	Expression
1		itgfsum.1	$⊢ φ \to A \in dom vol$
2		itgfsum.2	$⊢ φ \to B \in Fin$
3		itgfsum.3	$⊢ (φ \land (x \in A \land k \in B)) \to C \in V$
4		itgfsum.4	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \in 𝐿^{1}$
5		ssid	$⊢ B \subseteq B$
6		sseq1	$⊢ t = \emptyset \to (t \subseteq B \leftrightarrow \emptyset \subseteq B)$
7		itgz	$⊢ \int_{A} 0 d x = 0$
8		sumeq1	$⊢ t = \emptyset \to \sum_{k \in t} C = \sum_{k \in \emptyset} C$
9		sum0	$⊢ \sum_{k \in \emptyset} C = 0$
10	8 9	eqtrdi	$⊢ t = \emptyset \to \sum_{k \in t} C = 0$
11	10	adantr	$⊢ (t = \emptyset \land x \in A) \to \sum_{k \in t} C = 0$
12	11	itgeq2dv	$⊢ t = \emptyset \to \int_{A} \sum_{k \in t} C d x = \int_{A} 0 d x$
13		sumeq1	$⊢ t = \emptyset \to \sum_{k \in t} \int_{A} C d x = \sum_{k \in \emptyset} \int_{A} C d x$
14		sum0	$⊢ \sum_{k \in \emptyset} \int_{A} C d x = 0$
15	13 14	eqtrdi	$⊢ t = \emptyset \to \sum_{k \in t} \int_{A} C d x = 0$
16	7 12 15	3eqtr4a	$⊢ t = \emptyset \to \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x$
17	10	mpteq2dv	$⊢ t = \emptyset \to (x \in A ⟼ \sum_{k \in t} C) = (x \in A ⟼ 0)$
18		fconstmpt	$⊢ A \times \{0\} = (x \in A ⟼ 0)$
19	17 18	eqtr4di	$⊢ t = \emptyset \to (x \in A ⟼ \sum_{k \in t} C) = A \times \{0\}$
20	19	eleq1d	$⊢ t = \emptyset \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \leftrightarrow A \times \{0\} \in 𝐿^{1})$
21	20	anbi1d	$⊢ t = \emptyset \to (((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x) \leftrightarrow (A \times \{0\} \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x))$
22	16 21	mpbiran2d	$⊢ t = \emptyset \to (((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x) \leftrightarrow A \times \{0\} \in 𝐿^{1})$
23	6 22	imbi12d	$⊢ t = \emptyset \to ((t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x)) \leftrightarrow (\emptyset \subseteq B \to A \times \{0\} \in 𝐿^{1}))$
24	23	imbi2d	$⊢ t = \emptyset \to ((φ \to (t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x))) \leftrightarrow (φ \to (\emptyset \subseteq B \to A \times \{0\} \in 𝐿^{1})))$
25		sseq1	$⊢ t = w \to (t \subseteq B \leftrightarrow w \subseteq B)$
26		sumeq1	$⊢ t = w \to \sum_{k \in t} C = \sum_{k \in w} C$
27	26	mpteq2dv	$⊢ t = w \to (x \in A ⟼ \sum_{k \in t} C) = (x \in A ⟼ \sum_{k \in w} C)$
28	27	eleq1d	$⊢ t = w \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \leftrightarrow (x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1})$
29	26	adantr	$⊢ (t = w \land x \in A) \to \sum_{k \in t} C = \sum_{k \in w} C$
30	29	itgeq2dv	$⊢ t = w \to \int_{A} \sum_{k \in t} C d x = \int_{A} \sum_{k \in w} C d x$
31		sumeq1	$⊢ t = w \to \sum_{k \in t} \int_{A} C d x = \sum_{k \in w} \int_{A} C d x$
32	30 31	eqeq12d	$⊢ t = w \to (\int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x \leftrightarrow \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)$
33	28 32	anbi12d	$⊢ t = w \to (((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x) \leftrightarrow ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x))$
34	25 33	imbi12d	$⊢ t = w \to ((t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x)) \leftrightarrow (w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)))$
35	34	imbi2d	$⊢ t = w \to ((φ \to (t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x))) \leftrightarrow (φ \to (w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x))))$
36		sseq1	$⊢ t = w \cup \{z\} \to (t \subseteq B \leftrightarrow w \cup \{z\} \subseteq B)$
37		sumeq1	$⊢ t = w \cup \{z\} \to \sum_{k \in t} C = \sum_{k \in w \cup \{z\}} C$
38	37	mpteq2dv	$⊢ t = w \cup \{z\} \to (x \in A ⟼ \sum_{k \in t} C) = (x \in A ⟼ \sum_{k \in w \cup \{z\}} C)$
39	38	eleq1d	$⊢ t = w \cup \{z\} \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \leftrightarrow (x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1})$
40	37	adantr	$⊢ (t = w \cup \{z\} \land x \in A) \to \sum_{k \in t} C = \sum_{k \in w \cup \{z\}} C$
41	40	itgeq2dv	$⊢ t = w \cup \{z\} \to \int_{A} \sum_{k \in t} C d x = \int_{A} \sum_{k \in w \cup \{z\}} C d x$
42		sumeq1	$⊢ t = w \cup \{z\} \to \sum_{k \in t} \int_{A} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x$
43	41 42	eqeq12d	$⊢ t = w \cup \{z\} \to (\int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x \leftrightarrow \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)$
44	39 43	anbi12d	$⊢ t = w \cup \{z\} \to (((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x) \leftrightarrow ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))$
45	36 44	imbi12d	$⊢ t = w \cup \{z\} \to ((t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x)) \leftrightarrow (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)))$
46	45	imbi2d	$⊢ t = w \cup \{z\} \to ((φ \to (t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x))) \leftrightarrow (φ \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))))$
47		sseq1	$⊢ t = B \to (t \subseteq B \leftrightarrow B \subseteq B)$
48		sumeq1	$⊢ t = B \to \sum_{k \in t} C = \sum_{k \in B} C$
49	48	mpteq2dv	$⊢ t = B \to (x \in A ⟼ \sum_{k \in t} C) = (x \in A ⟼ \sum_{k \in B} C)$
50	49	eleq1d	$⊢ t = B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \leftrightarrow (x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1})$
51	48	adantr	$⊢ (t = B \land x \in A) \to \sum_{k \in t} C = \sum_{k \in B} C$
52	51	itgeq2dv	$⊢ t = B \to \int_{A} \sum_{k \in t} C d x = \int_{A} \sum_{k \in B} C d x$
53		sumeq1	$⊢ t = B \to \sum_{k \in t} \int_{A} C d x = \sum_{k \in B} \int_{A} C d x$
54	52 53	eqeq12d	$⊢ t = B \to (\int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x \leftrightarrow \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x)$
55	50 54	anbi12d	$⊢ t = B \to (((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x) \leftrightarrow ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x))$
56	47 55	imbi12d	$⊢ t = B \to ((t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x)) \leftrightarrow (B \subseteq B \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x)))$
57	56	imbi2d	$⊢ t = B \to ((φ \to (t \subseteq B \to ((x \in A ⟼ \sum_{k \in t} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in t} C d x = \sum_{k \in t} \int_{A} C d x))) \leftrightarrow (φ \to (B \subseteq B \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x))))$
58		ibl0	$⊢ A \in dom vol \to A \times \{0\} \in 𝐿^{1}$
59	1 58	syl	$⊢ φ \to A \times \{0\} \in 𝐿^{1}$
60	59	a1d	$⊢ φ \to (\emptyset \subseteq B \to A \times \{0\} \in 𝐿^{1})$
61		ssun1	$⊢ w \subseteq w \cup \{z\}$
62		sstr	$⊢ (w \subseteq w \cup \{z\} \land w \cup \{z\} \subseteq B) \to w \subseteq B$
63	61 62	mpan	$⊢ w \cup \{z\} \subseteq B \to w \subseteq B$
64	63	imim1i	$⊢ (w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x))$
65		nfcv	$⊢ \underline{Ⅎ} m C$
66		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ C$
67		csbeq1a	$⊢ k = m \to C = ⦋ m / k ⦌ C$
68	65 66 67	cbvsumi	$⊢ \sum_{k \in w \cup \{z\}} C = \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C$
69		simprl	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \neg z \in w$
70		disjsn	$⊢ w \cap \{z\} = \emptyset \leftrightarrow \neg z \in w$
71	69 70	sylibr	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to w \cap \{z\} = \emptyset$
72	71	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to w \cap \{z\} = \emptyset$
73		eqidd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to w \cup \{z\} = w \cup \{z\}$
74	2	adantr	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to B \in Fin$
75		simprr	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to w \cup \{z\} \subseteq B$
76	74 75	ssfid	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to w \cup \{z\} \in Fin$
77	76	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to w \cup \{z\} \in Fin$
78		simplrr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to w \cup \{z\} \subseteq B$
79	78	sselda	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \land m \in (w \cup \{z\})) \to m \in B$
80		iblmbf	$⊢ (x \in A ⟼ C) \in 𝐿^{1} \to (x \in A ⟼ C) \in MblFn$
81	4 80	syl	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \in MblFn$
82	3	anass1rs	$⊢ ((φ \land k \in B) \land x \in A) \to C \in V$
83	81 82	mbfmptcl	$⊢ ((φ \land k \in B) \land x \in A) \to C \in ℂ$
84	83	an32s	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℂ$
85	84	ralrimiva	$⊢ (φ \land x \in A) \to \forall k \in B C \in ℂ$
86	85	adantlr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \forall k \in B C \in ℂ$
87	65	nfel1	$⊢ Ⅎ m C \in ℂ$
88	66	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ C \in ℂ$
89	67	eleq1d	$⊢ k = m \to (C \in ℂ \leftrightarrow ⦋ m / k ⦌ C \in ℂ)$
90	87 88 89	cbvralw	$⊢ \forall k \in B C \in ℂ \leftrightarrow \forall m \in B ⦋ m / k ⦌ C \in ℂ$
91	86 90	sylib	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \forall m \in B ⦋ m / k ⦌ C \in ℂ$
92	91	r19.21bi	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \land m \in B) \to ⦋ m / k ⦌ C \in ℂ$
93	79 92	syldan	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \land m \in (w \cup \{z\})) \to ⦋ m / k ⦌ C \in ℂ$
94	72 73 77 93	fsumsplit	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C = \sum_{m \in w} ⦋ m / k ⦌ C + \sum_{m \in \{z\}} ⦋ m / k ⦌ C$
95		vex	$⊢ z \in V$
96		csbeq1	$⊢ m = z \to ⦋ m / k ⦌ C = ⦋ z / k ⦌ C$
97	96	eleq1d	$⊢ m = z \to (⦋ m / k ⦌ C \in ℂ \leftrightarrow ⦋ z / k ⦌ C \in ℂ)$
98	75	unssbd	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \{z\} \subseteq B$
99	95	snss	$⊢ z \in B \leftrightarrow \{z\} \subseteq B$
100	98 99	sylibr	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to z \in B$
101	100	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to z \in B$
102	97 91 101	rspcdva	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to ⦋ z / k ⦌ C \in ℂ$
103	96	sumsn	$⊢ (z \in V \land ⦋ z / k ⦌ C \in ℂ) \to \sum_{m \in \{z\}} ⦋ m / k ⦌ C = ⦋ z / k ⦌ C$
104	95 102 103	sylancr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{m \in \{z\}} ⦋ m / k ⦌ C = ⦋ z / k ⦌ C$
105	104	oveq2d	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{m \in w} ⦋ m / k ⦌ C + \sum_{m \in \{z\}} ⦋ m / k ⦌ C = \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C$
106	94 105	eqtrd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C = \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C$
107	68 106	syl5eq	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in w \cup \{z\}} C = \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C$
108	107	mpteq2dva	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in w \cup \{z\}} C) = (x \in A ⟼ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C)$
109		nfcv	$⊢ \underline{Ⅎ} y (\sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C)$
110		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C$
111		nfcv	$⊢ \underline{Ⅎ} x +$
112		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ ⦋ z / k ⦌ C$
113	110 111 112	nfov	$⊢ \underline{Ⅎ} x (⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C)$
114		csbeq1a	$⊢ x = y \to \sum_{m \in w} ⦋ m / k ⦌ C = ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C$
115		csbeq1a	$⊢ x = y \to ⦋ z / k ⦌ C = ⦋ y / x ⦌ ⦋ z / k ⦌ C$
116	114 115	oveq12d	$⊢ x = y \to \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C = ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C$
117	109 113 116	cbvmpt	$⊢ (x \in A ⟼ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C) = (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C)$
118	108 117	eqtrdi	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in w \cup \{z\}} C) = (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C)$
119	118	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (x \in A ⟼ \sum_{k \in w \cup \{z\}} C) = (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C)$
120		sumex	$⊢ \sum_{m \in w} ⦋ m / k ⦌ C \in V$
121	120	csbex	$⊢ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C \in V$
122	121	a1i	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \land y \in A) \to ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C \in V$
123	65 66 67	cbvsumi	$⊢ \sum_{k \in w} C = \sum_{m \in w} ⦋ m / k ⦌ C$
124	123	mpteq2i	$⊢ (x \in A ⟼ \sum_{k \in w} C) = (x \in A ⟼ \sum_{m \in w} ⦋ m / k ⦌ C)$
125		nfcv	$⊢ \underline{Ⅎ} y \sum_{m \in w} ⦋ m / k ⦌ C$
126	125 110 114	cbvmpt	$⊢ (x \in A ⟼ \sum_{m \in w} ⦋ m / k ⦌ C) = (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C)$
127	124 126	eqtri	$⊢ (x \in A ⟼ \sum_{k \in w} C) = (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C)$
128		simprl	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1}$
129	127 128	eqeltrrid	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C) \in 𝐿^{1}$
130	102	elexd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land x \in A) \to ⦋ z / k ⦌ C \in V$
131	130	ralrimiva	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \forall x \in A ⦋ z / k ⦌ C \in V$
132	131	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \forall x \in A ⦋ z / k ⦌ C \in V$
133		nfv	$⊢ Ⅎ y ⦋ z / k ⦌ C \in V$
134	112	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ ⦋ z / k ⦌ C \in V$
135	115	eleq1d	$⊢ x = y \to (⦋ z / k ⦌ C \in V \leftrightarrow ⦋ y / x ⦌ ⦋ z / k ⦌ C \in V)$
136	133 134 135	cbvralw	$⊢ \forall x \in A ⦋ z / k ⦌ C \in V \leftrightarrow \forall y \in A ⦋ y / x ⦌ ⦋ z / k ⦌ C \in V$
137	132 136	sylib	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \forall y \in A ⦋ y / x ⦌ ⦋ z / k ⦌ C \in V$
138	137	r19.21bi	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \land y \in A) \to ⦋ y / x ⦌ ⦋ z / k ⦌ C \in V$
139		nfcv	$⊢ \underline{Ⅎ} y ⦋ z / k ⦌ C$
140	139 112 115	cbvmpt	$⊢ (x \in A ⟼ ⦋ z / k ⦌ C) = (y \in A ⟼ ⦋ y / x ⦌ ⦋ z / k ⦌ C)$
141	96	mpteq2dv	$⊢ m = z \to (x \in A ⟼ ⦋ m / k ⦌ C) = (x \in A ⟼ ⦋ z / k ⦌ C)$
142	141	eleq1d	$⊢ m = z \to ((x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1} \leftrightarrow (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝐿^{1})$
143	4	ralrimiva	$⊢ φ \to \forall k \in B (x \in A ⟼ C) \in 𝐿^{1}$
144		nfv	$⊢ Ⅎ m (x \in A ⟼ C) \in 𝐿^{1}$
145		nfcv	$⊢ \underline{Ⅎ} k A$
146	145 66	nfmpt	$⊢ \underline{Ⅎ} k (x \in A ⟼ ⦋ m / k ⦌ C)$
147	146	nfel1	$⊢ Ⅎ k (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1}$
148	67	mpteq2dv	$⊢ k = m \to (x \in A ⟼ C) = (x \in A ⟼ ⦋ m / k ⦌ C)$
149	148	eleq1d	$⊢ k = m \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1})$
150	144 147 149	cbvralw	$⊢ \forall k \in B (x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow \forall m \in B (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1}$
151	143 150	sylib	$⊢ φ \to \forall m \in B (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1}$
152	151	adantr	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \forall m \in B (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1}$
153	142 152 100	rspcdva	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝐿^{1}$
154	140 153	eqeltrrid	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to (y \in A ⟼ ⦋ y / x ⦌ ⦋ z / k ⦌ C) \in 𝐿^{1}$
155	154	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (y \in A ⟼ ⦋ y / x ⦌ ⦋ z / k ⦌ C) \in 𝐿^{1}$
156	122 129 138 155	ibladd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (y \in A ⟼ ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C) \in 𝐿^{1}$
157	119 156	eqeltrd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1}$
158	122 129 138 155	itgadd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} (⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C) d y = \int_{A} ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C d y + \int_{A} ⦋ y / x ⦌ ⦋ z / k ⦌ C d y$
159	116 109 113	cbvitg	$⊢ \int_{A} (\sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C) d x = \int_{A} (⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C + ⦋ y / x ⦌ ⦋ z / k ⦌ C) d y$
160	114 125 110	cbvitg	$⊢ \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x = \int_{A} ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C d y$
161	115 139 112	cbvitg	$⊢ \int_{A} ⦋ z / k ⦌ C d x = \int_{A} ⦋ y / x ⦌ ⦋ z / k ⦌ C d y$
162	160 161	oveq12i	$⊢ \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x + \int_{A} ⦋ z / k ⦌ C d x = \int_{A} ⦋ y / x ⦌ \sum_{m \in w} ⦋ m / k ⦌ C d y + \int_{A} ⦋ y / x ⦌ ⦋ z / k ⦌ C d y$
163	158 159 162	3eqtr4g	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} (\sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C) d x = \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x + \int_{A} ⦋ z / k ⦌ C d x$
164	106	itgeq2dv	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \int_{A} \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C d x = \int_{A} (\sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C) d x$
165	164	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C d x = \int_{A} (\sum_{m \in w} ⦋ m / k ⦌ C + ⦋ z / k ⦌ C) d x$
166		eqidd	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to w \cup \{z\} = w \cup \{z\}$
167	75	sselda	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land m \in (w \cup \{z\})) \to m \in B$
168	92	an32s	$⊢ (((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land m \in B) \land x \in A) \to ⦋ m / k ⦌ C \in ℂ$
169	152	r19.21bi	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land m \in B) \to (x \in A ⟼ ⦋ m / k ⦌ C) \in 𝐿^{1}$
170	168 169	itgcl	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land m \in B) \to \int_{A} ⦋ m / k ⦌ C d x \in ℂ$
171	167 170	syldan	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land m \in (w \cup \{z\})) \to \int_{A} ⦋ m / k ⦌ C d x \in ℂ$
172	71 166 76 171	fsumsplit	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \sum_{m \in w \cup \{z\}} \int_{A} ⦋ m / k ⦌ C d x = \sum_{m \in w} \int_{A} ⦋ m / k ⦌ C d x + \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
173	172	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \sum_{m \in w \cup \{z\}} \int_{A} ⦋ m / k ⦌ C d x = \sum_{m \in w} \int_{A} ⦋ m / k ⦌ C d x + \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
174		simprr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x$
175		itgeq2	$⊢ \forall x \in A \sum_{k \in w} C = \sum_{m \in w} ⦋ m / k ⦌ C \to \int_{A} \sum_{k \in w} C d x = \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x$
176	123	a1i	$⊢ x \in A \to \sum_{k \in w} C = \sum_{m \in w} ⦋ m / k ⦌ C$
177	175 176	mprg	$⊢ \int_{A} \sum_{k \in w} C d x = \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x$
178		nfcv	$⊢ \underline{Ⅎ} m \int_{A} C d x$
179	145 66	nfitg	$⊢ \underline{Ⅎ} k \int_{A} ⦋ m / k ⦌ C d x$
180	67	adantr	$⊢ (k = m \land x \in A) \to C = ⦋ m / k ⦌ C$
181	180	itgeq2dv	$⊢ k = m \to \int_{A} C d x = \int_{A} ⦋ m / k ⦌ C d x$
182	178 179 181	cbvsumi	$⊢ \sum_{k \in w} \int_{A} C d x = \sum_{m \in w} \int_{A} ⦋ m / k ⦌ C d x$
183	174 177 182	3eqtr3g	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x = \sum_{m \in w} \int_{A} ⦋ m / k ⦌ C d x$
184	102 153	itgcl	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to \int_{A} ⦋ z / k ⦌ C d x \in ℂ$
185	184	adantr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} ⦋ z / k ⦌ C d x \in ℂ$
186	96	adantr	$⊢ (m = z \land x \in A) \to ⦋ m / k ⦌ C = ⦋ z / k ⦌ C$
187	186	itgeq2dv	$⊢ m = z \to \int_{A} ⦋ m / k ⦌ C d x = \int_{A} ⦋ z / k ⦌ C d x$
188	187	sumsn	$⊢ (z \in V \land \int_{A} ⦋ z / k ⦌ C d x \in ℂ) \to \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x = \int_{A} ⦋ z / k ⦌ C d x$
189	95 185 188	sylancr	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x = \int_{A} ⦋ z / k ⦌ C d x$
190	189	eqcomd	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} ⦋ z / k ⦌ C d x = \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
191	183 190	oveq12d	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x + \int_{A} ⦋ z / k ⦌ C d x = \sum_{m \in w} \int_{A} ⦋ m / k ⦌ C d x + \sum_{m \in \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
192	173 191	eqtr4d	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \sum_{m \in w \cup \{z\}} \int_{A} ⦋ m / k ⦌ C d x = \int_{A} \sum_{m \in w} ⦋ m / k ⦌ C d x + \int_{A} ⦋ z / k ⦌ C d x$
193	163 165 192	3eqtr4d	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C d x = \sum_{m \in w \cup \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
194		itgeq2	$⊢ \forall x \in A \sum_{k \in w \cup \{z\}} C = \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C \to \int_{A} \sum_{k \in w \cup \{z\}} C d x = \int_{A} \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C d x$
195	68	a1i	$⊢ x \in A \to \sum_{k \in w \cup \{z\}} C = \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C$
196	194 195	mprg	$⊢ \int_{A} \sum_{k \in w \cup \{z\}} C d x = \int_{A} \sum_{m \in w \cup \{z\}} ⦋ m / k ⦌ C d x$
197	178 179 181	cbvsumi	$⊢ \sum_{k \in w \cup \{z\}} \int_{A} C d x = \sum_{m \in w \cup \{z\}} \int_{A} ⦋ m / k ⦌ C d x$
198	193 196 197	3eqtr4g	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x$
199	157 198	jca	$⊢ ((φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \land ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)$
200	199	ex	$⊢ (φ \land (\neg z \in w \land w \cup \{z\} \subseteq B)) \to (((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x) \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))$
201	200	expr	$⊢ (φ \land \neg z \in w) \to (w \cup \{z\} \subseteq B \to (((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x) \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)))$
202	201	a2d	$⊢ (φ \land \neg z \in w) \to ((w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)))$
203	64 202	syl5	$⊢ (φ \land \neg z \in w) \to ((w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x)))$
204	203	expcom	$⊢ \neg z \in w \to (φ \to ((w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))))$
205	204	adantl	$⊢ (w \in Fin \land \neg z \in w) \to (φ \to ((w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x)) \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))))$
206	205	a2d	$⊢ (w \in Fin \land \neg z \in w) \to ((φ \to (w \subseteq B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w} C d x = \sum_{k \in w} \int_{A} C d x))) \to (φ \to (w \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in w \cup \{z\}} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in w \cup \{z\}} C d x = \sum_{k \in w \cup \{z\}} \int_{A} C d x))))$
207	24 35 46 57 60 206	findcard2s	$⊢ B \in Fin \to (φ \to (B \subseteq B \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x)))$
208	2 207	mpcom	$⊢ φ \to (B \subseteq B \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x))$
209	5 208	mpi	$⊢ φ \to ((x \in A ⟼ \sum_{k \in B} C) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} C d x = \sum_{k \in B} \int_{A} C d x)$

Metamath Proof Explorer

Theorem itgfsum

Proof