itg2splitlem

	Ref	Expression
Hypotheses	itg2split.a	$⊢ φ \to A \in dom vol$
	itg2split.b	$⊢ φ \to B \in dom vol$
	itg2split.i	$⊢ φ \to {vol}^{*} (A \cap B) = 0$
	itg2split.u	$⊢ φ \to U = A \cup B$
	itg2split.c	$⊢ (φ \land x \in U) \to C \in [0, +∞]$
	itg2split.f	$⊢ F = (x \in ℝ ⟼ if (x \in A, C, 0))$
	itg2split.g	$⊢ G = (x \in ℝ ⟼ if (x \in B, C, 0))$
	itg2split.h	$⊢ H = (x \in ℝ ⟼ if (x \in U, C, 0))$
	itg2split.sf	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2split.sg	$⊢ φ \to \int^{2} (G) \in ℝ$
Assertion	itg2splitlem	$⊢ φ \to \int^{2} (H) \leq \int^{2} (F) + \int^{2} (G)$

Proof

Step	Hyp	Ref	Expression
1		itg2split.a	$⊢ φ \to A \in dom vol$
2		itg2split.b	$⊢ φ \to B \in dom vol$
3		itg2split.i	$⊢ φ \to {vol}^{*} (A \cap B) = 0$
4		itg2split.u	$⊢ φ \to U = A \cup B$
5		itg2split.c	$⊢ (φ \land x \in U) \to C \in [0, +∞]$
6		itg2split.f	$⊢ F = (x \in ℝ ⟼ if (x \in A, C, 0))$
7		itg2split.g	$⊢ G = (x \in ℝ ⟼ if (x \in B, C, 0))$
8		itg2split.h	$⊢ H = (x \in ℝ ⟼ if (x \in U, C, 0))$
9		itg2split.sf	$⊢ φ \to \int^{2} (F) \in ℝ$
10		itg2split.sg	$⊢ φ \to \int^{2} (G) \in ℝ$
11		simprl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to f \in dom \int^{1}$
12		itg1cl	$⊢ f \in dom \int^{1} \to \int^{1} (f) \in ℝ$
13	11 12	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} (f) \in ℝ$
14	1	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to A \in dom vol$
15		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, f (x), 0)) = (x \in ℝ ⟼ if (x \in A, f (x), 0))$
16	15	i1fres	$⊢ (f \in dom \int^{1} \land A \in dom vol) \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) \in dom \int^{1}$
17	11 14 16	syl2anc	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) \in dom \int^{1}$
18		itg1cl	$⊢ (x \in ℝ ⟼ if (x \in A, f (x), 0)) \in dom \int^{1} \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) \in ℝ$
19	17 18	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) \in ℝ$
20	2	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to B \in dom vol$
21		eqid	$⊢ (x \in ℝ ⟼ if (x \in B, f (x), 0)) = (x \in ℝ ⟼ if (x \in B, f (x), 0))$
22	21	i1fres	$⊢ (f \in dom \int^{1} \land B \in dom vol) \to (x \in ℝ ⟼ if (x \in B, f (x), 0)) \in dom \int^{1}$
23	11 20 22	syl2anc	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in B, f (x), 0)) \in dom \int^{1}$
24		itg1cl	$⊢ (x \in ℝ ⟼ if (x \in B, f (x), 0)) \in dom \int^{1} \to \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \in ℝ$
25	23 24	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \in ℝ$
26	19 25	readdcld	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) + \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \in ℝ$
27	9 10	readdcld	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \in ℝ$
28	27	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{2} (F) + \int^{2} (G) \in ℝ$
29		inss1	$⊢ A \cap B \subseteq A$
30		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
31	1 30	syl	$⊢ φ \to A \subseteq ℝ$
32	29 31	sstrid	$⊢ φ \to A \cap B \subseteq ℝ$
33	32	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to A \cap B \subseteq ℝ$
34	3	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to {vol}^{*} (A \cap B) = 0$
35		reex	$⊢ ℝ \in V$
36	35	a1i	$⊢ φ \to ℝ \in V$
37		fvex	$⊢ f (x) \in V$
38		c0ex	$⊢ 0 \in V$
39	37 38	ifex	$⊢ if (x \in A, f (x), 0) \in V$
40	39	a1i	$⊢ (φ \land x \in ℝ) \to if (x \in A, f (x), 0) \in V$
41	37 38	ifex	$⊢ if (x \in B, f (x), 0) \in V$
42	41	a1i	$⊢ (φ \land x \in ℝ) \to if (x \in B, f (x), 0) \in V$
43		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) = (x \in ℝ ⟼ if (x \in A, f (x), 0))$
44		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in B, f (x), 0)) = (x \in ℝ ⟼ if (x \in B, f (x), 0))$
45	36 40 42 43 44	offval2	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) +_{f} (x \in ℝ ⟼ if (x \in B, f (x), 0)) = (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0))$
46	45	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) +_{f} (x \in ℝ ⟼ if (x \in B, f (x), 0)) = (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0))$
47	17 23	i1fadd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) +_{f} (x \in ℝ ⟼ if (x \in B, f (x), 0)) \in dom \int^{1}$
48	46 47	eqeltrrd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)) \in dom \int^{1}$
49		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
50	11 49	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to f : ℝ ⟶ ℝ$
51		eldifi	$⊢ y \in (ℝ ∖ (A \cap B)) \to y \in ℝ$
52		ffvelrn	$⊢ (f : ℝ ⟶ ℝ \land y \in ℝ) \to f (y) \in ℝ$
53	50 51 52	syl2an	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \in ℝ$
54	53	leidd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \leq f (y)$
55	54	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to f (y) \leq f (y)$
56		iftrue	$⊢ y \in A \to if (y \in A, f (y), 0) = f (y)$
57	56	adantl	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to if (y \in A, f (y), 0) = f (y)$
58		eldifn	$⊢ y \in (ℝ ∖ (A \cap B)) \to \neg y \in (A \cap B)$
59	58	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to \neg y \in (A \cap B)$
60		elin	$⊢ y \in (A \cap B) \leftrightarrow (y \in A \land y \in B)$
61	59 60	sylnib	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to \neg (y \in A \land y \in B)$
62		imnan	$⊢ (y \in A \to \neg y \in B) \leftrightarrow \neg (y \in A \land y \in B)$
63	61 62	sylibr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (y \in A \to \neg y \in B)$
64	63	imp	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to \neg y \in B$
65		iffalse	$⊢ \neg y \in B \to if (y \in B, f (y), 0) = 0$
66	64 65	syl	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to if (y \in B, f (y), 0) = 0$
67	57 66	oveq12d	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to if (y \in A, f (y), 0) + if (y \in B, f (y), 0) = f (y) + 0$
68	53	recnd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \in ℂ$
69	68	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to f (y) \in ℂ$
70	69	addid1d	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to f (y) + 0 = f (y)$
71	67 70	eqtrd	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to if (y \in A, f (y), 0) + if (y \in B, f (y), 0) = f (y)$
72	55 71	breqtrrd	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land y \in A) \to f (y) \leq if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
73	54	ad2antrr	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land y \in B) \to f (y) \leq f (y)$
74		iftrue	$⊢ y \in B \to if (y \in B, f (y), 0) = f (y)$
75	74	adantl	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land y \in B) \to if (y \in B, f (y), 0) = f (y)$
76	73 75	breqtrrd	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land y \in B) \to f (y) \leq if (y \in B, f (y), 0)$
77	4	ad2antrr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to U = A \cup B$
78	77	eleq2d	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (y \in U \leftrightarrow y \in (A \cup B))$
79		elun	$⊢ y \in (A \cup B) \leftrightarrow (y \in A \lor y \in B)$
80	78 79	bitrdi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (y \in U \leftrightarrow (y \in A \lor y \in B))$
81	80	notbid	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (\neg y \in U \leftrightarrow \neg (y \in A \lor y \in B))$
82		ioran	$⊢ \neg (y \in A \lor y \in B) \leftrightarrow (\neg y \in A \land \neg y \in B)$
83	81 82	bitrdi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (\neg y \in U \leftrightarrow (\neg y \in A \land \neg y \in B))$
84	83	biimpar	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land (\neg y \in A \land \neg y \in B)) \to \neg y \in U$
85		simprr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to f \leq_{f} H$
86	50	ffnd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to f Fn ℝ$
87	5	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in U) \to C \in [0, +∞]$
88		0e0iccpnf	$⊢ 0 \in [0, +∞]$
89	88	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in U) \to 0 \in [0, +∞]$
90	87 89	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in U, C, 0) \in [0, +∞]$
91	90 8	fmptd	$⊢ φ \to H : ℝ ⟶ [0, +∞]$
92	91	ffnd	$⊢ φ \to H Fn ℝ$
93	92	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to H Fn ℝ$
94	35	a1i	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to ℝ \in V$
95		inidm	$⊢ ℝ \cap ℝ = ℝ$
96		eqidd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in ℝ) \to f (y) = f (y)$
97		eqidd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in ℝ) \to H (y) = H (y)$
98	86 93 94 94 95 96 97	ofrfval	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (f \leq_{f} H \leftrightarrow \forall y \in ℝ f (y) \leq H (y))$
99	85 98	mpbid	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \forall y \in ℝ f (y) \leq H (y)$
100	99	r19.21bi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in ℝ) \to f (y) \leq H (y)$
101	51 100	sylan2	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \leq H (y)$
102	101	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in U) \to f (y) \leq H (y)$
103	51	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to y \in ℝ$
104		eldif	$⊢ y \in (ℝ ∖ U) \leftrightarrow (y \in ℝ \land \neg y \in U)$
105		nfcv	$⊢ \underline{Ⅎ} x y$
106		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in U, C, 0))$
107	8 106	nfcxfr	$⊢ \underline{Ⅎ} x H$
108	107 105	nffv	$⊢ \underline{Ⅎ} x H (y)$
109	108	nfeq1	$⊢ Ⅎ x H (y) = 0$
110		fveqeq2	$⊢ x = y \to (H (x) = 0 \leftrightarrow H (y) = 0)$
111		eldif	$⊢ x \in (ℝ ∖ U) \leftrightarrow (x \in ℝ \land \neg x \in U)$
112	8	fvmpt2i	$⊢ x \in ℝ \to H (x) = I (if (x \in U, C, 0))$
113		iffalse	$⊢ \neg x \in U \to if (x \in U, C, 0) = 0$
114	113	fveq2d	$⊢ \neg x \in U \to I (if (x \in U, C, 0)) = I (0)$
115		0cn	$⊢ 0 \in ℂ$
116		fvi	$⊢ 0 \in ℂ \to I (0) = 0$
117	115 116	ax-mp	$⊢ I (0) = 0$
118	114 117	eqtrdi	$⊢ \neg x \in U \to I (if (x \in U, C, 0)) = 0$
119	112 118	sylan9eq	$⊢ (x \in ℝ \land \neg x \in U) \to H (x) = 0$
120	111 119	sylbi	$⊢ x \in (ℝ ∖ U) \to H (x) = 0$
121	105 109 110 120	vtoclgaf	$⊢ y \in (ℝ ∖ U) \to H (y) = 0$
122	104 121	sylbir	$⊢ (y \in ℝ \land \neg y \in U) \to H (y) = 0$
123	103 122	sylan	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in U) \to H (y) = 0$
124	102 123	breqtrd	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in U) \to f (y) \leq 0$
125	84 124	syldan	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land (\neg y \in A \land \neg y \in B)) \to f (y) \leq 0$
126	125	anassrs	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land \neg y \in B) \to f (y) \leq 0$
127	65	adantl	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land \neg y \in B) \to if (y \in B, f (y), 0) = 0$
128	126 127	breqtrrd	$⊢ ((((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \land \neg y \in B) \to f (y) \leq if (y \in B, f (y), 0)$
129	76 128	pm2.61dan	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to f (y) \leq if (y \in B, f (y), 0)$
130		iffalse	$⊢ \neg y \in A \to if (y \in A, f (y), 0) = 0$
131	130	adantl	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to if (y \in A, f (y), 0) = 0$
132	131	oveq1d	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to if (y \in A, f (y), 0) + if (y \in B, f (y), 0) = 0 + if (y \in B, f (y), 0)$
133		0re	$⊢ 0 \in ℝ$
134		ifcl	$⊢ (f (y) \in ℝ \land 0 \in ℝ) \to if (y \in B, f (y), 0) \in ℝ$
135	53 133 134	sylancl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to if (y \in B, f (y), 0) \in ℝ$
136	135	recnd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to if (y \in B, f (y), 0) \in ℂ$
137	136	adantr	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to if (y \in B, f (y), 0) \in ℂ$
138	137	addid2d	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to 0 + if (y \in B, f (y), 0) = if (y \in B, f (y), 0)$
139	132 138	eqtrd	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to if (y \in A, f (y), 0) + if (y \in B, f (y), 0) = if (y \in B, f (y), 0)$
140	129 139	breqtrrd	$⊢ (((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \land \neg y \in A) \to f (y) \leq if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
141	72 140	pm2.61dan	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \leq if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
142		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
143		fveq2	$⊢ x = y \to f (x) = f (y)$
144	142 143	ifbieq1d	$⊢ x = y \to if (x \in A, f (x), 0) = if (y \in A, f (y), 0)$
145		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
146	145 143	ifbieq1d	$⊢ x = y \to if (x \in B, f (x), 0) = if (y \in B, f (y), 0)$
147	144 146	oveq12d	$⊢ x = y \to if (x \in A, f (x), 0) + if (x \in B, f (x), 0) = if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
148		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)) = (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0))$
149		ovex	$⊢ if (y \in A, f (y), 0) + if (y \in B, f (y), 0) \in V$
150	147 148 149	fvmpt	$⊢ y \in ℝ \to (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)) (y) = if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
151	103 150	syl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)) (y) = if (y \in A, f (y), 0) + if (y \in B, f (y), 0)$
152	141 151	breqtrrd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land y \in (ℝ ∖ (A \cap B))) \to f (y) \leq (x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)) (y)$
153	11 33 34 48 152	itg1lea	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} (f) \leq \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)))$
154	46	fveq2d	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0)) +_{f} (x \in ℝ ⟼ if (x \in B, f (x), 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0)))$
155	17 23	itg1add	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0)) +_{f} (x \in ℝ ⟼ if (x \in B, f (x), 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) + \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0)))$
156	154 155	eqtr3d	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0) + if (x \in B, f (x), 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) + \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0)))$
157	153 156	breqtrd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} (f) \leq \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) + \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0)))$
158	9	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{2} (F) \in ℝ$
159	10	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{2} (G) \in ℝ$
160		ssun1	$⊢ A \subseteq A \cup B$
161	160 4	sseqtrrid	$⊢ φ \to A \subseteq U$
162	161	sselda	$⊢ (φ \land x \in A) \to x \in U$
163	162	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in A) \to x \in U$
164	163 87	syldan	$⊢ ((φ \land x \in ℝ) \land x \in A) \to C \in [0, +∞]$
165	88	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to 0 \in [0, +∞]$
166	164 165	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in A, C, 0) \in [0, +∞]$
167	166 6	fmptd	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
168	167	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to F : ℝ ⟶ [0, +∞]$
169		nfv	$⊢ Ⅎ x φ$
170		nfv	$⊢ Ⅎ x f \in dom \int^{1}$
171		nfcv	$⊢ \underline{Ⅎ} x f$
172		nfcv	$⊢ \underline{Ⅎ} x \circ_{r} \leq$
173	171 172 107	nfbr	$⊢ Ⅎ x f \leq_{f} H$
174	170 173	nfan	$⊢ Ⅎ x (f \in dom \int^{1} \land f \leq_{f} H)$
175	169 174	nfan	$⊢ Ⅎ x (φ \land (f \in dom \int^{1} \land f \leq_{f} H))$
176	14 30	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to A \subseteq ℝ$
177	176	sselda	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to x \in ℝ$
178	35	a1i	$⊢ (φ \land f \in dom \int^{1}) \to ℝ \in V$
179	37	a1i	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to f (x) \in V$
180	90	adantlr	$⊢ ((φ \land f \in dom \int^{1}) \land x \in ℝ) \to if (x \in U, C, 0) \in [0, +∞]$
181	49	adantl	$⊢ (φ \land f \in dom \int^{1}) \to f : ℝ ⟶ ℝ$
182	181	feqmptd	$⊢ (φ \land f \in dom \int^{1}) \to f = (x \in ℝ ⟼ f (x))$
183	8	a1i	$⊢ (φ \land f \in dom \int^{1}) \to H = (x \in ℝ ⟼ if (x \in U, C, 0))$
184	178 179 180 182 183	ofrfval2	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} H \leftrightarrow \forall x \in ℝ f (x) \leq if (x \in U, C, 0))$
185	184	biimpd	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} H \to \forall x \in ℝ f (x) \leq if (x \in U, C, 0))$
186	185	impr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \forall x \in ℝ f (x) \leq if (x \in U, C, 0)$
187	186	r19.21bi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in ℝ) \to f (x) \leq if (x \in U, C, 0)$
188	177 187	syldan	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to f (x) \leq if (x \in U, C, 0)$
189	162	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to x \in U$
190	189	iftrued	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to if (x \in U, C, 0) = C$
191	188 190	breqtrd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to f (x) \leq C$
192		iftrue	$⊢ x \in A \to if (x \in A, f (x), 0) = f (x)$
193	192	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to if (x \in A, f (x), 0) = f (x)$
194		iftrue	$⊢ x \in A \to if (x \in A, C, 0) = C$
195	194	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to if (x \in A, C, 0) = C$
196	191 193 195	3brtr4d	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in A) \to if (x \in A, f (x), 0) \leq if (x \in A, C, 0)$
197		0le0	$⊢ 0 \leq 0$
198	197	a1i	$⊢ \neg x \in A \to 0 \leq 0$
199		iffalse	$⊢ \neg x \in A \to if (x \in A, f (x), 0) = 0$
200		iffalse	$⊢ \neg x \in A \to if (x \in A, C, 0) = 0$
201	198 199 200	3brtr4d	$⊢ \neg x \in A \to if (x \in A, f (x), 0) \leq if (x \in A, C, 0)$
202	201	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land \neg x \in A) \to if (x \in A, f (x), 0) \leq if (x \in A, C, 0)$
203	196 202	pm2.61dan	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to if (x \in A, f (x), 0) \leq if (x \in A, C, 0)$
204	203	a1d	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ \to if (x \in A, f (x), 0) \leq if (x \in A, C, 0))$
205	175 204	ralrimi	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \forall x \in ℝ if (x \in A, f (x), 0) \leq if (x \in A, C, 0)$
206	6	a1i	$⊢ φ \to F = (x \in ℝ ⟼ if (x \in A, C, 0))$
207	36 40 166 43 206	ofrfval2	$⊢ φ \to ((x \in ℝ ⟼ if (x \in A, f (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in A, f (x), 0) \leq if (x \in A, C, 0))$
208	207	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to ((x \in ℝ ⟼ if (x \in A, f (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in A, f (x), 0) \leq if (x \in A, C, 0))$
209	205 208	mpbird	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in A, f (x), 0)) \leq_{f} F$
210		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A, f (x), 0)) \in dom \int^{1} \land (x \in ℝ ⟼ if (x \in A, f (x), 0)) \leq_{f} F) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) \leq \int^{2} (F)$
211	168 17 209 210	syl3anc	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) \leq \int^{2} (F)$
212		ssun2	$⊢ B \subseteq A \cup B$
213	212 4	sseqtrrid	$⊢ φ \to B \subseteq U$
214	213	sselda	$⊢ (φ \land x \in B) \to x \in U$
215	214	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in B) \to x \in U$
216	215 87	syldan	$⊢ ((φ \land x \in ℝ) \land x \in B) \to C \in [0, +∞]$
217	88	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in B) \to 0 \in [0, +∞]$
218	216 217	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in B, C, 0) \in [0, +∞]$
219	218 7	fmptd	$⊢ φ \to G : ℝ ⟶ [0, +∞]$
220	219	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to G : ℝ ⟶ [0, +∞]$
221		mblss	$⊢ B \in dom vol \to B \subseteq ℝ$
222	20 221	syl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to B \subseteq ℝ$
223	222	sselda	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to x \in ℝ$
224	223 187	syldan	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to f (x) \leq if (x \in U, C, 0)$
225	214	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to x \in U$
226	225	iftrued	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to if (x \in U, C, 0) = C$
227	224 226	breqtrd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to f (x) \leq C$
228		iftrue	$⊢ x \in B \to if (x \in B, f (x), 0) = f (x)$
229	228	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to if (x \in B, f (x), 0) = f (x)$
230		iftrue	$⊢ x \in B \to if (x \in B, C, 0) = C$
231	230	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to if (x \in B, C, 0) = C$
232	227 229 231	3brtr4d	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land x \in B) \to if (x \in B, f (x), 0) \leq if (x \in B, C, 0)$
233	197	a1i	$⊢ \neg x \in B \to 0 \leq 0$
234		iffalse	$⊢ \neg x \in B \to if (x \in B, f (x), 0) = 0$
235		iffalse	$⊢ \neg x \in B \to if (x \in B, C, 0) = 0$
236	233 234 235	3brtr4d	$⊢ \neg x \in B \to if (x \in B, f (x), 0) \leq if (x \in B, C, 0)$
237	236	adantl	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \land \neg x \in B) \to if (x \in B, f (x), 0) \leq if (x \in B, C, 0)$
238	232 237	pm2.61dan	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to if (x \in B, f (x), 0) \leq if (x \in B, C, 0)$
239	238	a1d	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ \to if (x \in B, f (x), 0) \leq if (x \in B, C, 0))$
240	175 239	ralrimi	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \forall x \in ℝ if (x \in B, f (x), 0) \leq if (x \in B, C, 0)$
241	7	a1i	$⊢ φ \to G = (x \in ℝ ⟼ if (x \in B, C, 0))$
242	36 42 218 44 241	ofrfval2	$⊢ φ \to ((x \in ℝ ⟼ if (x \in B, f (x), 0)) \leq_{f} G \leftrightarrow \forall x \in ℝ if (x \in B, f (x), 0) \leq if (x \in B, C, 0))$
243	242	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to ((x \in ℝ ⟼ if (x \in B, f (x), 0)) \leq_{f} G \leftrightarrow \forall x \in ℝ if (x \in B, f (x), 0) \leq if (x \in B, C, 0))$
244	240 243	mpbird	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to (x \in ℝ ⟼ if (x \in B, f (x), 0)) \leq_{f} G$
245		itg2ub	$⊢ (G : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in B, f (x), 0)) \in dom \int^{1} \land (x \in ℝ ⟼ if (x \in B, f (x), 0)) \leq_{f} G) \to \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \leq \int^{2} (G)$
246	220 23 244 245	syl3anc	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \leq \int^{2} (G)$
247	19 25 158 159 211 246	le2addd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, f (x), 0))) + \int^{1} ((x \in ℝ ⟼ if (x \in B, f (x), 0))) \leq \int^{2} (F) + \int^{2} (G)$
248	13 26 28 157 247	letrd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} H)) \to \int^{1} (f) \leq \int^{2} (F) + \int^{2} (G)$
249	248	expr	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} H \to \int^{1} (f) \leq \int^{2} (F) + \int^{2} (G))$
250	249	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} H \to \int^{1} (f) \leq \int^{2} (F) + \int^{2} (G))$
251	27	rexrd	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \in ℝ^{*}$
252		itg2leub	$⊢ (H : ℝ ⟶ [0, +∞] \land \int^{2} (F) + \int^{2} (G) \in ℝ^{*}) \to (\int^{2} (H) \leq \int^{2} (F) + \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} H \to \int^{1} (f) \leq \int^{2} (F) + \int^{2} (G)))$
253	91 251 252	syl2anc	$⊢ φ \to (\int^{2} (H) \leq \int^{2} (F) + \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} H \to \int^{1} (f) \leq \int^{2} (F) + \int^{2} (G)))$
254	250 253	mpbird	$⊢ φ \to \int^{2} (H) \leq \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2splitlem

Proof