iblabsnclem

	Ref	Expression
Hypotheses	iblabsnc.1	$⊢ (φ \land x \in A) \to B \in V$
	iblabsnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
	iblabsnclem.1	$⊢ G = (x \in ℝ ⟼ if (x \in A, \|F (B)\|, 0))$
	iblabsnclem.2	$⊢ φ \to (x \in A ⟼ F (B)) \in 𝐿^{1}$
	iblabsnclem.3	$⊢ (φ \land x \in A) \to F (B) \in ℝ$
Assertion	iblabsnclem	$⊢ φ \to (G \in MblFn \land \int^{2} (G) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		iblabsnc.1	$⊢ (φ \land x \in A) \to B \in V$
2		iblabsnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3		iblabsnclem.1	$⊢ G = (x \in ℝ ⟼ if (x \in A, \|F (B)\|, 0))$
4		iblabsnclem.2	$⊢ φ \to (x \in A ⟼ F (B)) \in 𝐿^{1}$
5		iblabsnclem.3	$⊢ (φ \land x \in A) \to F (B) \in ℝ$
6	5	iblrelem	$⊢ φ \to ((x \in A ⟼ F (B)) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ F (B)) \in MblFn \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))) \in ℝ))$
7	4 6	mpbid	$⊢ φ \to ((x \in A ⟼ F (B)) \in MblFn \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))) \in ℝ)$
8	7	simp1d	$⊢ φ \to (x \in A ⟼ F (B)) \in MblFn$
9	8 5	mbfdm2	$⊢ φ \to A \in dom vol$
10		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
11	9 10	syl	$⊢ φ \to A \subseteq ℝ$
12		rembl	$⊢ ℝ \in dom vol$
13	12	a1i	$⊢ φ \to ℝ \in dom vol$
14	5	recnd	$⊢ (φ \land x \in A) \to F (B) \in ℂ$
15	14	abscld	$⊢ (φ \land x \in A) \to \|F (B)\| \in ℝ$
16		0re	$⊢ 0 \in ℝ$
17		ifcl	$⊢ (\|F (B)\| \in ℝ \land 0 \in ℝ) \to if (x \in A, \|F (B)\|, 0) \in ℝ$
18	15 16 17	sylancl	$⊢ (φ \land x \in A) \to if (x \in A, \|F (B)\|, 0) \in ℝ$
19		eldifn	$⊢ x \in (ℝ ∖ A) \to \neg x \in A$
20	19	adantl	$⊢ (φ \land x \in (ℝ ∖ A)) \to \neg x \in A$
21		iffalse	$⊢ \neg x \in A \to if (x \in A, \|F (B)\|, 0) = 0$
22	20 21	syl	$⊢ (φ \land x \in (ℝ ∖ A)) \to if (x \in A, \|F (B)\|, 0) = 0$
23		iftrue	$⊢ x \in A \to if (x \in A, \|F (B)\|, 0) = \|F (B)\|$
24	23	mpteq2ia	$⊢ (x \in A ⟼ if (x \in A, \|F (B)\|, 0)) = (x \in A ⟼ \|F (B)\|)$
25	15	fmpttd	$⊢ φ \to (x \in A ⟼ \|F (B)\|) : A ⟶ ℝ$
26	15	adantlr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to \|F (B)\| \in ℝ$
27	26	biantrurd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y < \|F (B)\| \leftrightarrow (\|F (B)\| \in ℝ \land y < \|F (B)\|))$
28	5	adantlr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to F (B) \in ℝ$
29		simplr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to y \in ℝ$
30	28 29	absled	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \leq y \leftrightarrow (- y \leq F (B) \land F (B) \leq y))$
31	30	notbid	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\neg \|F (B)\| \leq y \leftrightarrow \neg (- y \leq F (B) \land F (B) \leq y))$
32	29 26	ltnled	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y < \|F (B)\| \leftrightarrow \neg \|F (B)\| \leq y)$
33		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
34	33	rexrd	$⊢ y \in ℝ \to - y \in ℝ^{*}$
35	34	ad2antlr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to - y \in ℝ^{*}$
36		elioomnf	$⊢ - y \in ℝ^{*} \to (F (B) \in (−∞, - y) \leftrightarrow (F (B) \in ℝ \land F (B) < - y))$
37	35 36	syl	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) \in (−∞, - y) \leftrightarrow (F (B) \in ℝ \land F (B) < - y))$
38	28	biantrurd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) < - y \leftrightarrow (F (B) \in ℝ \land F (B) < - y))$
39	29	renegcld	$⊢ ((φ \land y \in ℝ) \land x \in A) \to - y \in ℝ$
40	28 39	ltnled	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) < - y \leftrightarrow \neg - y \leq F (B))$
41	37 38 40	3bitr2d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) \in (−∞, - y) \leftrightarrow \neg - y \leq F (B))$
42		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
43	42	ad2antlr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to y \in ℝ^{*}$
44		elioopnf	$⊢ y \in ℝ^{*} \to (F (B) \in (y, +∞) \leftrightarrow (F (B) \in ℝ \land y < F (B)))$
45	43 44	syl	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) \in (y, +∞) \leftrightarrow (F (B) \in ℝ \land y < F (B)))$
46	28	biantrurd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y < F (B) \leftrightarrow (F (B) \in ℝ \land y < F (B)))$
47	29 28	ltnled	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y < F (B) \leftrightarrow \neg F (B) \leq y)$
48	45 46 47	3bitr2d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) \in (y, +∞) \leftrightarrow \neg F (B) \leq y)$
49	41 48	orbi12d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((F (B) \in (−∞, - y) \lor F (B) \in (y, +∞)) \leftrightarrow (\neg - y \leq F (B) \lor \neg F (B) \leq y))$
50		ianor	$⊢ \neg (- y \leq F (B) \land F (B) \leq y) \leftrightarrow (\neg - y \leq F (B) \lor \neg F (B) \leq y)$
51	49 50	bitr4di	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((F (B) \in (−∞, - y) \lor F (B) \in (y, +∞)) \leftrightarrow \neg (- y \leq F (B) \land F (B) \leq y))$
52	31 32 51	3bitr4rd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((F (B) \in (−∞, - y) \lor F (B) \in (y, +∞)) \leftrightarrow y < \|F (B)\|)$
53		elioopnf	$⊢ y \in ℝ^{*} \to (\|F (B)\| \in (y, +∞) \leftrightarrow (\|F (B)\| \in ℝ \land y < \|F (B)\|))$
54	43 53	syl	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (y, +∞) \leftrightarrow (\|F (B)\| \in ℝ \land y < \|F (B)\|))$
55	27 52 54	3bitr4rd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (y, +∞) \leftrightarrow (F (B) \in (−∞, - y) \lor F (B) \in (y, +∞)))$
56	55	rabbidva	$⊢ (φ \land y \in ℝ) \to \{x \in A \| \|F (B)\| \in (y, +∞)\} = \{x \in A \| (F (B) \in (−∞, - y) \lor F (B) \in (y, +∞))\}$
57		eqid	$⊢ (x \in A ⟼ \|F (B)\|) = (x \in A ⟼ \|F (B)\|)$
58	57	mptpreima	$⊢ {(x \in A ⟼ \|F (B)\|)}^{-1} [(y, +∞)] = \{x \in A \| \|F (B)\| \in (y, +∞)\}$
59		eqid	$⊢ (x \in A ⟼ F (B)) = (x \in A ⟼ F (B))$
60	59	mptpreima	$⊢ {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] = \{x \in A \| F (B) \in (−∞, - y)\}$
61	59	mptpreima	$⊢ {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] = \{x \in A \| F (B) \in (y, +∞)\}$
62	60 61	uneq12i	$⊢ {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] = \{x \in A \| F (B) \in (−∞, - y)\} \cup \{x \in A \| F (B) \in (y, +∞)\}$
63		unrab	$⊢ \{x \in A \| F (B) \in (−∞, - y)\} \cup \{x \in A \| F (B) \in (y, +∞)\} = \{x \in A \| (F (B) \in (−∞, - y) \lor F (B) \in (y, +∞))\}$
64	62 63	eqtri	$⊢ {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] = \{x \in A \| (F (B) \in (−∞, - y) \lor F (B) \in (y, +∞))\}$
65	56 58 64	3eqtr4g	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ \|F (B)\|)}^{-1} [(y, +∞)] = {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)]$
66		iblmbf	$⊢ (x \in A ⟼ F (B)) \in 𝐿^{1} \to (x \in A ⟼ F (B)) \in MblFn$
67	4 66	syl	$⊢ φ \to (x \in A ⟼ F (B)) \in MblFn$
68	5	fmpttd	$⊢ φ \to (x \in A ⟼ F (B)) : A ⟶ ℝ$
69		mbfima	$⊢ ((x \in A ⟼ F (B)) \in MblFn \land (x \in A ⟼ F (B)) : A ⟶ ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \in dom vol$
70		mbfima	$⊢ ((x \in A ⟼ F (B)) \in MblFn \land (x \in A ⟼ F (B)) : A ⟶ ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol$
71		unmbl	$⊢ ({(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \in dom vol \land {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol) \to {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol$
72	69 70 71	syl2anc	$⊢ ((x \in A ⟼ F (B)) \in MblFn \land (x \in A ⟼ F (B)) : A ⟶ ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol$
73	67 68 72	syl2anc	$⊢ φ \to {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol$
74	73	adantr	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(−∞, - y)] \cup {(x \in A ⟼ F (B))}^{-1} [(y, +∞)] \in dom vol$
75	65 74	eqeltrd	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ \|F (B)\|)}^{-1} [(y, +∞)] \in dom vol$
76		elioomnf	$⊢ y \in ℝ^{*} \to (\|F (B)\| \in (−∞, y) \leftrightarrow (\|F (B)\| \in ℝ \land \|F (B)\| < y))$
77	43 76	syl	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (−∞, y) \leftrightarrow (\|F (B)\| \in ℝ \land \|F (B)\| < y))$
78	26	biantrurd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| < y \leftrightarrow (\|F (B)\| \in ℝ \land \|F (B)\| < y))$
79	28 29	absltd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| < y \leftrightarrow (- y < F (B) \land F (B) < y))$
80	77 78 79	3bitr2d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (−∞, y) \leftrightarrow (- y < F (B) \land F (B) < y))$
81	28	biantrurd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((- y < F (B) \land F (B) < y) \leftrightarrow (F (B) \in ℝ \land (- y < F (B) \land F (B) < y)))$
82	80 81	bitrd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (−∞, y) \leftrightarrow (F (B) \in ℝ \land (- y < F (B) \land F (B) < y)))$
83		3anass	$⊢ (F (B) \in ℝ \land - y < F (B) \land F (B) < y) \leftrightarrow (F (B) \in ℝ \land (- y < F (B) \land F (B) < y))$
84	82 83	bitr4di	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (−∞, y) \leftrightarrow (F (B) \in ℝ \land - y < F (B) \land F (B) < y))$
85		elioo2	$⊢ (- y \in ℝ^{} \land y \in ℝ^{}) \to (F (B) \in (- y, y) \leftrightarrow (F (B) \in ℝ \land - y < F (B) \land F (B) < y))$
86	34 42 85	syl2anc	$⊢ y \in ℝ \to (F (B) \in (- y, y) \leftrightarrow (F (B) \in ℝ \land - y < F (B) \land F (B) < y))$
87	86	ad2antlr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F (B) \in (- y, y) \leftrightarrow (F (B) \in ℝ \land - y < F (B) \land F (B) < y))$
88	84 87	bitr4d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\|F (B)\| \in (−∞, y) \leftrightarrow F (B) \in (- y, y))$
89	88	rabbidva	$⊢ (φ \land y \in ℝ) \to \{x \in A \| \|F (B)\| \in (−∞, y)\} = \{x \in A \| F (B) \in (- y, y)\}$
90	57	mptpreima	$⊢ {(x \in A ⟼ \|F (B)\|)}^{-1} [(−∞, y)] = \{x \in A \| \|F (B)\| \in (−∞, y)\}$
91	59	mptpreima	$⊢ {(x \in A ⟼ F (B))}^{-1} [(- y, y)] = \{x \in A \| F (B) \in (- y, y)\}$
92	89 90 91	3eqtr4g	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ \|F (B)\|)}^{-1} [(−∞, y)] = {(x \in A ⟼ F (B))}^{-1} [(- y, y)]$
93		mbfima	$⊢ ((x \in A ⟼ F (B)) \in MblFn \land (x \in A ⟼ F (B)) : A ⟶ ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(- y, y)] \in dom vol$
94	67 68 93	syl2anc	$⊢ φ \to {(x \in A ⟼ F (B))}^{-1} [(- y, y)] \in dom vol$
95	94	adantr	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ F (B))}^{-1} [(- y, y)] \in dom vol$
96	92 95	eqeltrd	$⊢ (φ \land y \in ℝ) \to {(x \in A ⟼ \|F (B)\|)}^{-1} [(−∞, y)] \in dom vol$
97	25 9 75 96	ismbf2d	$⊢ φ \to (x \in A ⟼ \|F (B)\|) \in MblFn$
98	24 97	eqeltrid	$⊢ φ \to (x \in A ⟼ if (x \in A, \|F (B)\|, 0)) \in MblFn$
99	11 13 18 22 98	mbfss	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|F (B)\|, 0)) \in MblFn$
100	3 99	eqeltrid	$⊢ φ \to G \in MblFn$
101		reex	$⊢ ℝ \in V$
102	101	a1i	$⊢ φ \to ℝ \in V$
103		ifan	$⊢ if ((x \in A \land 0 \leq F (B)), F (B), 0) = if (x \in A, if (0 \leq F (B), F (B), 0), 0)$
104		ifcl	$⊢ (F (B) \in ℝ \land 0 \in ℝ) \to if (0 \leq F (B), F (B), 0) \in ℝ$
105	5 16 104	sylancl	$⊢ (φ \land x \in A) \to if (0 \leq F (B), F (B), 0) \in ℝ$
106		max1	$⊢ (0 \in ℝ \land F (B) \in ℝ) \to 0 \leq if (0 \leq F (B), F (B), 0)$
107	16 5 106	sylancr	$⊢ (φ \land x \in A) \to 0 \leq if (0 \leq F (B), F (B), 0)$
108		elrege0	$⊢ if (0 \leq F (B), F (B), 0) \in [0, +∞) \leftrightarrow (if (0 \leq F (B), F (B), 0) \in ℝ \land 0 \leq if (0 \leq F (B), F (B), 0))$
109	105 107 108	sylanbrc	$⊢ (φ \land x \in A) \to if (0 \leq F (B), F (B), 0) \in [0, +∞)$
110		0e0icopnf	$⊢ 0 \in [0, +∞)$
111	110	a1i	$⊢ (φ \land \neg x \in A) \to 0 \in [0, +∞)$
112	109 111	ifclda	$⊢ φ \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) \in [0, +∞)$
113	103 112	eqeltrid	$⊢ φ \to if ((x \in A \land 0 \leq F (B)), F (B), 0) \in [0, +∞)$
114	113	adantr	$⊢ (φ \land x \in ℝ) \to if ((x \in A \land 0 \leq F (B)), F (B), 0) \in [0, +∞)$
115		ifan	$⊢ if ((x \in A \land 0 \leq - F (B)), - F (B), 0) = if (x \in A, if (0 \leq - F (B), - F (B), 0), 0)$
116	5	renegcld	$⊢ (φ \land x \in A) \to - F (B) \in ℝ$
117		ifcl	$⊢ (- F (B) \in ℝ \land 0 \in ℝ) \to if (0 \leq - F (B), - F (B), 0) \in ℝ$
118	116 16 117	sylancl	$⊢ (φ \land x \in A) \to if (0 \leq - F (B), - F (B), 0) \in ℝ$
119		max1	$⊢ (0 \in ℝ \land - F (B) \in ℝ) \to 0 \leq if (0 \leq - F (B), - F (B), 0)$
120	16 116 119	sylancr	$⊢ (φ \land x \in A) \to 0 \leq if (0 \leq - F (B), - F (B), 0)$
121		elrege0	$⊢ if (0 \leq - F (B), - F (B), 0) \in [0, +∞) \leftrightarrow (if (0 \leq - F (B), - F (B), 0) \in ℝ \land 0 \leq if (0 \leq - F (B), - F (B), 0))$
122	118 120 121	sylanbrc	$⊢ (φ \land x \in A) \to if (0 \leq - F (B), - F (B), 0) \in [0, +∞)$
123	122 111	ifclda	$⊢ φ \to if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) \in [0, +∞)$
124	115 123	eqeltrid	$⊢ φ \to if ((x \in A \land 0 \leq - F (B)), - F (B), 0) \in [0, +∞)$
125	124	adantr	$⊢ (φ \land x \in ℝ) \to if ((x \in A \land 0 \leq - F (B)), - F (B), 0) \in [0, +∞)$
126		eqidd	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) = (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))$
127		eqidd	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)) = (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))$
128	102 114 125 126 127	offval2	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) +_{f} (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)) = (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0) + if ((x \in A \land 0 \leq - F (B)), - F (B), 0))$
129	103 115	oveq12i	$⊢ if ((x \in A \land 0 \leq F (B)), F (B), 0) + if ((x \in A \land 0 \leq - F (B)), - F (B), 0) = if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0)$
130		max0add	$⊢ F (B) \in ℝ \to if (0 \leq F (B), F (B), 0) + if (0 \leq - F (B), - F (B), 0) = \|F (B)\|$
131	5 130	syl	$⊢ (φ \land x \in A) \to if (0 \leq F (B), F (B), 0) + if (0 \leq - F (B), - F (B), 0) = \|F (B)\|$
132		iftrue	$⊢ x \in A \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) = if (0 \leq F (B), F (B), 0)$
133	132	adantl	$⊢ (φ \land x \in A) \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) = if (0 \leq F (B), F (B), 0)$
134		iftrue	$⊢ x \in A \to if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (0 \leq - F (B), - F (B), 0)$
135	134	adantl	$⊢ (φ \land x \in A) \to if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (0 \leq - F (B), - F (B), 0)$
136	133 135	oveq12d	$⊢ (φ \land x \in A) \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (0 \leq F (B), F (B), 0) + if (0 \leq - F (B), - F (B), 0)$
137	23	adantl	$⊢ (φ \land x \in A) \to if (x \in A, \|F (B)\|, 0) = \|F (B)\|$
138	131 136 137	3eqtr4d	$⊢ (φ \land x \in A) \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (x \in A, \|F (B)\|, 0)$
139	138	ex	$⊢ φ \to (x \in A \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (x \in A, \|F (B)\|, 0))$
140		00id	$⊢ 0 + 0 = 0$
141		iffalse	$⊢ \neg x \in A \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) = 0$
142		iffalse	$⊢ \neg x \in A \to if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = 0$
143	141 142	oveq12d	$⊢ \neg x \in A \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = 0 + 0$
144	140 143 21	3eqtr4a	$⊢ \neg x \in A \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (x \in A, \|F (B)\|, 0)$
145	139 144	pm2.61d1	$⊢ φ \to if (x \in A, if (0 \leq F (B), F (B), 0), 0) + if (x \in A, if (0 \leq - F (B), - F (B), 0), 0) = if (x \in A, \|F (B)\|, 0)$
146	129 145	syl5eq	$⊢ φ \to if ((x \in A \land 0 \leq F (B)), F (B), 0) + if ((x \in A \land 0 \leq - F (B)), - F (B), 0) = if (x \in A, \|F (B)\|, 0)$
147	146	mpteq2dv	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0) + if ((x \in A \land 0 \leq - F (B)), - F (B), 0)) = (x \in ℝ ⟼ if (x \in A, \|F (B)\|, 0))$
148	128 147	eqtrd	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) +_{f} (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)) = (x \in ℝ ⟼ if (x \in A, \|F (B)\|, 0))$
149	3 148	eqtr4id	$⊢ φ \to G = (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) +_{f} (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))$
150	149	fveq2d	$⊢ φ \to \int^{2} (G) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) +_{f} (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)))$
151	113	adantr	$⊢ (φ \land x \in A) \to if ((x \in A \land 0 \leq F (B)), F (B), 0) \in [0, +∞)$
152	103 141	syl5eq	$⊢ \neg x \in A \to if ((x \in A \land 0 \leq F (B)), F (B), 0) = 0$
153	20 152	syl	$⊢ (φ \land x \in (ℝ ∖ A)) \to if ((x \in A \land 0 \leq F (B)), F (B), 0) = 0$
154		ibar	$⊢ x \in A \to (0 \leq F (B) \leftrightarrow (x \in A \land 0 \leq F (B)))$
155	154	ifbid	$⊢ x \in A \to if (0 \leq F (B), F (B), 0) = if ((x \in A \land 0 \leq F (B)), F (B), 0)$
156	155	mpteq2ia	$⊢ (x \in A ⟼ if (0 \leq F (B), F (B), 0)) = (x \in A ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))$
157	5 8	mbfpos	$⊢ φ \to (x \in A ⟼ if (0 \leq F (B), F (B), 0)) \in MblFn$
158	156 157	eqeltrrid	$⊢ φ \to (x \in A ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) \in MblFn$
159	11 13 151 153 158	mbfss	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) \in MblFn$
160	114	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) : ℝ ⟶ [0, +∞)$
161	7	simp2d	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) \in ℝ$
162	125	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)) : ℝ ⟶ [0, +∞)$
163	7	simp3d	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))) \in ℝ$
164	159 160 161 162 163	itg2addnc	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0)) +_{f} (x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) + \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)))$
165	150 164	eqtrd	$⊢ φ \to \int^{2} (G) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) + \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0)))$
166	161 163	readdcld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq F (B)), F (B), 0))) + \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - F (B)), - F (B), 0))) \in ℝ$
167	165 166	eqeltrd	$⊢ φ \to \int^{2} (G) \in ℝ$
168	100 167	jca	$⊢ φ \to (G \in MblFn \land \int^{2} (G) \in ℝ)$

Metamath Proof Explorer

Theorem iblabsnclem

Proof