Theorem 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	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2	1	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ℝ ∈ V )
3		simpl3	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ( 0 [,) +∞ ) )
4		1re	⊢ 1 ∈ ℝ
5		0re	⊢ 0 ∈ ℝ
6	4 5	ifcli	⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ ℝ
7	6	a1i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ ℝ )
8		fconstmpt	⊢ ( ℝ × { 𝐵 } ) = ( 𝑥 ∈ ℝ ↦ 𝐵 )
9	8	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ℝ × { 𝐵 } ) = ( 𝑥 ∈ ℝ ↦ 𝐵 ) )
10		eqidd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
11	2 3 7 9 10	offval2	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) )
12		ovif2	⊢ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐵 · 1 ) , ( 𝐵 · 0 ) )
13		simp3	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
14		elrege0	⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
15	13 14	sylib	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
16	15	simpld	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℝ )
17	16	recnd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℂ )
18	17	mulridd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · 1 ) = 𝐵 )
19	17	mul01d	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · 0 ) = 0 )
20	18 19	ifeq12d	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → if ( 𝑥 ∈ 𝐴 , ( 𝐵 · 1 ) , ( 𝐵 · 0 ) ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
21	12 20	eqtrid	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
22	21	mpteq2dv	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
23	11 22	eqtrd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
24		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
25	24	i1f1	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ dom ∫1 )
26	25	3adant3	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ dom ∫1 )
27	26 16	i1fmulc	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ∈ dom ∫1 )
28	23 27	eqeltrrd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ dom ∫1 )
29	15	simprd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
30		0le0	⊢ 0 ≤ 0
31		breq2	⊢ ( 𝐵 = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) → ( 0 ≤ 𝐵 ↔ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
32		breq2	⊢ ( 0 = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
33	31 32	ifboth	⊢ ( ( 0 ≤ 𝐵 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
34	29 30 33	sylancl	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
35	34	ralrimivw	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
36		ax-resscn	⊢ ℝ ⊆ ℂ
37	36	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ℝ ⊆ ℂ )
38	16	adantr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
39		ifcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
40	38 5 39	sylancl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
41	40	ralrimiva	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
42		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
43	42	fnmpt	⊢ ( ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) Fn ℝ )
44	41 43	syl	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) Fn ℝ )
45	37 44	0pledm	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
46	5	a1i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
47		fconstmpt	⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
48	47	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
49		eqidd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
50	2 46 40 48 49	ofrfval2	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
51	45 50	bitrd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
52	35 51	mpbird	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
53		itg2itg1	⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
54	28 52 53	syl2anc	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
55	26 16	itg1mulc	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( 𝐵 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) )
56	23	fveq2d	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
57	24	itg11	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( vol ‘ 𝐴 ) )
58	57	3adant3	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( vol ‘ 𝐴 ) )
59	58	oveq2d	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )
60	55 56 59	3eqtr3d	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )
61	54 60	eqtrd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )