Definition df-sitm 29720

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𝑚)‘(𝑓 ∘𝑓 (dist‘𝑤)𝑔))))

Distinct variable group:   𝑓,𝑔,𝑚,𝑤

Detailed syntax breakdown of Definition df-sitm

Step	Hyp	Ref	Expression
1		csitm 29717	. 2 class sitm
2		vw	. . 3 setvar 𝑤
3		vm	. . 3 setvar 𝑚
4		cvv 3173	. . 3 class V
5		cmeas 29585	. . . . 5 class measures
6	5	crn 5039	. . . 4 class ran measures
7	6	cuni 4372	. . 3 class ∪ ran measures
8		vf	. . . 4 setvar 𝑓
9		vg	. . . 4 setvar 𝑔
10	2	cv 1474	. . . . . 6 class 𝑤
11	3	cv 1474	. . . . . 6 class 𝑚
12		csitg 29718	. . . . . 6 class sitg
13	10, 11, 12	co 6549	. . . . 5 class (𝑤sitg𝑚)
14	13	cdm 5038	. . . 4 class dom (𝑤sitg𝑚)
15	8	cv 1474	. . . . . 6 class 𝑓
16	9	cv 1474	. . . . . 6 class 𝑔
17		cds 15777	. . . . . . . 8 class dist
18	10, 17	cfv 5804	. . . . . . 7 class (dist‘𝑤)
19	18	cof 6793	. . . . . 6 class ∘𝑓 (dist‘𝑤)
20	15, 16, 19	co 6549	. . . . 5 class (𝑓 ∘𝑓 (dist‘𝑤)𝑔)
21		cxrs 15983	. . . . . . 7 class ℝ*𝑠
22		cc0 9815	. . . . . . . 8 class 0
23		cpnf 9950	. . . . . . . 8 class +∞
24		cicc 12049	. . . . . . . 8 class [,]
25	22, 23, 24	co 6549	. . . . . . 7 class (0[,]+∞)
26		cress 15696	. . . . . . 7 class ↾s
27	21, 25, 26	co 6549	. . . . . 6 class (ℝ*𝑠 ↾s (0[,]+∞))
28	27, 11, 12	co 6549	. . . . 5 class ((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)
29	20, 28	cfv 5804	. . . 4 class (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘𝑓 (dist‘𝑤)𝑔))
30	8, 9, 14, 14, 29	cmpt2 6551	. . 3 class (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘𝑓 (dist‘𝑤)𝑔)))
31	2, 3, 4, 7, 30	cmpt2 6551	. 2 class (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘𝑓 (dist‘𝑤)𝑔))))
32	1, 31	wceq 1475	1 wff sitm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑚)‘(𝑓 ∘𝑓 (dist‘𝑤)𝑔))))

This definition is referenced by:  sitmval  29738