itg2add

Description: The S.2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	itg2add.f1	$⊢ φ \to F \in MblFn$
	itg2add.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2add.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2add.g1	$⊢ φ \to G \in MblFn$
	itg2add.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
	itg2add.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
Assertion	itg2add	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

Proof

Step	Hyp	Ref	Expression
1		itg2add.f1	$⊢ φ \to F \in MblFn$
2		itg2add.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2add.f3	$⊢ φ \to \int^{2} (F) \in ℝ$
4		itg2add.g1	$⊢ φ \to G \in MblFn$
5		itg2add.g2	$⊢ φ \to G : ℝ ⟶ [0, +∞)$
6		itg2add.g3	$⊢ φ \to \int^{2} (G) \in ℝ$
7	1 2	mbfi1fseq	$⊢ φ \to \exists f (f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x))$
8	4 5	mbfi1fseq	$⊢ φ \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x))$
9		exdistrv	$⊢ \exists f \exists g ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x))) \leftrightarrow (\exists f (f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))$
10	1	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to F \in MblFn$
11	2	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to F : ℝ ⟶ [0, +∞)$
12	3	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \int^{2} (F) \in ℝ$
13	4	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to G \in MblFn$
14	5	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to G : ℝ ⟶ [0, +∞)$
15	6	adantr	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \int^{2} (G) \in ℝ$
16		simprl1	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to f : ℕ ⟶ dom \int^{1}$
17		simprl2	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1))$
18		simprl3	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)$
19		simprr1	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to g : ℕ ⟶ dom \int^{1}$
20		simprr2	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1))$
21		simprr3	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)$
22	10 11 12 13 14 15 16 17 18 19 20 21	itg2addlem	$⊢ (φ \land ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x)))) \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$
23	22	ex	$⊢ φ \to (((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x))) \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G))$
24	23	exlimdvv	$⊢ φ \to (\exists f \exists g ((f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x))) \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G))$
25	9 24	syl5bir	$⊢ φ \to ((\exists f (f : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} f (n) \land f (n) \leq_{f} f (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ f (n) (x)) ⇝ F (x)) \land \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ G (x))) \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G))$
26	7 8 25	mp2and	$⊢ φ \to \int^{2} (F +_{f} G) = \int^{2} (F) + \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2add

Proof