fsumiunle

Description: Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021)

	Ref	Expression
Hypotheses	fsumiunle.1	$⊢ φ \to A \in Fin$
	fsumiunle.2	$⊢ (φ \land x \in A) \to B \in Fin$
	fsumiunle.3	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℝ$
	fsumiunle.4	$⊢ ((φ \land x \in A) \land k \in B) \to 0 \leq C$
Assertion	fsumiunle	$⊢ φ \to \sum_{k \in ⋃_{x \in A} B} C \leq \sum_{x \in A} \sum_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		fsumiunle.1	$⊢ φ \to A \in Fin$
2		fsumiunle.2	$⊢ (φ \land x \in A) \to B \in Fin$
3		fsumiunle.3	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℝ$
4		fsumiunle.4	$⊢ ((φ \land x \in A) \land k \in B) \to 0 \leq C$
5	1 2	aciunf1	$⊢ φ \to \exists f (f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l)$
6		f1f1orn	$⊢ f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \to f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f$
7	6	anim1i	$⊢ (f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \to (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l)$
8		f1f	$⊢ f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \to f : ⋃_{x \in A} B ⟶ ⋃_{x \in A} (\{x\} \times B)$
9	8	frnd	$⊢ f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \to ran f \subseteq ⋃_{x \in A} (\{x\} \times B)$
10	9	adantr	$⊢ (f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \to ran f \subseteq ⋃_{x \in A} (\{x\} \times B)$
11	7 10	jca	$⊢ (f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \to ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))$
12	11	eximi	$⊢ \exists f (f : ⋃_{x \in A} B \underset{1-1}{⟶} ⋃_{x \in A} (\{x\} \times B) \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \to \exists f ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))$
13	5 12	syl	$⊢ φ \to \exists f ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))$
14		csbeq1a	$⊢ k = y \to C = ⦋ y / k ⦌ C$
15		nfcv	$⊢ \underline{Ⅎ} y C$
16		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ C$
17	14 15 16	cbvsum	$⊢ \sum_{k \in ⋃_{x \in A} B} C = \sum_{y \in ⋃_{x \in A} B} ⦋ y / k ⦌ C$
18		csbeq1	$⊢ y = 2^{nd} (z) \to ⦋ y / k ⦌ C = ⦋ 2^{nd} (z) / k ⦌ C$
19		snfi	$⊢ \{x\} \in Fin$
20		xpfi	$⊢ (\{x\} \in Fin \land B \in Fin) \to \{x\} \times B \in Fin$
21	19 2 20	sylancr	$⊢ (φ \land x \in A) \to \{x\} \times B \in Fin$
22	21	ralrimiva	$⊢ φ \to \forall x \in A \{x\} \times B \in Fin$
23		iunfi	$⊢ (A \in Fin \land \forall x \in A \{x\} \times B \in Fin) \to ⋃_{x \in A} (\{x\} \times B) \in Fin$
24	1 22 23	syl2anc	$⊢ φ \to ⋃_{x \in A} (\{x\} \times B) \in Fin$
25	24	adantr	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to ⋃_{x \in A} (\{x\} \times B) \in Fin$
26		simprr	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to ran f \subseteq ⋃_{x \in A} (\{x\} \times B)$
27	25 26	ssfid	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to ran f \in Fin$
28		simprl	$⊢ (φ \land (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f$
29		f1ocnv	$⊢ f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{x \in A} B$
30	28 29	syl	$⊢ (φ \land (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{x \in A} B$
31	30	adantrlr	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{x \in A} B$
32		nfv	$⊢ Ⅎ x φ$
33		nfcv	$⊢ \underline{Ⅎ} x f$
34		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
35	33	nfrn	$⊢ \underline{Ⅎ} x ran f$
36	33 34 35	nff1o	$⊢ Ⅎ x f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f$
37		nfv	$⊢ Ⅎ x 2^{nd} (f (l)) = l$
38	34 37	nfralw	$⊢ Ⅎ x \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l$
39	36 38	nfan	$⊢ Ⅎ x (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l)$
40		nfcv	$⊢ \underline{Ⅎ} x ran f$
41		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} (\{x\} \times B)$
42	40 41	nfss	$⊢ Ⅎ x ran f \subseteq ⋃_{x \in A} (\{x\} \times B)$
43	39 42	nfan	$⊢ Ⅎ x ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))$
44	32 43	nfan	$⊢ Ⅎ x (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B)))$
45		nfv	$⊢ Ⅎ x z \in ran f$
46	44 45	nfan	$⊢ Ⅎ x ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f)$
47		simpr	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to f (k) = z$
48	47	fveq2d	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to 2^{nd} (f (k)) = 2^{nd} (z)$
49		simplr	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to k \in ⋃_{x \in A} B$
50		simp-4r	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))$
51	50	simpld	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l)$
52	51	simprd	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l$
53	52	ad2antrr	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l$
54		2fveq3	$⊢ l = k \to 2^{nd} (f (l)) = 2^{nd} (f (k))$
55		id	$⊢ l = k \to l = k$
56	54 55	eqeq12d	$⊢ l = k \to (2^{nd} (f (l)) = l \leftrightarrow 2^{nd} (f (k)) = k)$
57	56	rspcva	$⊢ (k \in ⋃_{x \in A} B \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \to 2^{nd} (f (k)) = k$
58	49 53 57	syl2anc	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to 2^{nd} (f (k)) = k$
59	48 58	eqtr3d	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to 2^{nd} (z) = k$
60	51	simpld	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f$
61	60	ad2antrr	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f$
62		f1ocnvfv1	$⊢ (f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land k \in ⋃_{x \in A} B) \to f^{-1} (f (k)) = k$
63	61 49 62	syl2anc	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to f^{-1} (f (k)) = k$
64	47	fveq2d	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to f^{-1} (f (k)) = f^{-1} (z)$
65	59 63 64	3eqtr2rd	$⊢ ((((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \land k \in ⋃_{x \in A} B) \land f (k) = z) \to f^{-1} (z) = 2^{nd} (z)$
66		f1ofn	$⊢ f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \to f Fn ⋃_{x \in A} B$
67	60 66	syl	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to f Fn ⋃_{x \in A} B$
68		simpllr	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to z \in ran f$
69		fvelrnb	$⊢ f Fn ⋃_{x \in A} B \to (z \in ran f \leftrightarrow \exists k \in ⋃_{x \in A} B f (k) = z)$
70	69	biimpa	$⊢ (f Fn ⋃_{x \in A} B \land z \in ran f) \to \exists k \in ⋃_{x \in A} B f (k) = z$
71	67 68 70	syl2anc	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to \exists k \in ⋃_{x \in A} B f (k) = z$
72	65 71	r19.29a	$⊢ ((((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \land x \in A) \land z \in (\{x\} \times B)) \to f^{-1} (z) = 2^{nd} (z)$
73	26	sselda	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \to z \in ⋃_{x \in A} (\{x\} \times B)$
74		eliun	$⊢ z \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \in A z \in (\{x\} \times B)$
75	73 74	sylib	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \to \exists x \in A z \in (\{x\} \times B)$
76	46 72 75	r19.29af	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ran f) \to f^{-1} (z) = 2^{nd} (z)$
77		nfv	$⊢ Ⅎ k (φ \land y \in ⋃_{x \in A} B)$
78		nfcv	$⊢ \underline{Ⅎ} k ℂ$
79	16 78	nfel	$⊢ Ⅎ k ⦋ y / k ⦌ C \in ℂ$
80	77 79	nfim	$⊢ Ⅎ k ((φ \land y \in ⋃_{x \in A} B) \to ⦋ y / k ⦌ C \in ℂ)$
81		eleq1w	$⊢ k = y \to (k \in ⋃_{x \in A} B \leftrightarrow y \in ⋃_{x \in A} B)$
82	81	anbi2d	$⊢ k = y \to ((φ \land k \in ⋃_{x \in A} B) \leftrightarrow (φ \land y \in ⋃_{x \in A} B))$
83	14	eleq1d	$⊢ k = y \to (C \in ℂ \leftrightarrow ⦋ y / k ⦌ C \in ℂ)$
84	82 83	imbi12d	$⊢ k = y \to (((φ \land k \in ⋃_{x \in A} B) \to C \in ℂ) \leftrightarrow ((φ \land y \in ⋃_{x \in A} B) \to ⦋ y / k ⦌ C \in ℂ))$
85		nfcv	$⊢ \underline{Ⅎ} x k$
86	85 34	nfel	$⊢ Ⅎ x k \in ⋃_{x \in A} B$
87	32 86	nfan	$⊢ Ⅎ x (φ \land k \in ⋃_{x \in A} B)$
88	3	adantllr	$⊢ (((φ \land k \in ⋃_{x \in A} B) \land x \in A) \land k \in B) \to C \in ℝ$
89	88	recnd	$⊢ (((φ \land k \in ⋃_{x \in A} B) \land x \in A) \land k \in B) \to C \in ℂ$
90		eliun	$⊢ k \in ⋃_{x \in A} B \leftrightarrow \exists x \in A k \in B$
91	90	biimpi	$⊢ k \in ⋃_{x \in A} B \to \exists x \in A k \in B$
92	91	adantl	$⊢ (φ \land k \in ⋃_{x \in A} B) \to \exists x \in A k \in B$
93	87 89 92	r19.29af	$⊢ (φ \land k \in ⋃_{x \in A} B) \to C \in ℂ$
94	80 84 93	chvarfv	$⊢ (φ \land y \in ⋃_{x \in A} B) \to ⦋ y / k ⦌ C \in ℂ$
95	94	adantlr	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land y \in ⋃_{x \in A} B) \to ⦋ y / k ⦌ C \in ℂ$
96	18 27 31 76 95	fsumf1o	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{y \in ⋃_{x \in A} B} ⦋ y / k ⦌ C = \sum_{z \in ran f} ⦋ 2^{nd} (z) / k ⦌ C$
97	17 96	eqtrid	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{k \in ⋃_{x \in A} B} C = \sum_{z \in ran f} ⦋ 2^{nd} (z) / k ⦌ C$
98	97	eqcomd	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{z \in ran f} ⦋ 2^{nd} (z) / k ⦌ C = \sum_{k \in ⋃_{x \in A} B} C$
99		nfcv	$⊢ \underline{Ⅎ} x z$
100	99 41	nfel	$⊢ Ⅎ x z \in ⋃_{x \in A} (\{x\} \times B)$
101	32 100	nfan	$⊢ Ⅎ x (φ \land z \in ⋃_{x \in A} (\{x\} \times B))$
102		xp2nd	$⊢ z \in (\{x\} \times B) \to 2^{nd} (z) \in B$
103	102	adantl	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land z \in (\{x\} \times B)) \to 2^{nd} (z) \in B$
104	3	ralrimiva	$⊢ (φ \land x \in A) \to \forall k \in B C \in ℝ$
105	104	adantlr	$⊢ ((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \to \forall k \in B C \in ℝ$
106	105	adantr	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land z \in (\{x\} \times B)) \to \forall k \in B C \in ℝ$
107		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ C$
108	107	nfel1	$⊢ Ⅎ k ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
109		csbeq1a	$⊢ k = 2^{nd} (z) \to C = ⦋ 2^{nd} (z) / k ⦌ C$
110	109	eleq1d	$⊢ k = 2^{nd} (z) \to (C \in ℝ \leftrightarrow ⦋ 2^{nd} (z) / k ⦌ C \in ℝ)$
111	108 110	rspc	$⊢ 2^{nd} (z) \in B \to (\forall k \in B C \in ℝ \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ)$
112	111	imp	$⊢ (2^{nd} (z) \in B \land \forall k \in B C \in ℝ) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
113	103 106 112	syl2anc	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land z \in (\{x\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
114	74	biimpi	$⊢ z \in ⋃_{x \in A} (\{x\} \times B) \to \exists x \in A z \in (\{x\} \times B)$
115	114	adantl	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to \exists x \in A z \in (\{x\} \times B)$
116	101 113 115	r19.29af	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
117	116	adantlr	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ⋃_{x \in A} (\{x\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
118		xp1st	$⊢ z \in (\{x\} \times B) \to 1^{st} (z) \in \{x\}$
119		elsni	$⊢ 1^{st} (z) \in \{x\} \to 1^{st} (z) = x$
120	118 119	syl	$⊢ z \in (\{x\} \times B) \to 1^{st} (z) = x$
121	120 102	jca	$⊢ z \in (\{x\} \times B) \to (1^{st} (z) = x \land 2^{nd} (z) \in B)$
122		simplll	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land (1^{st} (z) = x \land 2^{nd} (z) \in B)) \to φ$
123		simplr	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land (1^{st} (z) = x \land 2^{nd} (z) \in B)) \to x \in A$
124	4	ralrimiva	$⊢ (φ \land x \in A) \to \forall k \in B 0 \leq C$
125	122 123 124	syl2anc	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land (1^{st} (z) = x \land 2^{nd} (z) \in B)) \to \forall k \in B 0 \leq C$
126	121 125	sylan2	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land z \in (\{x\} \times B)) \to \forall k \in B 0 \leq C$
127		nfcv	$⊢ \underline{Ⅎ} k 0$
128		nfcv	$⊢ \underline{Ⅎ} k \leq$
129	127 128 107	nfbr	$⊢ Ⅎ k 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
130	109	breq2d	$⊢ k = 2^{nd} (z) \to (0 \leq C \leftrightarrow 0 \leq ⦋ 2^{nd} (z) / k ⦌ C)$
131	129 130	rspc	$⊢ 2^{nd} (z) \in B \to (\forall k \in B 0 \leq C \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C)$
132	131	imp	$⊢ (2^{nd} (z) \in B \land \forall k \in B 0 \leq C) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
133	103 126 132	syl2anc	$⊢ (((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \land z \in (\{x\} \times B)) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
134	101 133 115	r19.29af	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
135	134	adantlr	$⊢ ((φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \land z \in ⋃_{x \in A} (\{x\} \times B)) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
136	25 117 135 26	fsumless	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{z \in ran f} ⦋ 2^{nd} (z) / k ⦌ C \leq \sum_{z \in ⋃_{x \in A} (\{x\} \times B)} ⦋ 2^{nd} (z) / k ⦌ C$
137	98 136	eqbrtrrd	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{k \in ⋃_{x \in A} B} C \leq \sum_{z \in ⋃_{x \in A} (\{x\} \times B)} ⦋ 2^{nd} (z) / k ⦌ C$
138	14 15 16	cbvsum	$⊢ \sum_{k \in B} C = \sum_{y \in B} ⦋ y / k ⦌ C$
139	138	a1i	$⊢ φ \to \sum_{k \in B} C = \sum_{y \in B} ⦋ y / k ⦌ C$
140	139	sumeq2sdv	$⊢ φ \to \sum_{x \in A} \sum_{k \in B} C = \sum_{x \in A} \sum_{y \in B} ⦋ y / k ⦌ C$
141		vex	$⊢ x \in V$
142		vex	$⊢ y \in V$
143	141 142	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
144	143	eqcomd	$⊢ z = ⟨x, y⟩ \to y = 2^{nd} (z)$
145	144	csbeq1d	$⊢ z = ⟨x, y⟩ \to ⦋ y / k ⦌ C = ⦋ 2^{nd} (z) / k ⦌ C$
146	145	eqcomd	$⊢ z = ⟨x, y⟩ \to ⦋ 2^{nd} (z) / k ⦌ C = ⦋ y / k ⦌ C$
147		nfv	$⊢ Ⅎ k ((φ \land x \in A) \land y \in B)$
148	16	nfel1	$⊢ Ⅎ k ⦋ y / k ⦌ C \in ℂ$
149	147 148	nfim	$⊢ Ⅎ k (((φ \land x \in A) \land y \in B) \to ⦋ y / k ⦌ C \in ℂ)$
150		eleq1w	$⊢ k = y \to (k \in B \leftrightarrow y \in B)$
151	150	anbi2d	$⊢ k = y \to (((φ \land x \in A) \land k \in B) \leftrightarrow ((φ \land x \in A) \land y \in B))$
152	151 83	imbi12d	$⊢ k = y \to ((((φ \land x \in A) \land k \in B) \to C \in ℂ) \leftrightarrow (((φ \land x \in A) \land y \in B) \to ⦋ y / k ⦌ C \in ℂ))$
153	3	recnd	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℂ$
154	149 152 153	chvarfv	$⊢ ((φ \land x \in A) \land y \in B) \to ⦋ y / k ⦌ C \in ℂ$
155	154	anasss	$⊢ (φ \land (x \in A \land y \in B)) \to ⦋ y / k ⦌ C \in ℂ$
156	146 1 2 155	fsum2d	$⊢ φ \to \sum_{x \in A} \sum_{y \in B} ⦋ y / k ⦌ C = \sum_{z \in ⋃_{x \in A} (\{x\} \times B)} ⦋ 2^{nd} (z) / k ⦌ C$
157	140 156	eqtrd	$⊢ φ \to \sum_{x \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{x \in A} (\{x\} \times B)} ⦋ 2^{nd} (z) / k ⦌ C$
158	157	adantr	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{x \in A} \sum_{k \in B} C = \sum_{z \in ⋃_{x \in A} (\{x\} \times B)} ⦋ 2^{nd} (z) / k ⦌ C$
159	137 158	breqtrrd	$⊢ (φ \land ((f : ⋃_{x \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{x \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{x \in A} (\{x\} \times B))) \to \sum_{k \in ⋃_{x \in A} B} C \leq \sum_{x \in A} \sum_{k \in B} C$
160	13 159	exlimddv	$⊢ φ \to \sum_{k \in ⋃_{x \in A} B} C \leq \sum_{x \in A} \sum_{k \in B} C$

Metamath Proof Explorer

Theorem fsumiunle

Proof