itgconst

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

		Ref	Expression
	Assertion	itgconst	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} B d x = B vol (A)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (y = ℜ (B) \land x \in A) \to y = ℜ (B)$
2	1	itgeq2dv	$⊢ y = ℜ (B) \to \int_{A} y d x = \int_{A} ℜ (B) d x$
3		oveq1	$⊢ y = ℜ (B) \to y vol (A) = ℜ (B) vol (A)$
4	2 3	eqeq12d	$⊢ y = ℜ (B) \to (\int_{A} y d x = y vol (A) \leftrightarrow \int_{A} ℜ (B) d x = ℜ (B) vol (A))$
5		simplr	$⊢ (((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \land x \in A) \to y \in ℝ$
6		fconstmpt	$⊢ A \times \{y\} = (x \in A ⟼ y)$
7		simpl1	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to A \in dom vol$
8		simp2	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to vol (A) \in ℝ$
9	8	adantr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to vol (A) \in ℝ$
10		simpr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to y \in ℝ$
11	10	recnd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to y \in ℂ$
12		iblconst	$⊢ (A \in dom vol \land vol (A) \in ℝ \land y \in ℂ) \to A \times \{y\} \in 𝐿^{1}$
13	7 9 11 12	syl3anc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to A \times \{y\} \in 𝐿^{1}$
14	6 13	eqeltrrid	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to (x \in A ⟼ y) \in 𝐿^{1}$
15	5 14	itgrevallem1	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int_{A} y d x = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0))) - \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0)))$
16		ifan	$⊢ if ((x \in A \land 0 \leq y), y, 0) = if (x \in A, if (0 \leq y, y, 0), 0)$
17	16	mpteq2i	$⊢ (x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0)) = (x \in ℝ ⟼ if (x \in A, if (0 \leq y, y, 0), 0))$
18	17	fveq2i	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq y, y, 0), 0)))$
19		0re	$⊢ 0 \in ℝ$
20		ifcl	$⊢ (y \in ℝ \land 0 \in ℝ) \to if (0 \leq y, y, 0) \in ℝ$
21	10 19 20	sylancl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq y, y, 0) \in ℝ$
22		max1	$⊢ (0 \in ℝ \land y \in ℝ) \to 0 \leq if (0 \leq y, y, 0)$
23	19 10 22	sylancr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to 0 \leq if (0 \leq y, y, 0)$
24		elrege0	$⊢ if (0 \leq y, y, 0) \in [0, +∞) \leftrightarrow (if (0 \leq y, y, 0) \in ℝ \land 0 \leq if (0 \leq y, y, 0))$
25	21 23 24	sylanbrc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq y, y, 0) \in [0, +∞)$
26		itg2const	$⊢ (A \in dom vol \land vol (A) \in ℝ \land if (0 \leq y, y, 0) \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq y, y, 0), 0))) = if (0 \leq y, y, 0) vol (A)$
27	7 9 25 26	syl3anc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq y, y, 0), 0))) = if (0 \leq y, y, 0) vol (A)$
28	18 27	syl5eq	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0))) = if (0 \leq y, y, 0) vol (A)$
29		ifan	$⊢ if ((x \in A \land 0 \leq - y), - y, 0) = if (x \in A, if (0 \leq - y, - y, 0), 0)$
30	29	mpteq2i	$⊢ (x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0)) = (x \in ℝ ⟼ if (x \in A, if (0 \leq - y, - y, 0), 0))$
31	30	fveq2i	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq - y, - y, 0), 0)))$
32		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
33	32	adantl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to - y \in ℝ$
34		ifcl	$⊢ (- y \in ℝ \land 0 \in ℝ) \to if (0 \leq - y, - y, 0) \in ℝ$
35	33 19 34	sylancl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq - y, - y, 0) \in ℝ$
36		max1	$⊢ (0 \in ℝ \land - y \in ℝ) \to 0 \leq if (0 \leq - y, - y, 0)$
37	19 33 36	sylancr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to 0 \leq if (0 \leq - y, - y, 0)$
38		elrege0	$⊢ if (0 \leq - y, - y, 0) \in [0, +∞) \leftrightarrow (if (0 \leq - y, - y, 0) \in ℝ \land 0 \leq if (0 \leq - y, - y, 0))$
39	35 37 38	sylanbrc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq - y, - y, 0) \in [0, +∞)$
40		itg2const	$⊢ (A \in dom vol \land vol (A) \in ℝ \land if (0 \leq - y, - y, 0) \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq - y, - y, 0), 0))) = if (0 \leq - y, - y, 0) vol (A)$
41	7 9 39 40	syl3anc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq - y, - y, 0), 0))) = if (0 \leq - y, - y, 0) vol (A)$
42	31 41	syl5eq	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0))) = if (0 \leq - y, - y, 0) vol (A)$
43	28 42	oveq12d	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0))) - \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0))) = if (0 \leq y, y, 0) vol (A) - if (0 \leq - y, - y, 0) vol (A)$
44	21	recnd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq y, y, 0) \in ℂ$
45	35	recnd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq - y, - y, 0) \in ℂ$
46	8	recnd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to vol (A) \in ℂ$
47	46	adantr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to vol (A) \in ℂ$
48	44 45 47	subdird	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to (if (0 \leq y, y, 0) - if (0 \leq - y, - y, 0)) vol (A) = if (0 \leq y, y, 0) vol (A) - if (0 \leq - y, - y, 0) vol (A)$
49		max0sub	$⊢ y \in ℝ \to if (0 \leq y, y, 0) - if (0 \leq - y, - y, 0) = y$
50	49	adantl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to if (0 \leq y, y, 0) - if (0 \leq - y, - y, 0) = y$
51	50	oveq1d	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to (if (0 \leq y, y, 0) - if (0 \leq - y, - y, 0)) vol (A) = y vol (A)$
52	43 48 51	3eqtr2rd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to y vol (A) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq y), y, 0))) - \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - y), - y, 0)))$
53	15 52	eqtr4d	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land y \in ℝ) \to \int_{A} y d x = y vol (A)$
54	53	ralrimiva	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \forall y \in ℝ \int_{A} y d x = y vol (A)$
55		recl	$⊢ B \in ℂ \to ℜ (B) \in ℝ$
56	55	3ad2ant3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to ℜ (B) \in ℝ$
57	4 54 56	rspcdva	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} ℜ (B) d x = ℜ (B) vol (A)$
58		simpl	$⊢ (y = ℑ (B) \land x \in A) \to y = ℑ (B)$
59	58	itgeq2dv	$⊢ y = ℑ (B) \to \int_{A} y d x = \int_{A} ℑ (B) d x$
60		oveq1	$⊢ y = ℑ (B) \to y vol (A) = ℑ (B) vol (A)$
61	59 60	eqeq12d	$⊢ y = ℑ (B) \to (\int_{A} y d x = y vol (A) \leftrightarrow \int_{A} ℑ (B) d x = ℑ (B) vol (A))$
62		imcl	$⊢ B \in ℂ \to ℑ (B) \in ℝ$
63	62	3ad2ant3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to ℑ (B) \in ℝ$
64	61 54 63	rspcdva	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} ℑ (B) d x = ℑ (B) vol (A)$
65	64	oveq2d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to i \int_{A} ℑ (B) d x = i ℑ (B) vol (A)$
66		ax-icn	$⊢ i \in ℂ$
67	66	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to i \in ℂ$
68	63	recnd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to ℑ (B) \in ℂ$
69	67 68 46	mulassd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to i ℑ (B) vol (A) = i ℑ (B) vol (A)$
70	65 69	eqtr4d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to i \int_{A} ℑ (B) d x = i ℑ (B) vol (A)$
71	57 70	oveq12d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x = ℜ (B) vol (A) + i ℑ (B) vol (A)$
72	56	recnd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to ℜ (B) \in ℂ$
73		mulcl	$⊢ (i \in ℂ \land ℑ (B) \in ℂ) \to i ℑ (B) \in ℂ$
74	66 68 73	sylancr	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to i ℑ (B) \in ℂ$
75	72 74 46	adddird	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to (ℜ (B) + i ℑ (B)) vol (A) = ℜ (B) vol (A) + i ℑ (B) vol (A)$
76	71 75	eqtr4d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x = (ℜ (B) + i ℑ (B)) vol (A)$
77		simpl3	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land x \in A) \to B \in ℂ$
78		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
79		iblconst	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to A \times \{B\} \in 𝐿^{1}$
80	78 79	eqeltrrid	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to (x \in A ⟼ B) \in 𝐿^{1}$
81	77 80	itgcnval	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
82		replim	$⊢ B \in ℂ \to B = ℜ (B) + i ℑ (B)$
83	82	3ad2ant3	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to B = ℜ (B) + i ℑ (B)$
84	83	oveq1d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to B vol (A) = (ℜ (B) + i ℑ (B)) vol (A)$
85	76 81 84	3eqtr4d	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \int_{A} B d x = B vol (A)$

Metamath Proof Explorer

Theorem itgconst

Proof