Theorem iblabslem 26203

Description: Lemma for iblabs 26204. (Contributed by Mario Carneiro, 25-Aug-2014.)

Hypotheses

Ref	Expression
iblabs.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
iblabs.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
iblabs.3	⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
iblabs.4	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)
iblabs.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)

Assertion

Ref	Expression
iblabslem	⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝑉(𝑥)

Proof of Theorem iblabslem

Step	Hyp	Ref	Expression
1		iblabs.3	. . 3 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
2		iblabs.4	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)
3		iblabs.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)
4	3	iblrelem 26166	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ)))
5	2, 4	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ))
6	5	simp1d 1160	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn)
7	6, 3	mbfdm2 26013	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ dom vol)
8		mblss 25907	. . . . 5 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
9	7, 8	syl 18	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
10		rembl 25916	. . . . 5 ⊢ ℝ ∈ dom vol
11	10	a1i 11	. . . 4 ⊢ (𝜑 → ℝ ∈ dom vol)
12		iftrue 4491	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵)))
13	12	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = (abs‘(𝐹‘𝐵)))
14	3	recnd 11376	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ)
15	14	abscld 15650	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐹‘𝐵)) ∈ ℝ)
16	13, 15	eqeltrd 2864	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) ∈ ℝ)
17		eldifn 4071	. . . . . 6 ⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴)
18	17	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴)
19		iffalse 4494	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0)
20	18, 19	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0) = 0)
21	12	mpteq2ia 5206	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵)))
22		absf 15548	. . . . . . . 8 ⊢ abs:ℂ⟶ℝ
23	22	a1i 11	. . . . . . 7 ⊢ (𝜑 → abs:ℂ⟶ℝ)
24	23, 14	cofmpt 7165	. . . . . 6 ⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (abs‘(𝐹‘𝐵))))
25	21, 24	eqtr4id 2817	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) = (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))))
26	14	fmpttd 7147	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ)
27		ax-resscn 11296	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
28		ssid 3935	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
29		cncfss 25275	. . . . . . . . 9 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
30	27, 28, 29	mp2an 705	. . . . . . . 8 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
31		abscncf 25277	. . . . . . . 8 ⊢ abs ∈ (ℂ–cn→ℝ)
32	30, 31	sselii 3910	. . . . . . 7 ⊢ abs ∈ (ℂ–cn→ℂ)
33	32	a1i 11	. . . . . 6 ⊢ (𝜑 → abs ∈ (ℂ–cn→ℂ))
34		cncombf 26034	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ ∧ abs ∈ (ℂ–cn→ℂ)) → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn)
35	6, 26, 33, 34	syl3anc 1399	. . . . 5 ⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) ∈ MblFn)
36	25, 35	eqeltrd 2864	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn)
37	9, 11, 16, 20, 36	mbfss 26022	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)) ∈ MblFn)
38	1, 37	eqeltrid 2868	. 2 ⊢ (𝜑 → 𝐺 ∈ MblFn)
39		reex 11330	. . . . . . . . 9 ⊢ ℝ ∈ V
40	39	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ∈ V)
41		ifan 4539	. . . . . . . . . 10 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0)
42		0re 11349	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
43		ifcl 4531	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ)
44	3, 42, 43	sylancl 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ)
45		max1 13355	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0))
46	42, 3, 45	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0))
47		elrege0 13625	. . . . . . . . . . . 12 ⊢ (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)))
48	44, 46, 47	sylanbrc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) ∈ (0[,)+∞))
49		0e0icopnf 13629	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,)+∞)
50	49	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,)+∞))
51	48, 50	ifclda 4521	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) ∈ (0[,)+∞))
52	41, 51	eqeltrid 2868	. . . . . . . . 9 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈ (0[,)+∞))
53	52	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈ (0[,)+∞))
54		ifan 4539	. . . . . . . . . 10 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)
55	3	renegcld 11782	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐹‘𝐵) ∈ ℝ)
56		ifcl 4531	. . . . . . . . . . . . 13 ⊢ (( -(𝐹‘𝐵) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ)
57	55, 42, 56	sylancl 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ)
58		max1 13355	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ -(𝐹‘𝐵) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))
59	42, 55, 58	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))
60		elrege0 13625	. . . . . . . . . . . 12 ⊢ (if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)))
61	57, 59, 60	sylanbrc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) ∈ (0[,)+∞))
62	61, 50	ifclda 4521	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) ∈ (0[,)+∞))
63	54, 62	eqeltrid 2868	. . . . . . . . 9 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈ (0[,)+∞))
64	63	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈ (0[,)+∞))
65		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)))
66		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))
67	40, 53, 64, 65, 66	offval2 7745	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))
68	41, 54	oveq12i 7463	. . . . . . . . 9 ⊢ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0))
69		max0add 15520	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝐵) ∈ ℝ → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵)))
70	3, 69	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (abs‘(𝐹‘𝐵)))
71		iftrue 4491	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0))
72	71	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0))
73		iftrue 4491	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))
74	73	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0))
75	72, 74	oveq12d 7469	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) + if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)))
76	70, 75, 13	3eqtr4d 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
77	76	ex 418	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)))
78		00id 11524	. . . . . . . . . . 11 ⊢ (0 + 0) = 0
79		iffalse 4494	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) = 0)
80		iffalse 4494	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0) = 0)
81	79, 80	oveq12d 7469	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = (0 + 0))
82	78, 81, 19	3eqtr4a 2824	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
83	77, 82	pm2.61d1 182	. . . . . . . . 9 ⊢ (𝜑 → (if(𝑥 ∈ 𝐴, if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0), 0) + if(𝑥 ∈ 𝐴, if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
84	68, 83	eqtrid 2810	. . . . . . . 8 ⊢ (𝜑 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))
85	84	mpteq2dv 5205	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)))
86	67, 85	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0)))
87	1, 86	eqtr4id 2817	. . . . 5 ⊢ (𝜑 → 𝐺 = ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))))
88	87	fveq2d 6920	. . . 4 ⊢ (𝜑 → (∫2‘𝐺) = (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))))
89	52	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) ∈ (0[,)+∞))
90	41, 79	eqtrid 2810	. . . . . . 7 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0)
91	18, 90	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0) = 0)
92		ibar 538	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ (𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵))))
93	92	ifbid 4509	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))
94	93	mpteq2ia 5206	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))
95	3, 6	mbfpos 26027	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐹‘𝐵), (𝐹‘𝐵), 0)) ∈ MblFn)
96	94, 95	eqeltrrid 2869	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn)
97	9, 11, 89, 91, 96	mbfss 26022	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∈ MblFn)
98	53	fmpttd 7147	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)):ℝ⟶(0[,)+∞))
99	5	simp2d 1161	. . . . 5 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) ∈ ℝ)
100	63	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) ∈ (0[,)+∞))
101	54, 80	eqtrid 2810	. . . . . . 7 ⊢ (¬ 𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0)
102	18, 101	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0) = 0)
103		ibar 538	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (0 ≤ -(𝐹‘𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵))))
104	103	ifbid 4509	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))
105	104	mpteq2ia 5206	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))
106	3, 6	mbfneg 26026	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝐵)) ∈ MblFn)
107	55, 106	mbfpos 26027	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐹‘𝐵), -(𝐹‘𝐵), 0)) ∈ MblFn)
108	105, 107	eqeltrrid 2869	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn)
109	9, 11, 100, 102, 108	mbfss 26022	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)) ∈ MblFn)
110	64	fmpttd 7147	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)):ℝ⟶(0[,)+∞))
111	5	simp3d 1162	. . . . 5 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0))) ∈ ℝ)
112	97, 98, 99, 109, 110, 111	itg2add 26135	. . . 4 ⊢ (𝜑 → (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0)) ∘f + (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))))
113	88, 112	eqtrd 2798	. . 3 ⊢ (𝜑 → (∫2‘𝐺) = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))))
114	99, 111	readdcld 11377	. . 3 ⊢ (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (𝐹‘𝐵)), (𝐹‘𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(𝐹‘𝐵)), -(𝐹‘𝐵), 0)))) ∈ ℝ)
115	113, 114	eqeltrd 2864	. 2 ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)
116	38, 115	jca 521	1 ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048  ifcif 4485   class class class wbr 5108   ↦ cmpt 5192  dom cdm 5658   ∘ ccom 5662  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451   ∘_f cof 7723  ℂcc 11237  ℝcr 11238  0cc0 11239   + caddc 11242  +∞cpnf 11379   ≤ cle 11383   -cneg 11581  [,)cico 13518  abscabs 15444  –cn→ccncf 25252  volcvol 25839  MblFncmbf 25990  ∫₂citg2 25992  𝐿¹cibl 25993

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cc 10552  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317  ax-addf 11318

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-disj 5076  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7725  df-ofr 7726  df-om 7912  df-1st 8035  df-2nd 8036  df-supp 8215  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-oadd 8518  df-omul 8519  df-er 8755  df-map 8887  df-pm 8888  df-ixp 8964  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9541  df-dju 10019  df-card 10057  df-acn 10060  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-q 13116  df-rp 13161  df-xneg 13281  df-xadd 13282  df-xmul 13283  df-ioo 13520  df-ioc 13521  df-ico 13522  df-icc 13523  df-fz 13680  df-fzo 13829  df-fl 13972  df-seq 14185  df-exp 14245  df-hash 14516  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-clim 15699  df-rlim 15700  df-sum 15898  df-struct 17369  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453  df-plusg 17486  df-mulr 17487  df-starv 17488  df-sca 17489  df-vsca 17490  df-ip 17491  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-hom 17497  df-cco 17498  df-euf 17499  df-rest 17643  df-topn 17644  df-0g 17662  df-gsum 17663  df-topgen 17664  df-pt 17665  df-prds 17668  df-xrs 17724  df-qtop 17729  df-imas 17730  df-xps 17732  df-mre 17806  df-mrc 17807  df-acs 17809  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-submnd 19029  df-mulg 19328  df-cntz 19582  df-cmn 20047  df-psmet 21721  df-xmet 21722  df-met 21723  df-bl 21724  df-mopn 21725  df-cnfld 21730  df-top 23267  df-topon 23284  df-topsp 23306  df-bases 23319  df-cn 23600  df-cnp 23601  df-cmp 23760  df-tx 23936  df-hmeo 24129  df-xms 24694  df-ms 24695  df-tms 24696  df-cncf 25254  df-ovol 25840  df-vol 25841  df-mbf 25995  df-itg1 25996  df-itg2 25997  df-ibl 25998  df-0p 26046

This theorem is used by:  iblabs  26204