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	bilani	$⊢ (φ \land k \in ⋃_{x \in A} B) \to \exists x \in A k \in B$
92	87 89 91	r19.29af	$⊢ (φ \land k \in ⋃_{x \in A} B) \to C \in ℂ$
93	80 84 92	chvarfv	$⊢ (φ \land y \in ⋃_{x \in A} B) \to ⦋ y / k ⦌ C \in ℂ$
94	93	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 ℂ$
95	18 27 31 76 94	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$
96	17 95	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$
97	96	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$
98		nfcv	$⊢ \underline{Ⅎ} x z$
99	98 41	nfel	$⊢ Ⅎ x z \in ⋃_{x \in A} (\{x\} \times B)$
100	32 99	nfan	$⊢ Ⅎ x (φ \land z \in ⋃_{x \in A} (\{x\} \times B))$
101		xp2nd	$⊢ z \in (\{x\} \times B) \to 2^{nd} (z) \in B$
102	101	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$
103	3	ralrimiva	$⊢ (φ \land x \in A) \to \forall k \in B C \in ℝ$
104	103	adantlr	$⊢ ((φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \land x \in A) \to \forall k \in B C \in ℝ$
105	104	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 ℝ$
106		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ C$
107	106	nfel1	$⊢ Ⅎ k ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
108		csbeq1a	$⊢ k = 2^{nd} (z) \to C = ⦋ 2^{nd} (z) / k ⦌ C$
109	108	eleq1d	$⊢ k = 2^{nd} (z) \to (C \in ℝ \leftrightarrow ⦋ 2^{nd} (z) / k ⦌ C \in ℝ)$
110	107 109	rspc	$⊢ 2^{nd} (z) \in B \to (\forall k \in B C \in ℝ \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ)$
111	110	imp	$⊢ (2^{nd} (z) \in B \land \forall k \in B C \in ℝ) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
112	102 105 111	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 ℝ$
113	74	bilani	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to \exists x \in A z \in (\{x\} \times B)$
114	100 112 113	r19.29af	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in ℝ$
115	114	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 ℝ$
116		xp1st	$⊢ z \in (\{x\} \times B) \to 1^{st} (z) \in \{x\}$
117		elsni	$⊢ 1^{st} (z) \in \{x\} \to 1^{st} (z) = x$
118	116 117	syl	$⊢ z \in (\{x\} \times B) \to 1^{st} (z) = x$
119	118 101	jca	$⊢ z \in (\{x\} \times B) \to (1^{st} (z) = x \land 2^{nd} (z) \in B)$
120		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 φ$
121		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$
122	4	ralrimiva	$⊢ (φ \land x \in A) \to \forall k \in B 0 \leq C$
123	120 121 122	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$
124	119 123	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$
125		nfcv	$⊢ \underline{Ⅎ} k 0$
126		nfcv	$⊢ \underline{Ⅎ} k \leq$
127	125 126 106	nfbr	$⊢ Ⅎ k 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
128	108	breq2d	$⊢ k = 2^{nd} (z) \to (0 \leq C \leftrightarrow 0 \leq ⦋ 2^{nd} (z) / k ⦌ C)$
129	127 128	rspc	$⊢ 2^{nd} (z) \in B \to (\forall k \in B 0 \leq C \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C)$
130	129	imp	$⊢ (2^{nd} (z) \in B \land \forall k \in B 0 \leq C) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
131	102 124 130	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$
132	100 131 113	r19.29af	$⊢ (φ \land z \in ⋃_{x \in A} (\{x\} \times B)) \to 0 \leq ⦋ 2^{nd} (z) / k ⦌ C$
133	132	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$
134	25 115 133 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$
135	97 134	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$
136	14 15 16	cbvsum	$⊢ \sum_{k \in B} C = \sum_{y \in B} ⦋ y / k ⦌ C$
137	136	a1i	$⊢ φ \to \sum_{k \in B} C = \sum_{y \in B} ⦋ y / k ⦌ C$
138	137	sumeq2sdv	$⊢ φ \to \sum_{x \in A} \sum_{k \in B} C = \sum_{x \in A} \sum_{y \in B} ⦋ y / k ⦌ C$
139		vex	$⊢ x \in V$
140		vex	$⊢ y \in V$
141	139 140	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
142	141	eqcomd	$⊢ z = ⟨x, y⟩ \to y = 2^{nd} (z)$
143	142	csbeq1d	$⊢ z = ⟨x, y⟩ \to ⦋ y / k ⦌ C = ⦋ 2^{nd} (z) / k ⦌ C$
144	143	eqcomd	$⊢ z = ⟨x, y⟩ \to ⦋ 2^{nd} (z) / k ⦌ C = ⦋ y / k ⦌ C$
145		nfv	$⊢ Ⅎ k ((φ \land x \in A) \land y \in B)$
146	16	nfel1	$⊢ Ⅎ k ⦋ y / k ⦌ C \in ℂ$
147	145 146	nfim	$⊢ Ⅎ k (((φ \land x \in A) \land y \in B) \to ⦋ y / k ⦌ C \in ℂ)$
148		eleq1w	$⊢ k = y \to (k \in B \leftrightarrow y \in B)$
149	148	anbi2d	$⊢ k = y \to (((φ \land x \in A) \land k \in B) \leftrightarrow ((φ \land x \in A) \land y \in B))$
150	149 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 ℂ))$
151	3	recnd	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℂ$
152	147 150 151	chvarfv	$⊢ ((φ \land x \in A) \land y \in B) \to ⦋ y / k ⦌ C \in ℂ$
153	152	anasss	$⊢ (φ \land (x \in A \land y \in B)) \to ⦋ y / k ⦌ C \in ℂ$
154	144 1 2 153	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$
155	138 154	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$
156	155	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$
157	135 156	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$
158	13 157	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