itg2split

Description: The S.2 integral splits under an almost disjoint union. The proof avoids the use of itg2add , which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014)

	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	itg2split	$⊢ φ \to \int^{2} (H) = \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	5	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in U) \to C \in [0, +∞]$
12		0e0iccpnf	$⊢ 0 \in [0, +∞]$
13	12	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in U) \to 0 \in [0, +∞]$
14	11 13	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in U, C, 0) \in [0, +∞]$
15	14 8	fmptd	$⊢ φ \to H : ℝ ⟶ [0, +∞]$
16		itg2cl	$⊢ H : ℝ ⟶ [0, +∞] \to \int^{2} (H) \in ℝ^{*}$
17	15 16	syl	$⊢ φ \to \int^{2} (H) \in ℝ^{*}$
18	9 10	readdcld	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \in ℝ$
19	18	rexrd	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \in ℝ^{*}$
20	1 2 3 4 5 6 7 8 9 10	itg2splitlem	$⊢ φ \to \int^{2} (H) \leq \int^{2} (F) + \int^{2} (G)$
21	10	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (G) \in ℝ$
22		itg2lecl	$⊢ (H : ℝ ⟶ [0, +∞] \land \int^{2} (F) + \int^{2} (G) \in ℝ \land \int^{2} (H) \leq \int^{2} (F) + \int^{2} (G)) \to \int^{2} (H) \in ℝ$
23	15 18 20 22	syl3anc	$⊢ φ \to \int^{2} (H) \in ℝ$
24	23	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (H) \in ℝ$
25		itg1cl	$⊢ f \in dom \int^{1} \to \int^{1} (f) \in ℝ$
26	25	ad2antrl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{1} (f) \in ℝ$
27		simprll	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to f \in dom \int^{1}$
28		simprrl	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to g \in dom \int^{1}$
29	27 28	itg1add	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (f +_{f} g) = \int^{1} (f) + \int^{1} (g)$
30	15	adantr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to H : ℝ ⟶ [0, +∞]$
31	27 28	i1fadd	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to f +_{f} g \in dom \int^{1}$
32		inss1	$⊢ A \cap B \subseteq A$
33		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
34	1 33	syl	$⊢ φ \to A \subseteq ℝ$
35	32 34	sstrid	$⊢ φ \to A \cap B \subseteq ℝ$
36	35	adantr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to A \cap B \subseteq ℝ$
37	3	adantr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to {vol}^{*} (A \cap B) = 0$
38		nfv	$⊢ Ⅎ x φ$
39		nfv	$⊢ Ⅎ x f \in dom \int^{1}$
40		nfcv	$⊢ \underline{Ⅎ} x f$
41		nfcv	$⊢ \underline{Ⅎ} x \circ_{r} \leq$
42		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in A, C, 0))$
43	6 42	nfcxfr	$⊢ \underline{Ⅎ} x F$
44	40 41 43	nfbr	$⊢ Ⅎ x f \leq_{f} F$
45	39 44	nfan	$⊢ Ⅎ x (f \in dom \int^{1} \land f \leq_{f} F)$
46		nfv	$⊢ Ⅎ x g \in dom \int^{1}$
47		nfcv	$⊢ \underline{Ⅎ} x g$
48		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in B, C, 0))$
49	7 48	nfcxfr	$⊢ \underline{Ⅎ} x G$
50	47 41 49	nfbr	$⊢ Ⅎ x g \leq_{f} G$
51	46 50	nfan	$⊢ Ⅎ x (g \in dom \int^{1} \land g \leq_{f} G)$
52	45 51	nfan	$⊢ Ⅎ x ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))$
53	38 52	nfan	$⊢ Ⅎ x (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G)))$
54		eldifi	$⊢ x \in (ℝ ∖ (A \cap B)) \to x \in ℝ$
55		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
56	27 55	syl	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to f : ℝ ⟶ ℝ$
57	56	ffnd	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to f Fn ℝ$
58		i1ff	$⊢ g \in dom \int^{1} \to g : ℝ ⟶ ℝ$
59	28 58	syl	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to g : ℝ ⟶ ℝ$
60	59	ffnd	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to g Fn ℝ$
61		reex	$⊢ ℝ \in V$
62	61	a1i	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to ℝ \in V$
63		inidm	$⊢ ℝ \cap ℝ = ℝ$
64		eqidd	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to f (x) = f (x)$
65		eqidd	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to g (x) = g (x)$
66	57 60 62 62 63 64 65	ofval	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to (f +_{f} g) (x) = f (x) + g (x)$
67	54 66	sylan2	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to (f +_{f} g) (x) = f (x) + g (x)$
68		ffvelcdm	$⊢ (f : ℝ ⟶ ℝ \land x \in ℝ) \to f (x) \in ℝ$
69	56 54 68	syl2an	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to f (x) \in ℝ$
70		ffvelcdm	$⊢ (g : ℝ ⟶ ℝ \land x \in ℝ) \to g (x) \in ℝ$
71	59 54 70	syl2an	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to g (x) \in ℝ$
72	69 71	readdcld	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to f (x) + g (x) \in ℝ$
73	72	rexrd	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to f (x) + g (x) \in ℝ^{*}$
74	73	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) + g (x) \in ℝ^{*}$
75	69	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) \in ℝ$
76	75	rexrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) \in ℝ^{*}$
77		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
78		ffvelcdm	$⊢ (H : ℝ ⟶ [0, +∞] \land x \in ℝ) \to H (x) \in [0, +∞]$
79	30 54 78	syl2an	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to H (x) \in [0, +∞]$
80	77 79	sselid	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to H (x) \in ℝ^{*}$
81	80	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to H (x) \in ℝ^{*}$
82	71	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to g (x) \in ℝ$
83		0red	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to 0 \in ℝ$
84		simprrr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to g \leq_{f} G$
85	61	a1i	$⊢ (φ \land g Fn ℝ) \to ℝ \in V$
86		fvexd	$⊢ ((φ \land g Fn ℝ) \land x \in ℝ) \to g (x) \in V$
87		ssun2	$⊢ B \subseteq A \cup B$
88	87 4	sseqtrrid	$⊢ φ \to B \subseteq U$
89	88	sselda	$⊢ (φ \land x \in B) \to x \in U$
90	89	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in B) \to x \in U$
91	90 11	syldan	$⊢ ((φ \land x \in ℝ) \land x \in B) \to C \in [0, +∞]$
92	12	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in B) \to 0 \in [0, +∞]$
93	91 92	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in B, C, 0) \in [0, +∞]$
94	93	adantlr	$⊢ ((φ \land g Fn ℝ) \land x \in ℝ) \to if (x \in B, C, 0) \in [0, +∞]$
95		dffn5	$⊢ g Fn ℝ \leftrightarrow g = (x \in ℝ ⟼ g (x))$
96	95	bilani	$⊢ (φ \land g Fn ℝ) \to g = (x \in ℝ ⟼ g (x))$
97	7	a1i	$⊢ (φ \land g Fn ℝ) \to G = (x \in ℝ ⟼ if (x \in B, C, 0))$
98	85 86 94 96 97	ofrfval2	$⊢ (φ \land g Fn ℝ) \to (g \leq_{f} G \leftrightarrow \forall x \in ℝ g (x) \leq if (x \in B, C, 0))$
99	60 98	syldan	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to (g \leq_{f} G \leftrightarrow \forall x \in ℝ g (x) \leq if (x \in B, C, 0))$
100	84 99	mpbid	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \forall x \in ℝ g (x) \leq if (x \in B, C, 0)$
101	100	r19.21bi	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to g (x) \leq if (x \in B, C, 0)$
102	54 101	sylan2	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to g (x) \leq if (x \in B, C, 0)$
103	102	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to g (x) \leq if (x \in B, C, 0)$
104		eldifn	$⊢ x \in (ℝ ∖ (A \cap B)) \to \neg x \in (A \cap B)$
105	104	adantl	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to \neg x \in (A \cap B)$
106		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
107	105 106	sylnib	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to \neg (x \in A \land x \in B)$
108		imnan	$⊢ (x \in A \to \neg x \in B) \leftrightarrow \neg (x \in A \land x \in B)$
109	107 108	sylibr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to (x \in A \to \neg x \in B)$
110	109	imp	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to \neg x \in B$
111	110	iffalsed	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to if (x \in B, C, 0) = 0$
112	103 111	breqtrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to g (x) \leq 0$
113	82 83 75 112	leadd2dd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) + g (x) \leq f (x) + 0$
114	75	recnd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) \in ℂ$
115	114	addridd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) + 0 = f (x)$
116	113 115	breqtrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) + g (x) \leq f (x)$
117		simprlr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to f \leq_{f} F$
118	61	a1i	$⊢ (φ \land f Fn ℝ) \to ℝ \in V$
119		fvexd	$⊢ ((φ \land f Fn ℝ) \land x \in ℝ) \to f (x) \in V$
120		ssun1	$⊢ A \subseteq A \cup B$
121	120 4	sseqtrrid	$⊢ φ \to A \subseteq U$
122	121	sselda	$⊢ (φ \land x \in A) \to x \in U$
123	122	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in A) \to x \in U$
124	123 11	syldan	$⊢ ((φ \land x \in ℝ) \land x \in A) \to C \in [0, +∞]$
125	12	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to 0 \in [0, +∞]$
126	124 125	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in A, C, 0) \in [0, +∞]$
127	126	adantlr	$⊢ ((φ \land f Fn ℝ) \land x \in ℝ) \to if (x \in A, C, 0) \in [0, +∞]$
128		dffn5	$⊢ f Fn ℝ \leftrightarrow f = (x \in ℝ ⟼ f (x))$
129	128	bilani	$⊢ (φ \land f Fn ℝ) \to f = (x \in ℝ ⟼ f (x))$
130	6	a1i	$⊢ (φ \land f Fn ℝ) \to F = (x \in ℝ ⟼ if (x \in A, C, 0))$
131	118 119 127 129 130	ofrfval2	$⊢ (φ \land f Fn ℝ) \to (f \leq_{f} F \leftrightarrow \forall x \in ℝ f (x) \leq if (x \in A, C, 0))$
132	57 131	syldan	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to (f \leq_{f} F \leftrightarrow \forall x \in ℝ f (x) \leq if (x \in A, C, 0))$
133	117 132	mpbid	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \forall x \in ℝ f (x) \leq if (x \in A, C, 0)$
134	133	r19.21bi	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to f (x) \leq if (x \in A, C, 0)$
135	54 134	sylan2	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to f (x) \leq if (x \in A, C, 0)$
136	135	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) \leq if (x \in A, C, 0)$
137	121	ad2antrr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to A \subseteq U$
138	137	sselda	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to x \in U$
139	138	iftrued	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to if (x \in U, C, 0) = C$
140		simpr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to x \in ℝ$
141	14	adantlr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to if (x \in U, C, 0) \in [0, +∞]$
142	8	fvmpt2	$⊢ (x \in ℝ \land if (x \in U, C, 0) \in [0, +∞]) \to H (x) = if (x \in U, C, 0)$
143	140 141 142	syl2anc	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in ℝ) \to H (x) = if (x \in U, C, 0)$
144	54 143	sylan2	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to H (x) = if (x \in U, C, 0)$
145	144	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to H (x) = if (x \in U, C, 0)$
146		iftrue	$⊢ x \in A \to if (x \in A, C, 0) = C$
147	146	adantl	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to if (x \in A, C, 0) = C$
148	139 145 147	3eqtr4d	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to H (x) = if (x \in A, C, 0)$
149	136 148	breqtrrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) \leq H (x)$
150	74 76 81 116 149	xrletrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land x \in A) \to f (x) + g (x) \leq H (x)$
151	73	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) + g (x) \in ℝ^{*}$
152	71	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to g (x) \in ℝ$
153	152	rexrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to g (x) \in ℝ^{*}$
154	80	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to H (x) \in ℝ^{*}$
155	69	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) \in ℝ$
156		0red	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to 0 \in ℝ$
157	135	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) \leq if (x \in A, C, 0)$
158		iffalse	$⊢ \neg x \in A \to if (x \in A, C, 0) = 0$
159	158	adantl	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to if (x \in A, C, 0) = 0$
160	157 159	breqtrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) \leq 0$
161	155 156 152 160	leadd1dd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) + g (x) \leq 0 + g (x)$
162	152	recnd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to g (x) \in ℂ$
163	162	addlidd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to 0 + g (x) = g (x)$
164	161 163	breqtrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) + g (x) \leq g (x)$
165	102	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to g (x) \leq if (x \in B, C, 0)$
166	144	adantr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to H (x) = if (x \in U, C, 0)$
167	4	ad3antrrr	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to U = A \cup B$
168	167	eleq2d	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to (x \in U \leftrightarrow x \in (A \cup B))$
169		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
170		biorf	$⊢ \neg x \in A \to (x \in B \leftrightarrow (x \in A \lor x \in B))$
171	169 170	bitr4id	$⊢ \neg x \in A \to (x \in (A \cup B) \leftrightarrow x \in B)$
172	171	adantl	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to (x \in (A \cup B) \leftrightarrow x \in B)$
173	168 172	bitrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to (x \in U \leftrightarrow x \in B)$
174	173	ifbid	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to if (x \in U, C, 0) = if (x \in B, C, 0)$
175	166 174	eqtrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to H (x) = if (x \in B, C, 0)$
176	165 175	breqtrrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to g (x) \leq H (x)$
177	151 153 154 164 176	xrletrd	$⊢ (((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \land \neg x \in A) \to f (x) + g (x) \leq H (x)$
178	150 177	pm2.61dan	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to f (x) + g (x) \leq H (x)$
179	67 178	eqbrtrd	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land x \in (ℝ ∖ (A \cap B))) \to (f +_{f} g) (x) \leq H (x)$
180	179	ex	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to (x \in (ℝ ∖ (A \cap B)) \to (f +_{f} g) (x) \leq H (x))$
181	53 180	ralrimi	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \forall x \in (ℝ ∖ (A \cap B)) (f +_{f} g) (x) \leq H (x)$
182		nfv	$⊢ Ⅎ y (f +_{f} g) (x) \leq H (x)$
183		nfcv	$⊢ \underline{Ⅎ} x (f +_{f} g) (y)$
184		nfcv	$⊢ \underline{Ⅎ} x \leq$
185		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in U, C, 0))$
186	8 185	nfcxfr	$⊢ \underline{Ⅎ} x H$
187		nfcv	$⊢ \underline{Ⅎ} x y$
188	186 187	nffv	$⊢ \underline{Ⅎ} x H (y)$
189	183 184 188	nfbr	$⊢ Ⅎ x (f +_{f} g) (y) \leq H (y)$
190		fveq2	$⊢ x = y \to (f +_{f} g) (x) = (f +_{f} g) (y)$
191		fveq2	$⊢ x = y \to H (x) = H (y)$
192	190 191	breq12d	$⊢ x = y \to ((f +_{f} g) (x) \leq H (x) \leftrightarrow (f +_{f} g) (y) \leq H (y))$
193	182 189 192	cbvralw	$⊢ \forall x \in (ℝ ∖ (A \cap B)) (f +_{f} g) (x) \leq H (x) \leftrightarrow \forall y \in (ℝ ∖ (A \cap B)) (f +_{f} g) (y) \leq H (y)$
194	181 193	sylib	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \forall y \in (ℝ ∖ (A \cap B)) (f +_{f} g) (y) \leq H (y)$
195	194	r19.21bi	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \land y \in (ℝ ∖ (A \cap B))) \to (f +_{f} g) (y) \leq H (y)$
196	30 31 36 37 195	itg2uba	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (f +_{f} g) \leq \int^{2} (H)$
197	29 196	eqbrtrrd	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (f) + \int^{1} (g) \leq \int^{2} (H)$
198	26	adantrr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (f) \in ℝ$
199		itg1cl	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ$
200	28 199	syl	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (g) \in ℝ$
201	23	adantr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{2} (H) \in ℝ$
202	198 200 201	leaddsub2d	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to (\int^{1} (f) + \int^{1} (g) \leq \int^{2} (H) \leftrightarrow \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f))$
203	197 202	mpbid	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} F) \land (g \in dom \int^{1} \land g \leq_{f} G))) \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f)$
204	203	anassrs	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land (g \in dom \int^{1} \land g \leq_{f} G)) \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f)$
205	204	expr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land g \in dom \int^{1}) \to (g \leq_{f} G \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f))$
206	205	ralrimiva	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \forall g \in dom \int^{1} (g \leq_{f} G \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f))$
207	93 7	fmptd	$⊢ φ \to G : ℝ ⟶ [0, +∞]$
208	207	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to G : ℝ ⟶ [0, +∞]$
209	24 26	resubcld	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (H) - \int^{1} (f) \in ℝ$
210	209	rexrd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (H) - \int^{1} (f) \in ℝ^{*}$
211		itg2leub	$⊢ (G : ℝ ⟶ [0, +∞] \land \int^{2} (H) - \int^{1} (f) \in ℝ^{*}) \to (\int^{2} (G) \leq \int^{2} (H) - \int^{1} (f) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} G \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f)))$
212	208 210 211	syl2anc	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to (\int^{2} (G) \leq \int^{2} (H) - \int^{1} (f) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} G \to \int^{1} (g) \leq \int^{2} (H) - \int^{1} (f)))$
213	206 212	mpbird	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (G) \leq \int^{2} (H) - \int^{1} (f)$
214	21 24 26 213	lesubd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G)$
215	214	expr	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G))$
216	215	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G))$
217	126 6	fmptd	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
218	23 10	resubcld	$⊢ φ \to \int^{2} (H) - \int^{2} (G) \in ℝ$
219	218	rexrd	$⊢ φ \to \int^{2} (H) - \int^{2} (G) \in ℝ^{*}$
220		itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land \int^{2} (H) - \int^{2} (G) \in ℝ^{*}) \to (\int^{2} (F) \leq \int^{2} (H) - \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G)))$
221	217 219 220	syl2anc	$⊢ φ \to (\int^{2} (F) \leq \int^{2} (H) - \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G)))$
222	216 221	mpbird	$⊢ φ \to \int^{2} (F) \leq \int^{2} (H) - \int^{2} (G)$
223		leaddsub	$⊢ (\int^{2} (F) \in ℝ \land \int^{2} (G) \in ℝ \land \int^{2} (H) \in ℝ) \to (\int^{2} (F) + \int^{2} (G) \leq \int^{2} (H) \leftrightarrow \int^{2} (F) \leq \int^{2} (H) - \int^{2} (G))$
224	9 10 23 223	syl3anc	$⊢ φ \to (\int^{2} (F) + \int^{2} (G) \leq \int^{2} (H) \leftrightarrow \int^{2} (F) \leq \int^{2} (H) - \int^{2} (G))$
225	222 224	mpbird	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \leq \int^{2} (H)$
226	17 19 20 225	xrletrid	$⊢ φ \to \int^{2} (H) = \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2split

Proof