Definition df-sitm 34334

Description: Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in ℝ^*, the range structure for this integral is (ℝ^*_𝑠 ↾_s (0[,]+∞)). See definition 2.3.1 of [Bogachev] p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017.)

Assertion

Ref	Expression
df-sitm	⊢ sitm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))))

Distinct variable group:   𝑓,𝑔,𝑚,𝑤

Detailed syntax breakdown of Definition df-sitm

Step	Hyp	Ref	Expression
1		csitm 34331	. 2 class sitm
2		vw	. . 3 setvar 𝑤
3		vm	. . 3 setvar 𝑚
4		cvv 3479	. . 3 class V
5		cmeas 34197	. . . . 5 class measures
6	5	crn 5685	. . . 4 class ran measures
7	6	cuni 4906	. . 3 class ∪ ran measures
8		vf	. . . 4 setvar 𝑓
9		vg	. . . 4 setvar 𝑔
10	2	cv 1538	. . . . . 6 class 𝑤
11	3	cv 1538	. . . . . 6 class 𝑚
12		csitg 34332	. . . . . 6 class sitg
13	10, 11, 12	co 7432	. . . . 5 class (𝑤sitg𝑚)
14	13	cdm 5684	. . . 4 class dom (𝑤sitg𝑚)
15	8	cv 1538	. . . . . 6 class 𝑓
16	9	cv 1538	. . . . . 6 class 𝑔
17		cds 17307	. . . . . . . 8 class dist
18	10, 17	cfv 6560	. . . . . . 7 class (dist‘𝑤)
19	18	cof 7696	. . . . . 6 class ∘f (dist‘𝑤)
20	15, 16, 19	co 7432	. . . . 5 class (𝑓 ∘f (dist‘𝑤)𝑔)
21		cxrs 17546	. . . . . . 7 class ℝ*𝑠
22		cc0 11156	. . . . . . . 8 class 0
23		cpnf 11293	. . . . . . . 8 class +∞
24		cicc 13391	. . . . . . . 8 class [,]
25	22, 23, 24	co 7432	. . . . . . 7 class (0[,]+∞)
26		cress 17275	. . . . . . 7 class ↾s
27	21, 25, 26	co 7432	. . . . . 6 class (ℝ*𝑠 ↾s (0[,]+∞))
28	27, 11, 12	co 7432	. . . . 5 class ((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)
29	20, 28	cfv 6560	. . . 4 class (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))
30	8, 9, 14, 14, 29	cmpo 7434	. . 3 class (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))
31	2, 3, 4, 7, 30	cmpo 7434	. 2 class (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))))
32	1, 31	wceq 1539	1 wff sitm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))))

This definition is referenced by:  sitmval  34352