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