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		simpr	$⊢ (φ \land g Fn ℝ) \to g Fn ℝ$
96		dffn5	$⊢ g Fn ℝ \leftrightarrow g = (x \in ℝ ⟼ g (x))$
97	95 96	sylib	$⊢ (φ \land g Fn ℝ) \to g = (x \in ℝ ⟼ g (x))$
98	7	a1i	$⊢ (φ \land g Fn ℝ) \to G = (x \in ℝ ⟼ if (x \in B, C, 0))$
99	85 86 94 97 98	ofrfval2	$⊢ (φ \land g Fn ℝ) \to (g \leq_{f} G \leftrightarrow \forall x \in ℝ g (x) \leq if (x \in B, C, 0))$
100	60 99	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))$
101	84 100	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)$
102	101	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)$
103	54 102	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)$
104	103	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)$
105		eldifn	$⊢ x \in (ℝ ∖ (A \cap B)) \to \neg x \in (A \cap B)$
106	105	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)$
107		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
108	106 107	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)$
109		imnan	$⊢ (x \in A \to \neg x \in B) \leftrightarrow \neg (x \in A \land x \in B)$
110	108 109	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)$
111	110	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$
112	111	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$
113	104 112	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$
114	82 83 75 113	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$
115	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 ℂ$
116	115	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)$
117	114 116	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)$
118		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$
119	61	a1i	$⊢ (φ \land f Fn ℝ) \to ℝ \in V$
120		fvexd	$⊢ ((φ \land f Fn ℝ) \land x \in ℝ) \to f (x) \in V$
121		ssun1	$⊢ A \subseteq A \cup B$
122	121 4	sseqtrrid	$⊢ φ \to A \subseteq U$
123	122	sselda	$⊢ (φ \land x \in A) \to x \in U$
124	123	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in A) \to x \in U$
125	124 11	syldan	$⊢ ((φ \land x \in ℝ) \land x \in A) \to C \in [0, +∞]$
126	12	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to 0 \in [0, +∞]$
127	125 126	ifclda	$⊢ (φ \land x \in ℝ) \to if (x \in A, C, 0) \in [0, +∞]$
128	127	adantlr	$⊢ ((φ \land f Fn ℝ) \land x \in ℝ) \to if (x \in A, C, 0) \in [0, +∞]$
129		simpr	$⊢ (φ \land f Fn ℝ) \to f Fn ℝ$
130		dffn5	$⊢ f Fn ℝ \leftrightarrow f = (x \in ℝ ⟼ f (x))$
131	129 130	sylib	$⊢ (φ \land f Fn ℝ) \to f = (x \in ℝ ⟼ f (x))$
132	6	a1i	$⊢ (φ \land f Fn ℝ) \to F = (x \in ℝ ⟼ if (x \in A, C, 0))$
133	119 120 128 131 132	ofrfval2	$⊢ (φ \land f Fn ℝ) \to (f \leq_{f} F \leftrightarrow \forall x \in ℝ f (x) \leq if (x \in A, C, 0))$
134	57 133	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))$
135	118 134	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)$
136	135	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)$
137	54 136	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)$
138	137	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)$
139	122	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$
140	139	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$
141	140	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$
142		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 ℝ$
143	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, +∞]$
144	8	fvmpt2	$⊢ (x \in ℝ \land if (x \in U, C, 0) \in [0, +∞]) \to H (x) = if (x \in U, C, 0)$
145	142 143 144	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)$
146	54 145	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)$
147	146	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)$
148		iftrue	$⊢ x \in A \to if (x \in A, C, 0) = C$
149	148	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$
150	141 147 149	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)$
151	138 150	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)$
152	74 76 81 117 151	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)$
153	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 ℝ^{*}$
154	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 ℝ$
155	154	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 ℝ^{*}$
156	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 ℝ^{*}$
157	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 ℝ$
158		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 ℝ$
159	137	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)$
160		iffalse	$⊢ \neg x \in A \to if (x \in A, C, 0) = 0$
161	160	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$
162	159 161	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$
163	157 158 154 162	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)$
164	154	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 ℂ$
165	164	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)$
166	163 165	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)$
167	103	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)$
168	146	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)$
169	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$
170	169	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))$
171		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
172		biorf	$⊢ \neg x \in A \to (x \in B \leftrightarrow (x \in A \lor x \in B))$
173	171 172	bitr4id	$⊢ \neg x \in A \to (x \in (A \cup B) \leftrightarrow x \in B)$
174	173	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)$
175	170 174	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)$
176	175	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)$
177	168 176	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)$
178	167 177	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)$
179	153 155 156 166 178	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)$
180	152 179	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)$
181	67 180	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)$
182	181	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))$
183	53 182	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)$
184		nfv	$⊢ Ⅎ y (f +_{f} g) (x) \leq H (x)$
185		nfcv	$⊢ \underline{Ⅎ} x (f +_{f} g) (y)$
186		nfcv	$⊢ \underline{Ⅎ} x \leq$
187		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in U, C, 0))$
188	8 187	nfcxfr	$⊢ \underline{Ⅎ} x H$
189		nfcv	$⊢ \underline{Ⅎ} x y$
190	188 189	nffv	$⊢ \underline{Ⅎ} x H (y)$
191	185 186 190	nfbr	$⊢ Ⅎ x (f +_{f} g) (y) \leq H (y)$
192		fveq2	$⊢ x = y \to (f +_{f} g) (x) = (f +_{f} g) (y)$
193		fveq2	$⊢ x = y \to H (x) = H (y)$
194	192 193	breq12d	$⊢ x = y \to ((f +_{f} g) (x) \leq H (x) \leftrightarrow (f +_{f} g) (y) \leq H (y))$
195	184 191 194	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)$
196	183 195	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)$
197	196	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)$
198	30 31 36 37 197	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)$
199	29 198	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)$
200	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 ℝ$
201		itg1cl	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ$
202	28 201	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 ℝ$
203	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 ℝ$
204	200 202 203	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))$
205	199 204	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)$
206	205	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)$
207	206	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))$
208	207	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))$
209	93 7	fmptd	$⊢ φ \to G : ℝ ⟶ [0, +∞]$
210	209	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to G : ℝ ⟶ [0, +∞]$
211	24 26	resubcld	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (H) - \int^{1} (f) \in ℝ$
212	211	rexrd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (H) - \int^{1} (f) \in ℝ^{*}$
213		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)))$
214	210 212 213	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)))$
215	208 214	mpbird	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{2} (G) \leq \int^{2} (H) - \int^{1} (f)$
216	21 24 26 215	lesubd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G)$
217	216	expr	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G))$
218	217	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (H) - \int^{2} (G))$
219	127 6	fmptd	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
220	23 10	resubcld	$⊢ φ \to \int^{2} (H) - \int^{2} (G) \in ℝ$
221	220	rexrd	$⊢ φ \to \int^{2} (H) - \int^{2} (G) \in ℝ^{*}$
222		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)))$
223	219 221 222	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)))$
224	218 223	mpbird	$⊢ φ \to \int^{2} (F) \leq \int^{2} (H) - \int^{2} (G)$
225		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))$
226	9 10 23 225	syl3anc	$⊢ φ \to (\int^{2} (F) + \int^{2} (G) \leq \int^{2} (H) \leftrightarrow \int^{2} (F) \leq \int^{2} (H) - \int^{2} (G))$
227	224 226	mpbird	$⊢ φ \to \int^{2} (F) + \int^{2} (G) \leq \int^{2} (H)$
228	17 19 20 227	xrletrid	$⊢ φ \to \int^{2} (H) = \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2split

Proof