sitgclg

Description: Closure of the Bochner integral on simple functions, generic version. See sitgclbn for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018) (Proof shortened by AV, 12-Dec-2019)

	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$
	sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
	sitgclg.g	$⊢ G = Scalar (W)$
	sitgclg.d	$⊢ D = {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}$
	sitgclg.1	$⊢ φ \to W \in TopSp$
	sitgclg.2	$⊢ φ \to W \in CMnd$
	sitgclg.3	$⊢ φ \to Scalar (W) \in ℝExt$
	sitgclg.4	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \underset{˙}{\cdot} x \in B$
Assertion	sitgclg	$⊢ φ \to \int_{ℑ}^{W} F d M \in B$

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		sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
10		sitgclg.g	$⊢ G = Scalar (W)$
11		sitgclg.d	$⊢ D = {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}$
12		sitgclg.1	$⊢ φ \to W \in TopSp$
13		sitgclg.2	$⊢ φ \to W \in CMnd$
14		sitgclg.3	$⊢ φ \to Scalar (W) \in ℝExt$
15		sitgclg.4	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \underset{˙}{\cdot} x \in B$
16	1 2 3 4 5 6 7 8 9	sitgfval	$⊢ φ \to \int_{ℑ}^{W} F d M = \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)$
17		rnexg	$⊢ F \in ℑ_{M}^{W} \to ran F \in V$
18		difexg	$⊢ ran F \in V \to ran F ∖ \{\underset{˙}{0}\} \in V$
19	9 17 18	3syl	$⊢ φ \to ran F ∖ \{\underset{˙}{0}\} \in V$
20		simpl	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to φ$
21	1 2 3 4 5 6 7 8 9	sibfima	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to M (F^{-1} [\{x\}]) \in [0, +∞)$
22	10	fveq2i	$⊢ dist (G) = dist (Scalar (W))$
23	10	fveq2i	$⊢ {Base}_{G} = {Base}_{Scalar (W)}$
24	23 23	xpeq12i	$⊢ {Base}_{G} \times {Base}_{G} = {Base}_{Scalar (W)} \times {Base}_{Scalar (W)}$
25	22 24	reseq12i	$⊢ {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} = {dist (Scalar (W)) ↾}_{({Base}_{Scalar (W)} \times {Base}_{Scalar (W)})}$
26	11 25	eqtri	$⊢ D = {dist (Scalar (W)) ↾}_{({Base}_{Scalar (W)} \times {Base}_{Scalar (W)})}$
27		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
28		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
29	10	fveq2i	$⊢ TopOpen (G) = TopOpen (Scalar (W))$
30	10	fveq2i	$⊢ ℤMod (G) = ℤMod (Scalar (W))$
31	10 14	eqeltrid	$⊢ φ \to G \in ℝExt$
32		rrextdrg	$⊢ G \in ℝExt \to G \in DivRing$
33	31 32	syl	$⊢ φ \to G \in DivRing$
34	10 33	eqeltrrid	$⊢ φ \to Scalar (W) \in DivRing$
35		rrextnrg	$⊢ G \in ℝExt \to G \in NrmRing$
36	31 35	syl	$⊢ φ \to G \in NrmRing$
37	10 36	eqeltrrid	$⊢ φ \to Scalar (W) \in NrmRing$
38		eqid	$⊢ ℤMod (G) = ℤMod (G)$
39	38	rrextnlm	$⊢ G \in ℝExt \to ℤMod (G) \in NrmMod$
40	31 39	syl	$⊢ φ \to ℤMod (G) \in NrmMod$
41	10	fveq2i	$⊢ chr (G) = chr (Scalar (W))$
42		rrextchr	$⊢ G \in ℝExt \to chr (G) = 0$
43	31 42	syl	$⊢ φ \to chr (G) = 0$
44	41 43	eqtr3id	$⊢ φ \to chr (Scalar (W)) = 0$
45		rrextcusp	$⊢ G \in ℝExt \to G \in CUnifSp$
46	31 45	syl	$⊢ φ \to G \in CUnifSp$
47	10 46	eqeltrrid	$⊢ φ \to Scalar (W) \in CUnifSp$
48	10	fveq2i	$⊢ UnifSt (G) = UnifSt (Scalar (W))$
49		eqid	$⊢ {Base}_{G} = {Base}_{G}$
50	49 11	rrextust	$⊢ G \in ℝExt \to UnifSt (G) = metUnif (D)$
51	31 50	syl	$⊢ φ \to UnifSt (G) = metUnif (D)$
52	48 51	eqtr3id	$⊢ φ \to UnifSt (Scalar (W)) = metUnif (D)$
53	26 27 28 29 30 34 37 40 44 47 52	rrhf	$⊢ φ \to ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
54	6	feq1i	$⊢ H : ℝ ⟶ {Base}_{Scalar (W)} \leftrightarrow ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
55	53 54	sylibr	$⊢ φ \to H : ℝ ⟶ {Base}_{Scalar (W)}$
56	55	ffund	$⊢ φ \to Fun H$
57		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
58	55	fdmd	$⊢ φ \to dom H = ℝ$
59	57 58	sseqtrrid	$⊢ φ \to [0, +∞) \subseteq dom H$
60		funfvima2	$⊢ (Fun H \land [0, +∞) \subseteq dom H) \to (M (F^{-1} [\{x\}]) \in [0, +∞) \to H (M (F^{-1} [\{x\}])) \in H [[0, +∞)])$
61	56 59 60	syl2anc	$⊢ φ \to (M (F^{-1} [\{x\}]) \in [0, +∞) \to H (M (F^{-1} [\{x\}])) \in H [[0, +∞)])$
62	20 21 61	sylc	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to H (M (F^{-1} [\{x\}])) \in H [[0, +∞)]$
63		dmmeas	$⊢ M \in ⋃ ran measures \to dom M \in ⋃ ran sigAlgebra$
64	8 63	syl	$⊢ φ \to dom M \in ⋃ ran sigAlgebra$
65	2	fvexi	$⊢ J \in V$
66	65	a1i	$⊢ φ \to J \in V$
67	66	sgsiga	$⊢ φ \to 𝛔 (J) \in ⋃ ran sigAlgebra$
68	3 67	eqeltrid	$⊢ φ \to S \in ⋃ ran sigAlgebra$
69	1 2 3 4 5 6 7 8 9	sibfmbl	$⊢ φ \to F \in (dom M {MblFn}_{μ} S)$
70	64 68 69	mbfmf	$⊢ φ \to F : ⋃ dom M ⟶ ⋃ S$
71	70	frnd	$⊢ φ \to ran F \subseteq ⋃ S$
72	3	unieqi	$⊢ ⋃ S = ⋃ 𝛔 (J)$
73		unisg	$⊢ J \in V \to ⋃ 𝛔 (J) = ⋃ J$
74	65 73	mp1i	$⊢ φ \to ⋃ 𝛔 (J) = ⋃ J$
75	72 74	syl5eq	$⊢ φ \to ⋃ S = ⋃ J$
76	1 2	tpsuni	$⊢ W \in TopSp \to B = ⋃ J$
77	12 76	syl	$⊢ φ \to B = ⋃ J$
78	75 77	eqtr4d	$⊢ φ \to ⋃ S = B$
79	71 78	sseqtrd	$⊢ φ \to ran F \subseteq B$
80	79	ssdifd	$⊢ φ \to ran F ∖ \{\underset{˙}{0}\} \subseteq B ∖ \{\underset{˙}{0}\}$
81	80	sselda	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to x \in (B ∖ \{\underset{˙}{0}\})$
82	81	eldifad	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to x \in B$
83		simp2	$⊢ (φ \land H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \land x \in B) \to H (M (F^{-1} [\{x\}])) \in H [[0, +∞)]$
84		eleq1	$⊢ m = H (M (F^{-1} [\{x\}])) \to (m \in H [[0, +∞)] \leftrightarrow H (M (F^{-1} [\{x\}])) \in H [[0, +∞)])$
85	84	3anbi2d	$⊢ m = H (M (F^{-1} [\{x\}])) \to ((φ \land m \in H [[0, +∞)] \land x \in B) \leftrightarrow (φ \land H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \land x \in B))$
86		oveq1	$⊢ m = H (M (F^{-1} [\{x\}])) \to m \underset{˙}{\cdot} x = H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x$
87	86	eleq1d	$⊢ m = H (M (F^{-1} [\{x\}])) \to (m \underset{˙}{\cdot} x \in B \leftrightarrow H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x \in B)$
88	85 87	imbi12d	$⊢ m = H (M (F^{-1} [\{x\}])) \to (((φ \land m \in H [[0, +∞)] \land x \in B) \to m \underset{˙}{\cdot} x \in B) \leftrightarrow ((φ \land H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \land x \in B) \to H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x \in B))$
89	88 15	vtoclg	$⊢ H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \to ((φ \land H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \land x \in B) \to H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x \in B)$
90	83 89	mpcom	$⊢ (φ \land H (M (F^{-1} [\{x\}])) \in H [[0, +∞)] \land x \in B) \to H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x \in B$
91	20 62 82 90	syl3anc	$⊢ (φ \land x \in (ran F ∖ \{\underset{˙}{0}\})) \to H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x \in B$
92	91	fmpttd	$⊢ φ \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) : ran F ∖ \{\underset{˙}{0}\} ⟶ B$
93		mptexg	$⊢ ran F ∖ \{\underset{˙}{0}\} \in V \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V$
94	19 93	syl	$⊢ φ \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V$
95	4	fvexi	$⊢ \underset{˙}{0} \in V$
96		suppimacnv	$⊢ ((x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in V \land \underset{˙}{0} \in V) \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) supp \underset{˙}{0} = {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
97	94 95 96	sylancl	$⊢ φ \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) supp \underset{˙}{0} = {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
98	1 2 3 4 5 6 7 8 9	sibfrn	$⊢ φ \to ran F \in Fin$
99		cnvimass	$⊢ {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq dom (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)$
100		eqid	$⊢ (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)$
101	100	dmmptss	$⊢ dom (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \subseteq ran F ∖ \{\underset{˙}{0}\}$
102	99 101	sstri	$⊢ {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran F ∖ \{\underset{˙}{0}\}$
103		difss	$⊢ ran F ∖ \{\underset{˙}{0}\} \subseteq ran F$
104	102 103	sstri	$⊢ {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran F$
105		ssfi	$⊢ (ran F \in Fin \land {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \subseteq ran F) \to {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \in Fin$
106	98 104 105	sylancl	$⊢ φ \to {(x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x)}^{-1} [V ∖ \{\underset{˙}{0}\}] \in Fin$
107	97 106	eqeltrd	$⊢ φ \to (x \in (ran F ∖ \{\underset{˙}{0}\}) ⟼ H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) supp \underset{˙}{0} \in Fin$
108	1 4 13 19 92 107	gsumcl2	$⊢ φ \to \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{W}} (H (M (F^{-1} [\{x\}])) \underset{˙}{\cdot} x) \in B$
109	16 108	eqeltrd	$⊢ φ \to \int_{ℑ}^{W} F d M \in B$

Metamath Proof Explorer

Theorem sitgclg

Proof