itg2const

Description: Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	itg2const	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = B vol (A)$

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2	1	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to ℝ \in V$
3		simpl3	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \land x \in ℝ) \to B \in [0, +∞)$
4		1re	$⊢ 1 \in ℝ$
5		0re	$⊢ 0 \in ℝ$
6	4 5	ifcli	$⊢ if (x \in A, 1, 0) \in ℝ$
7	6	a1i	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \land x \in ℝ) \to if (x \in A, 1, 0) \in ℝ$
8		fconstmpt	$⊢ ℝ \times \{B\} = (x \in ℝ ⟼ B)$
9	8	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to ℝ \times \{B\} = (x \in ℝ ⟼ B)$
10		eqidd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ if (x \in A, 1, 0)) = (x \in ℝ ⟼ if (x \in A, 1, 0))$
11	2 3 7 9 10	offval2	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (ℝ \times \{B\}) \times_{f} (x \in ℝ ⟼ if (x \in A, 1, 0)) = (x \in ℝ ⟼ B if (x \in A, 1, 0))$
12		ovif2	$⊢ B if (x \in A, 1, 0) = if (x \in A, B \cdot 1, B \cdot 0)$
13		simp3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \in [0, +∞)$
14		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
15	13 14	sylib	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (B \in ℝ \land 0 \leq B)$
16	15	simpld	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \in ℝ$
17	16	recnd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \in ℂ$
18	17	mulid1d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \cdot 1 = B$
19	17	mul01d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \cdot 0 = 0$
20	18 19	ifeq12d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to if (x \in A, B \cdot 1, B \cdot 0) = if (x \in A, B, 0)$
21	12 20	syl5eq	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B if (x \in A, 1, 0) = if (x \in A, B, 0)$
22	21	mpteq2dv	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ B if (x \in A, 1, 0)) = (x \in ℝ ⟼ if (x \in A, B, 0))$
23	11 22	eqtrd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (ℝ \times \{B\}) \times_{f} (x \in ℝ ⟼ if (x \in A, 1, 0)) = (x \in ℝ ⟼ if (x \in A, B, 0))$
24		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, 1, 0)) = (x \in ℝ ⟼ if (x \in A, 1, 0))$
25	24	i1f1	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to (x \in ℝ ⟼ if (x \in A, 1, 0)) \in dom \int^{1}$
26	25	3adant3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ if (x \in A, 1, 0)) \in dom \int^{1}$
27	26 16	i1fmulc	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (ℝ \times \{B\}) \times_{f} (x \in ℝ ⟼ if (x \in A, 1, 0)) \in dom \int^{1}$
28	23 27	eqeltrrd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ if (x \in A, B, 0)) \in dom \int^{1}$
29	15	simprd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to 0 \leq B$
30		0le0	$⊢ 0 \leq 0$
31		breq2	$⊢ B = if (x \in A, B, 0) \to (0 \leq B \leftrightarrow 0 \leq if (x \in A, B, 0))$
32		breq2	$⊢ 0 = if (x \in A, B, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (x \in A, B, 0))$
33	31 32	ifboth	$⊢ (0 \leq B \land 0 \leq 0) \to 0 \leq if (x \in A, B, 0)$
34	29 30 33	sylancl	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to 0 \leq if (x \in A, B, 0)$
35	34	ralrimivw	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \forall x \in ℝ 0 \leq if (x \in A, B, 0)$
36		ax-resscn	$⊢ ℝ \subseteq ℂ$
37	36	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to ℝ \subseteq ℂ$
38	16	adantr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \land x \in ℝ) \to B \in ℝ$
39		ifcl	$⊢ (B \in ℝ \land 0 \in ℝ) \to if (x \in A, B, 0) \in ℝ$
40	38 5 39	sylancl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \land x \in ℝ) \to if (x \in A, B, 0) \in ℝ$
41	40	ralrimiva	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \forall x \in ℝ if (x \in A, B, 0) \in ℝ$
42		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, B, 0)) = (x \in ℝ ⟼ if (x \in A, B, 0))$
43	42	fnmpt	$⊢ \forall x \in ℝ if (x \in A, B, 0) \in ℝ \to (x \in ℝ ⟼ if (x \in A, B, 0)) Fn ℝ$
44	41 43	syl	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ if (x \in A, B, 0)) Fn ℝ$
45	37 44	0pledm	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (0_{𝑝} \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0)) \leftrightarrow (ℝ \times \{0\}) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0)))$
46	5	a1i	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \land x \in ℝ) \to 0 \in ℝ$
47		fconstmpt	$⊢ ℝ \times \{0\} = (x \in ℝ ⟼ 0)$
48	47	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to ℝ \times \{0\} = (x \in ℝ ⟼ 0)$
49		eqidd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (x \in ℝ ⟼ if (x \in A, B, 0)) = (x \in ℝ ⟼ if (x \in A, B, 0))$
50	2 46 40 48 49	ofrfval2	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to ((ℝ \times \{0\}) \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0)) \leftrightarrow \forall x \in ℝ 0 \leq if (x \in A, B, 0))$
51	45 50	bitrd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to (0_{𝑝} \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0)) \leftrightarrow \forall x \in ℝ 0 \leq if (x \in A, B, 0))$
52	35 51	mpbird	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to 0_{𝑝} \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))$
53		itg2itg1	$⊢ ((x \in ℝ ⟼ if (x \in A, B, 0)) \in dom \int^{1} \land 0_{𝑝} \leq_{f} (x \in ℝ ⟼ if (x \in A, B, 0))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
54	28 52 53	syl2anc	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
55	26 16	itg1mulc	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{1} ((ℝ \times \{B\}) \times_{f} (x \in ℝ ⟼ if (x \in A, 1, 0))) = B \int^{1} ((x \in ℝ ⟼ if (x \in A, 1, 0)))$
56	23	fveq2d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{1} ((ℝ \times \{B\}) \times_{f} (x \in ℝ ⟼ if (x \in A, 1, 0))) = \int^{1} ((x \in ℝ ⟼ if (x \in A, B, 0)))$
57	24	itg11	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 1, 0))) = vol (A)$
58	57	3adant3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 1, 0))) = vol (A)$
59	58	oveq2d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to B \int^{1} ((x \in ℝ ⟼ if (x \in A, 1, 0))) = B vol (A)$
60	55 56 59	3eqtr3d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, B, 0))) = B vol (A)$
61	54 60	eqtrd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, B, 0))) = B vol (A)$

Metamath Proof Explorer

Theorem itg2const

Proof