issibf

Description: The predicate " F is a simple function" relative to the Bochner integral. (Contributed by Thierry Arnoux, 19-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	$⊢ B = {Base}_{W}$
	sitgval.j	$⊢ J = TopOpen (W)$
	sitgval.s	$⊢ S = 𝛔 (J)$
	sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
	sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	sitgval.h	$⊢ H = ℝHom (Scalar (W))$
	sitgval.1	$⊢ φ \to W \in V$
	sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
Assertion	issibf	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow (F \in (dom M {MblFn}_{μ} S) \land ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)))$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$⊢ B = {Base}_{W}$
2		sitgval.j	$⊢ J = TopOpen (W)$
3		sitgval.s	$⊢ S = 𝛔 (J)$
4		sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
5		sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		sitgval.h	$⊢ H = ℝHom (Scalar (W))$
7		sitgval.1	$⊢ φ \to W \in V$
8		sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
9	1 2 3 4 5 6 7 8	sitgval	$⊢ φ \to W sitg M = (f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} ⟼ \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x))$
10	9	dmeqd	$⊢ φ \to ℑ_{M}^{W} = dom (f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} ⟼ \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x))$
11		eqid	$⊢ (f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} ⟼ \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x)) = (f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} ⟼ \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x))$
12	11	dmmpt	$⊢ dom (f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} ⟼ \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x)) = \{f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \| \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V\}$
13	10 12	eqtrdi	$⊢ φ \to ℑ_{M}^{W} = \{f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \| \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V\}$
14	13	eleq2d	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow F \in \{f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \| \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V\})$
15		rneq	$⊢ f = F \to ran f = ran F$
16	15	difeq1d	$⊢ f = F \to ran f ∖ \{\underset{˙}{0}\} = ran F ∖ \{\underset{˙}{0}\}$
17		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
18	17	imaeq1d	$⊢ f = F \to f^{-1} [\{x\}] = F^{-1} [\{x\}]$
19	18	fveq2d	$⊢ f = F \to M (f^{-1} [\{x\}]) = M (F^{-1} [\{x\}])$
20	19	fveq2d	$⊢ f = F \to H (M (f^{-1} [\{x\}])) = H (M (F^{-1} [\{x\}]))$
21	20	oveq1d	$⊢ f = F \to H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x = H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x$
22	16 21	mpteq12dv	$⊢ f = F \to (x \in (ran f ∖ \{\underset{˙}{0}\}) ⟼ H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) = (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)$
23	22	oveq2d	$⊢ f = F \to \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) = \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)$
24	23	eleq1d	$⊢ f = F \to (\underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V \leftrightarrow \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V)$
25	24	elrab	$⊢ F \in \{f \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \| \underset{x \in ran f ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (f^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V\} \leftrightarrow (F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \land \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V)$
26	14 25	bitrdi	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow (F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \land \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V))$
27		ovex	$⊢ \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V$
28	27	biantru	$⊢ F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \leftrightarrow (F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \land \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V)$
29	26 28	bitr4di	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\})$
30		rneq	$⊢ g = F \to ran g = ran F$
31	30	eleq1d	$⊢ g = F \to (ran g \in Fin \leftrightarrow ran F \in Fin)$
32	30	difeq1d	$⊢ g = F \to ran g ∖ \{\underset{˙}{0}\} = ran F ∖ \{\underset{˙}{0}\}$
33		cnveq	$⊢ g = F \to g^{-1} = F^{-1}$
34	33	imaeq1d	$⊢ g = F \to g^{-1} [\{x\}] = F^{-1} [\{x\}]$
35	34	fveq2d	$⊢ g = F \to M (g^{-1} [\{x\}]) = M (F^{-1} [\{x\}])$
36	35	eleq1d	$⊢ g = F \to (M (g^{-1} [\{x\}]) \in [0, +∞) \leftrightarrow M (F^{-1} [\{x\}]) \in [0, +∞))$
37	32 36	raleqbidv	$⊢ g = F \to (\forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞) \leftrightarrow \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞))$
38	31 37	anbi12d	$⊢ g = F \to ((ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞)) \leftrightarrow (ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)))$
39	38	elrab	$⊢ F \in \{g \in (dom M {MblFn}_{μ} S) \| (ran g \in Fin \land \forall x \in (ran g ∖ \{\underset{˙}{0}\}) M (g^{-1} [\{x\}]) \in [0, +∞))\} \leftrightarrow (F \in (dom M {MblFn}_{μ} S) \land (ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)))$
40	29 39	bitrdi	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow (F \in (dom M {MblFn}_{μ} S) \land (ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞))))$
41		3anass	$⊢ (F \in (dom M {MblFn}_{μ} S) \land ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)) \leftrightarrow (F \in (dom M {MblFn}_{μ} S) \land (ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)))$
42	40 41	bitr4di	$⊢ φ \to (F \in ℑ_{M}^{W} \leftrightarrow (F \in (dom M {MblFn}_{μ} S) \land ran F \in Fin \land \forall x \in (ran F ∖ \{\underset{˙}{0}\}) M (F^{-1} [\{x\}]) \in [0, +∞)))$

Metamath Proof Explorer

Theorem issibf

Proof