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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
Assertion	issibf	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9	1 2 3 4 5 6 7 8	sitgval	⊢ ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
10	9	dmeqd	⊢ ( 𝜑 → dom ( 𝑊 sitg 𝑀 ) = dom ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
11		eqid	⊢ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
12	11	dmmpt	⊢ dom ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) = { 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∣ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V }
13	10 12	eqtrdi	⊢ ( 𝜑 → dom ( 𝑊 sitg 𝑀 ) = { 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∣ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V } )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ 𝐹 ∈ { 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∣ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V } ) )
15		rneq	⊢ ( 𝑓 = 𝐹 → ran 𝑓 = ran 𝐹 )
16	15	difeq1d	⊢ ( 𝑓 = 𝐹 → ( ran 𝑓 ∖ { 0 } ) = ( ran 𝐹 ∖ { 0 } ) )
17		cnveq	⊢ ( 𝑓 = 𝐹 → ^◡ 𝑓 = ^◡ 𝐹 )
18	17	imaeq1d	⊢ ( 𝑓 = 𝐹 → ( ^◡ 𝑓 “ { 𝑥 } ) = ( ^◡ 𝐹 “ { 𝑥 } ) )
19	18	fveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
20	19	fveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) )
21	20	oveq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) )
22	16 21	mpteq12dv	⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
23	22	oveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
24	23	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V ↔ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V ) )
25	24	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∣ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V } ↔ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∧ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V ) )
26	14 25	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∧ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V ) ) )
27		ovex	⊢ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V
28	27	biantru	⊢ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↔ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ∧ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V ) )
29	26 28	bitr4di	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ) )
30		rneq	⊢ ( 𝑔 = 𝐹 → ran 𝑔 = ran 𝐹 )
31	30	eleq1d	⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
32	30	difeq1d	⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∖ { 0 } ) = ( ran 𝐹 ∖ { 0 } ) )
33		cnveq	⊢ ( 𝑔 = 𝐹 → ^◡ 𝑔 = ^◡ 𝐹 )
34	33	imaeq1d	⊢ ( 𝑔 = 𝐹 → ( ^◡ 𝑔 “ { 𝑥 } ) = ( ^◡ 𝐹 “ { 𝑥 } ) )
35	34	fveq2d	⊢ ( 𝑔 = 𝐹 → ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
36	35	eleq1d	⊢ ( 𝑔 = 𝐹 → ( ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
37	32 36	raleqbidv	⊢ ( 𝑔 = 𝐹 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
38	31 37	anbi12d	⊢ ( 𝑔 = 𝐹 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
39	38	elrab	⊢ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
40	29 39	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) ) )
41		3anass	⊢ ( ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
42	40 41	bitr4di	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )

Metamath Proof Explorer

Theorem issibf

Proof