Metamath Proof Explorer

Theorem 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 ⊢ 0 ˙ = 0 W
sitgval.x ⊢ · ˙ = ⋅ W
sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
sitgval.1 ⊢ φ → W ∈ V
sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
Assertion issibf ⊢ φ → F ∈ ℑ M W ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 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 ⊢ 0 ˙ = 0 W
5 sitgval.x ⊢ · ˙ = ⋅ W
6 sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
7 sitgval.1 ⊢ φ → W ∈ V
8 sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
9 1 2 3 4 5 6 7 8 sitgval ⊢ φ → W sitg M = f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
10 9 dmeqd ⊢ φ → ℑ M W = dom ⁡ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
11 eqid ⊢ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x = f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
12 11 dmmpt ⊢ dom ⁡ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x = f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ | ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x ∈ V
13 10 12 eqtrdi ⊢ φ → ℑ M W = f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ | ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x ∈ V
14 13 eleq2d ⊢ φ → F ∈ ℑ M W ↔ F ∈ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ | ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x ∈ V
15 rneq ⊢ f = F → ran ⁡ f = ran ⁡ F
16 15 difeq1d ⊢ f = F → ran ⁡ f ∖ 0 ˙ = ran ⁡ F ∖ 0 ˙
17 cnveq ⊢ f = F → f -1 = F -1
18 17 imaeq1d ⊢ f = F → f -1 x = F -1 x
19 18 fveq2d ⊢ f = F → M ⁡ f -1 x = M ⁡ F -1 x
20 19 fveq2d ⊢ f = F → H ⁡ M ⁡ f -1 x = H ⁡ M ⁡ F -1 x
21 20 oveq1d ⊢ f = F → H ⁡ M ⁡ f -1 x · ˙ x = H ⁡ M ⁡ F -1 x · ˙ x
22 16 21 mpteq12dv ⊢ f = F → x ∈ ran ⁡ f ∖ 0 ˙ ⟼ H ⁡ M ⁡ f -1 x · ˙ x = x ∈ ran ⁡ F ∖ 0 ˙ ⟼ H ⁡ M ⁡ F -1 x · ˙ x
23 22 oveq2d ⊢ f = F → ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x = ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x
24 23 eleq1d ⊢ f = F → ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x ∈ V ↔ ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
25 24 elrab ⊢ F ∈ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ | ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x ∈ V ↔ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ∧ ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
26 14 25 bitrdi ⊢ φ → F ∈ ℑ M W ↔ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ∧ ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
27 ovex ⊢ ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
28 27 biantru ⊢ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ∧ ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
29 26 28 bitr4di ⊢ φ → F ∈ ℑ M W ↔ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞
30 rneq ⊢ g = F → ran ⁡ g = ran ⁡ F
31 30 eleq1d ⊢ g = F → ran ⁡ g ∈ Fin ↔ ran ⁡ F ∈ Fin
32 30 difeq1d ⊢ g = F → ran ⁡ g ∖ 0 ˙ = ran ⁡ F ∖ 0 ˙
33 cnveq ⊢ g = F → g -1 = F -1
34 33 imaeq1d ⊢ g = F → g -1 x = F -1 x
35 34 fveq2d ⊢ g = F → M ⁡ g -1 x = M ⁡ F -1 x
36 35 eleq1d ⊢ g = F → M ⁡ g -1 x ∈ 0 +∞ ↔ M ⁡ F -1 x ∈ 0 +∞
37 32 36 raleqbidv ⊢ g = F → ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
38 31 37 anbi12d ⊢ g = F → ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
39 38 elrab ⊢ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
40 29 39 bitrdi ⊢ φ → F ∈ ℑ M W ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
41 3anass ⊢ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞ ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
42 40 41 bitr4di ⊢ φ → F ∈ ℑ M W ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞