esumiun

Description: Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019)

	Ref	Expression
Hypotheses	esumiun.0	$⊢ φ \to A \in V$
	esumiun.1	$⊢ (φ \land j \in A) \to B \in W$
	esumiun.2	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
Assertion	esumiun	$⊢ φ \to \underset{k \in ⋃_{j \in A} B}{\sum^{}} C \leq \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{*}} C$

Proof

Step	Hyp	Ref	Expression
1		esumiun.0	$⊢ φ \to A \in V$
2		esumiun.1	$⊢ (φ \land j \in A) \to B \in W$
3		esumiun.2	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
4	1 2	aciunf1	$⊢ φ \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l)$
5		f1f1orn	$⊢ f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \to f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f$
6	5	anim1i	$⊢ (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \to (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l)$
7		f1f	$⊢ f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \to f : ⋃_{j \in A} B ⟶ ⋃_{j \in A} (\{j\} \times B)$
8	7	frnd	$⊢ f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \to ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
9	8	adantr	$⊢ (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \to ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
10	6 9	jca	$⊢ (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \to ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))$
11	10	eximi	$⊢ \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \to \exists f ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))$
12	4 11	syl	$⊢ φ \to \exists f ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))$
13		nfv	$⊢ Ⅎ z (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B)))$
14		nfcv	$⊢ \underline{Ⅎ} z C$
15		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ C$
16		nfcv	$⊢ \underline{Ⅎ} z ⋃_{j \in A} B$
17		nfcv	$⊢ \underline{Ⅎ} z ran f$
18		nfcv	$⊢ \underline{Ⅎ} z f^{-1}$
19		csbeq1a	$⊢ k = 2^{nd} (z) \to C = ⦋ 2^{nd} (z) / k ⦌ C$
20	2	ralrimiva	$⊢ φ \to \forall j \in A B \in W$
21		iunexg	$⊢ (A \in V \land \forall j \in A B \in W) \to ⋃_{j \in A} B \in V$
22	1 20 21	syl2anc	$⊢ φ \to ⋃_{j \in A} B \in V$
23	22	adantr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to ⋃_{j \in A} B \in V$
24		simprl	$⊢ (φ \land (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f$
25		f1ocnv	$⊢ f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{j \in A} B$
26	24 25	syl	$⊢ (φ \land (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{j \in A} B$
27	26	adantrlr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to f^{-1} : ran f \underset{1-1 onto}{⟶} ⋃_{j \in A} B$
28		nfv	$⊢ Ⅎ j φ$
29		nfcv	$⊢ \underline{Ⅎ} j f$
30		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} B$
31	29	nfrn	$⊢ \underline{Ⅎ} j ran f$
32	29 30 31	nff1o	$⊢ Ⅎ j f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f$
33		nfv	$⊢ Ⅎ j 2^{nd} (f (l)) = l$
34	30 33	nfralw	$⊢ Ⅎ j \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l$
35	32 34	nfan	$⊢ Ⅎ j (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l)$
36		nfcv	$⊢ \underline{Ⅎ} j ran f$
37		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times B)$
38	36 37	nfss	$⊢ Ⅎ j ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
39	35 38	nfan	$⊢ Ⅎ j ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))$
40	28 39	nfan	$⊢ Ⅎ j (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B)))$
41		nfv	$⊢ Ⅎ j z \in ran f$
42	40 41	nfan	$⊢ Ⅎ j ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f)$
43		simpr	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to f (k) = z$
44	43	fveq2d	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to 2^{nd} (f (k)) = 2^{nd} (z)$
45		simplr	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to k \in ⋃_{j \in A} B$
46		simp-4r	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))$
47	46	simpld	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l)$
48	47	simprd	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l$
49	48	ad2antrr	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l$
50		2fveq3	$⊢ l = k \to 2^{nd} (f (l)) = 2^{nd} (f (k))$
51		id	$⊢ l = k \to l = k$
52	50 51	eqeq12d	$⊢ l = k \to (2^{nd} (f (l)) = l \leftrightarrow 2^{nd} (f (k)) = k)$
53	52	rspcva	$⊢ (k \in ⋃_{j \in A} B \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \to 2^{nd} (f (k)) = k$
54	45 49 53	syl2anc	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to 2^{nd} (f (k)) = k$
55	44 54	eqtr3d	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to 2^{nd} (z) = k$
56	47	simpld	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f$
57	56	ad2antrr	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f$
58		f1ocnvfv1	$⊢ (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land k \in ⋃_{j \in A} B) \to f^{-1} (f (k)) = k$
59	57 45 58	syl2anc	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to f^{-1} (f (k)) = k$
60	43	fveq2d	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to f^{-1} (f (k)) = f^{-1} (z)$
61	55 59 60	3eqtr2rd	$⊢ ((((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \land k \in ⋃_{j \in A} B) \land f (k) = z) \to f^{-1} (z) = 2^{nd} (z)$
62		f1ofn	$⊢ f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \to f Fn ⋃_{j \in A} B$
63	56 62	syl	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to f Fn ⋃_{j \in A} B$
64		simpllr	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to z \in ran f$
65		fvelrnb	$⊢ f Fn ⋃_{j \in A} B \to (z \in ran f \leftrightarrow \exists k \in ⋃_{j \in A} B f (k) = z)$
66	65	biimpa	$⊢ (f Fn ⋃_{j \in A} B \land z \in ran f) \to \exists k \in ⋃_{j \in A} B f (k) = z$
67	63 64 66	syl2anc	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to \exists k \in ⋃_{j \in A} B f (k) = z$
68	61 67	r19.29a	$⊢ ((((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \land j \in A) \land z \in (\{j\} \times B)) \to f^{-1} (z) = 2^{nd} (z)$
69		simprr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
70	69	sselda	$⊢ ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \to z \in ⋃_{j \in A} (\{j\} \times B)$
71		eliun	$⊢ z \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A z \in (\{j\} \times B)$
72	70 71	sylib	$⊢ ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \to \exists j \in A z \in (\{j\} \times B)$
73	42 68 72	r19.29af	$⊢ ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ran f) \to f^{-1} (z) = 2^{nd} (z)$
74		nfcv	$⊢ \underline{Ⅎ} j k$
75	74 30	nfel	$⊢ Ⅎ j k \in ⋃_{j \in A} B$
76	28 75	nfan	$⊢ Ⅎ j (φ \land k \in ⋃_{j \in A} B)$
77	3	adantllr	$⊢ (((φ \land k \in ⋃_{j \in A} B) \land j \in A) \land k \in B) \to C \in [0, +∞]$
78		eliun	$⊢ k \in ⋃_{j \in A} B \leftrightarrow \exists j \in A k \in B$
79	78	biimpi	$⊢ k \in ⋃_{j \in A} B \to \exists j \in A k \in B$
80	79	adantl	$⊢ (φ \land k \in ⋃_{j \in A} B) \to \exists j \in A k \in B$
81	76 77 80	r19.29af	$⊢ (φ \land k \in ⋃_{j \in A} B) \to C \in [0, +∞]$
82	81	adantlr	$⊢ ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land k \in ⋃_{j \in A} B) \to C \in [0, +∞]$
83	13 14 15 16 17 18 19 23 27 73 82	esumf1o	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{k \in ⋃_{j \in A} B}{\sum^{}} C = \underset{z \in ran f}{\sum^{}} ⦋ 2^{nd} (z) / k ⦌ C$
84	83	eqcomd	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{z \in ran f}{\sum^{}} ⦋ 2^{nd} (z) / k ⦌ C = \underset{k \in ⋃_{j \in A} B}{\sum^{}} C$
85		vsnex	$⊢ \{j\} \in V$
86	85	a1i	$⊢ (φ \land j \in A) \to \{j\} \in V$
87	86 2	xpexd	$⊢ (φ \land j \in A) \to \{j\} \times B \in V$
88	87	ralrimiva	$⊢ φ \to \forall j \in A \{j\} \times B \in V$
89		iunexg	$⊢ (A \in V \land \forall j \in A \{j\} \times B \in V) \to ⋃_{j \in A} (\{j\} \times B) \in V$
90	1 88 89	syl2anc	$⊢ φ \to ⋃_{j \in A} (\{j\} \times B) \in V$
91	90	adantr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to ⋃_{j \in A} (\{j\} \times B) \in V$
92		nfcv	$⊢ \underline{Ⅎ} j z$
93	92 37	nfel	$⊢ Ⅎ j z \in ⋃_{j \in A} (\{j\} \times B)$
94	28 93	nfan	$⊢ Ⅎ j (φ \land z \in ⋃_{j \in A} (\{j\} \times B))$
95		nfcv	$⊢ \underline{Ⅎ} j 2^{nd} (z)$
96		nfcv	$⊢ \underline{Ⅎ} j C$
97	95 96	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ 2^{nd} (z) / k ⦌ C$
98		nfcv	$⊢ \underline{Ⅎ} j [0, +∞]$
99	97 98	nfel	$⊢ Ⅎ j ⦋ 2^{nd} (z) / k ⦌ C \in [0, +∞]$
100		simprr	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land (1^{st} (z) = j \land 2^{nd} (z) \in B)) \to 2^{nd} (z) \in B$
101		simplll	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land (1^{st} (z) = j \land 2^{nd} (z) \in B)) \to φ$
102		simplr	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land (1^{st} (z) = j \land 2^{nd} (z) \in B)) \to j \in A$
103	3	ralrimiva	$⊢ (φ \land j \in A) \to \forall k \in B C \in [0, +∞]$
104	101 102 103	syl2anc	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land (1^{st} (z) = j \land 2^{nd} (z) \in B)) \to \forall k \in B C \in [0, +∞]$
105		rspcsbela	$⊢ (2^{nd} (z) \in B \land \forall k \in B C \in [0, +∞]) \to ⦋ 2^{nd} (z) / k ⦌ C \in [0, +∞]$
106	100 104 105	syl2anc	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land (1^{st} (z) = j \land 2^{nd} (z) \in B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in [0, +∞]$
107		xp1st	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) \in \{j\}$
108		elsni	$⊢ 1^{st} (z) \in \{j\} \to 1^{st} (z) = j$
109	107 108	syl	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) = j$
110		xp2nd	$⊢ z \in (\{j\} \times B) \to 2^{nd} (z) \in B$
111	109 110	jca	$⊢ z \in (\{j\} \times B) \to (1^{st} (z) = j \land 2^{nd} (z) \in B)$
112	111	reximi	$⊢ \exists j \in A z \in (\{j\} \times B) \to \exists j \in A (1^{st} (z) = j \land 2^{nd} (z) \in B)$
113	71 112	sylbi	$⊢ z \in ⋃_{j \in A} (\{j\} \times B) \to \exists j \in A (1^{st} (z) = j \land 2^{nd} (z) \in B)$
114	113	adantl	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to \exists j \in A (1^{st} (z) = j \land 2^{nd} (z) \in B)$
115	94 99 106 114	r19.29af2	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in [0, +∞]$
116	115	adantlr	$⊢ ((φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \land z \in ⋃_{j \in A} (\{j\} \times B)) \to ⦋ 2^{nd} (z) / k ⦌ C \in [0, +∞]$
117		simprr	$⊢ (φ \land (f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
118	117	adantrlr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to ran f \subseteq ⋃_{j \in A} (\{j\} \times B)$
119	13 91 116 118	esummono	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{z \in ran f}{\sum^{}} ⦋ 2^{nd} (z) / k ⦌ C \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} ⦋ 2^{nd} (z) / k ⦌ C$
120	84 119	eqbrtrrd	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{k \in ⋃_{j \in A} B}{\sum^{}} C \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} ⦋ 2^{nd} (z) / k ⦌ C$
121		vex	$⊢ j \in V$
122		vex	$⊢ k \in V$
123	121 122	op2ndd	$⊢ z = ⟨j, k⟩ \to 2^{nd} (z) = k$
124	123	eqcomd	$⊢ z = ⟨j, k⟩ \to k = 2^{nd} (z)$
125	124 19	syl	$⊢ z = ⟨j, k⟩ \to C = ⦋ 2^{nd} (z) / k ⦌ C$
126	125	eqcomd	$⊢ z = ⟨j, k⟩ \to ⦋ 2^{nd} (z) / k ⦌ C = C$
127	3	anasss	$⊢ (φ \land (j \in A \land k \in B)) \to C \in [0, +∞]$
128	15 126 1 2 127	esum2d	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} ⦋ 2^{nd} (z) / k ⦌ C$
129	128	adantr	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} ⦋ 2^{nd} (z) / k ⦌ C$
130	120 129	breqtrrd	$⊢ (φ \land ((f : ⋃_{j \in A} B \underset{1-1 onto}{⟶} ran f \land \forall l \in ⋃_{j \in A} B 2^{nd} (f (l)) = l) \land ran f \subseteq ⋃_{j \in A} (\{j\} \times B))) \to \underset{k \in ⋃_{j \in A} B}{\sum^{}} C \leq \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{*}} C$
131	12 130	exlimddv	$⊢ φ \to \underset{k \in ⋃_{j \in A} B}{\sum^{}} C \leq \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{*}} C$

Metamath Proof Explorer

Theorem esumiun

Proof