Theorem sitgclg 32609

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

Hypotheses

Ref	Expression
sitgval.b	⊢ 𝐵 = (Base‘𝑊)
sitgval.j	⊢ 𝐽 = (TopOpen‘𝑊)
sitgval.s	⊢ 𝑆 = (sigaGen‘𝐽)
sitgval.0	⊢ 0 = (0g‘𝑊)
sitgval.x	⊢ · = ( ·𝑠 ‘𝑊)
sitgval.h	⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
sitgval.1	⊢ (𝜑 → 𝑊 ∈ 𝑉)
sitgval.2	⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
sibfmbl.1	⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
sitgclg.g	⊢ 𝐺 = (Scalar‘𝑊)
sitgclg.d	⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))
sitgclg.1	⊢ (𝜑 → 𝑊 ∈ TopSp)
sitgclg.2	⊢ (𝜑 → 𝑊 ∈ CMnd)
sitgclg.3	⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
sitgclg.4	⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵)

Assertion

Ref	Expression
sitgclg	⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)

Distinct variable groups:   𝐵,𝑚   𝑥,𝐹   𝑚,𝐻   𝑥,𝑚,𝑀   𝑆,𝑚   𝑚,𝑊,𝑥   0 ,𝑚,𝑥   · ,𝑚   𝜑,𝑥   𝑥,𝐵   𝑚,𝐹   𝑚,𝐺   𝜑,𝑚

Allowed substitution hints:   𝐷(𝑥,𝑚)   𝑆(𝑥)   · (𝑥)   𝐺(𝑥)   𝐻(𝑥)   𝐽(𝑥,𝑚)   𝑉(𝑥,𝑚)

Proof of Theorem sitgclg

Step	Hyp	Ref	Expression
1		sitgval.b	. . 3 ⊢ 𝐵 = (Base‘𝑊)
2		sitgval.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝑊)
3		sitgval.s	. . 3 ⊢ 𝑆 = (sigaGen‘𝐽)
4		sitgval.0	. . 3 ⊢ 0 = (0g‘𝑊)
5		sitgval.x	. . 3 ⊢ · = ( ·𝑠 ‘𝑊)
6		sitgval.h	. . 3 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
7		sitgval.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝑉)
8		sitgval.2	. . 3 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
9		sibfmbl.1	. . 3 ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
10	1, 2, 3, 4, 5, 6, 7, 8, 9	sitgfval 32608	. 2 ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))))
11		sitgclg.2	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
12		rnexg 7819	. . . 4 ⊢ (𝐹 ∈ dom (𝑊sitg𝑀) → ran 𝐹 ∈ V)
13		difexg 5271	. . . 4 ⊢ (ran 𝐹 ∈ V → (ran 𝐹 ∖ { 0 }) ∈ V)
14	9, 12, 13	3syl 18	. . 3 ⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ∈ V)
15		simpl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝜑)
16	1, 2, 3, 4, 5, 6, 7, 8, 9	sibfima 32605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞))
17		sitgclg.d	. . . . . . . . . . 11 ⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))
18		sitgclg.g	. . . . . . . . . . . . 13 ⊢ 𝐺 = (Scalar‘𝑊)
19	18	fveq2i 6828	. . . . . . . . . . . 12 ⊢ (dist‘𝐺) = (dist‘(Scalar‘𝑊))
20	18	fveq2i 6828	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) = (Base‘(Scalar‘𝑊))
21	20, 20	xpeq12i 5648	. . . . . . . . . . . 12 ⊢ ((Base‘𝐺) × (Base‘𝐺)) = ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊)))
22	19, 21	reseq12i 5921	. . . . . . . . . . 11 ⊢ ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
23	17, 22	eqtri 2764	. . . . . . . . . 10 ⊢ 𝐷 = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
24		eqid 2736	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
25		eqid 2736	. . . . . . . . . 10 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	18	fveq2i 6828	. . . . . . . . . 10 ⊢ (TopOpen‘𝐺) = (TopOpen‘(Scalar‘𝑊))
27	18	fveq2i 6828	. . . . . . . . . 10 ⊢ (ℤMod‘𝐺) = (ℤMod‘(Scalar‘𝑊))
28		sitgclg.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
29	18, 28	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ ℝExt )
30		rrextdrg 32250	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ ℝExt → 𝐺 ∈ DivRing)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ DivRing)
32	18, 31	eqeltrrid 2842	. . . . . . . . . 10 ⊢ (𝜑 → (Scalar‘𝑊) ∈ DivRing)
33		rrextnrg 32249	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ ℝExt → 𝐺 ∈ NrmRing)
34	29, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ NrmRing)
35	18, 34	eqeltrrid 2842	. . . . . . . . . 10 ⊢ (𝜑 → (Scalar‘𝑊) ∈ NrmRing)
36		eqid 2736	. . . . . . . . . . . 12 ⊢ (ℤMod‘𝐺) = (ℤMod‘𝐺)
37	36	rrextnlm 32251	. . . . . . . . . . 11 ⊢ (𝐺 ∈ ℝExt → (ℤMod‘𝐺) ∈ NrmMod)
38	29, 37	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ℤMod‘𝐺) ∈ NrmMod)
39	18	fveq2i 6828	. . . . . . . . . . 11 ⊢ (chr‘𝐺) = (chr‘(Scalar‘𝑊))
40		rrextchr 32252	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ ℝExt → (chr‘𝐺) = 0)
41	29, 40	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (chr‘𝐺) = 0)
42	39, 41	eqtr3id 2790	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘(Scalar‘𝑊)) = 0)
43		rrextcusp 32253	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ ℝExt → 𝐺 ∈ CUnifSp)
44	29, 43	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ CUnifSp)
45	18, 44	eqeltrrid 2842	. . . . . . . . . 10 ⊢ (𝜑 → (Scalar‘𝑊) ∈ CUnifSp)
46	18	fveq2i 6828	. . . . . . . . . . 11 ⊢ (UnifSt‘𝐺) = (UnifSt‘(Scalar‘𝑊))
47		eqid 2736	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) = (Base‘𝐺)
48	47, 17	rrextust 32256	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ ℝExt → (UnifSt‘𝐺) = (metUnif‘𝐷))
49	29, 48	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (UnifSt‘𝐺) = (metUnif‘𝐷))
50	46, 49	eqtr3id 2790	. . . . . . . . . 10 ⊢ (𝜑 → (UnifSt‘(Scalar‘𝑊)) = (metUnif‘𝐷))
51	23, 24, 25, 26, 27, 32, 35, 38, 42, 45, 50	rrhf 32246	. . . . . . . . 9 ⊢ (𝜑 → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
52	6	feq1i 6642	. . . . . . . . 9 ⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔ (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
53	51, 52	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊)))
54	53	ffund 6655	. . . . . . 7 ⊢ (𝜑 → Fun 𝐻)
55		rge0ssre 13289	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
56	53	fdmd 6662	. . . . . . . 8 ⊢ (𝜑 → dom 𝐻 = ℝ)
57	55, 56	sseqtrrid 3985	. . . . . . 7 ⊢ (𝜑 → (0[,)+∞) ⊆ dom 𝐻)
58		funfvima2 7163	. . . . . . 7 ⊢ ((Fun 𝐻 ∧ (0[,)+∞) ⊆ dom 𝐻) → ((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
59	54, 57, 58	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
60	15, 16, 59	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))
61		dmmeas 32467	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
62	8, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra)
63	2	fvexi 6839	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
64	63	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ V)
65	64	sgsiga 32408	. . . . . . . . . . . 12 ⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra)
66	3, 65	eqeltrid 2841	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
67	1, 2, 3, 4, 5, 6, 7, 8, 9	sibfmbl 32602	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆))
68	62, 66, 67	mbfmf 32520	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝑆)
69	68	frnd 6659	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝑆)
70	3	unieqi 4865	. . . . . . . . . . 11 ⊢ ∪ 𝑆 = ∪ (sigaGen‘𝐽)
71		unisg 32409	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽)
72	63, 71	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽)
73	70, 72	eqtrid 2788	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝐽)
74		sitgclg.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ TopSp)
75	1, 2	tpsuni 22191	. . . . . . . . . . 11 ⊢ (𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽)
76	74, 75	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
77	73, 76	eqtr4d 2779	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 = 𝐵)
78	69, 77	sseqtrd 3972	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
79	78	ssdifd 4087	. . . . . . 7 ⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }))
80	79	sselda 3932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 }))
81	80	eldifad 3910	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ 𝐵)
82		simp2 1136	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))
83		eleq1 2824	. . . . . . . . 9 ⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 ∈ (𝐻 “ (0[,)+∞)) ↔ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
84	83	3anbi2d 1440	. . . . . . . 8 ⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) ↔ (𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵)))
85		oveq1 7344	. . . . . . . . 9 ⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))
86	85	eleq1d 2821	. . . . . . . 8 ⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝑚 · 𝑥) ∈ 𝐵 ↔ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))
87	84, 86	imbi12d 344	. . . . . . 7 ⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ↔ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)))
88		sitgclg.4	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵)
89	87, 88	vtoclg 3514	. . . . . 6 ⊢ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) → ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))
90	82, 89	mpcom 38	. . . . 5 ⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)
91	15, 60, 81, 90	syl3anc 1370	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)
92	91	fmpttd 7045	. . 3 ⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)):(ran 𝐹 ∖ { 0 })⟶𝐵)
93		mptexg 7153	. . . . . 6 ⊢ ((ran 𝐹 ∖ { 0 }) ∈ V → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V)
94	14, 93	syl 17	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V)
95	4	fvexi 6839	. . . . 5 ⊢ 0 ∈ V
96		suppimacnv 8060	. . . . 5 ⊢ (((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })))
97	94, 95, 96	sylancl 586	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })))
98	1, 2, 3, 4, 5, 6, 7, 8, 9	sibfrn 32604	. . . . 5 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
99		cnvimass 6019	. . . . . . 7 ⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))
100		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))
101	100	dmmptss 6179	. . . . . . 7 ⊢ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ⊆ (ran 𝐹 ∖ { 0 })
102	99, 101	sstri 3941	. . . . . 6 ⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ (ran 𝐹 ∖ { 0 })
103		difss 4078	. . . . . 6 ⊢ (ran 𝐹 ∖ { 0 }) ⊆ ran 𝐹
104	102, 103	sstri 3941	. . . . 5 ⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹
105		ssfi 9038	. . . . 5 ⊢ ((ran 𝐹 ∈ Fin ∧ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹) → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈ Fin)
106	98, 104, 105	sylancl 586	. . . 4 ⊢ (𝜑 → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈ Fin)
107	97, 106	eqeltrd 2837	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) ∈ Fin)
108	1, 4, 11, 14, 92, 107	gsumcl2 19610	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ 𝐵)
109	10, 108	eqeltrd 2837	1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  Vcvv 3441   ∖ cdif 3895   ⊆ wss 3898  {csn 4573  ∪ cuni 4852   ↦ cmpt 5175   × cxp 5618  ^◡ccnv 5619  dom cdm 5620  ran crn 5621   ↾ cres 5622   “ cima 5623  Fun wfun 6473  ⟶wf 6475  ‘cfv 6479  (class class class)co 7337   supp csupp 8047  Fincfn 8804  ℝcr 10971  0cc0 10972  +∞cpnf 11107  (,)cioo 13180  [,)cico 13182  Basecbs 17009  Scalarcsca 17062   ·_𝑠 cvsca 17063  distcds 17068  TopOpenctopn 17229  topGenctg 17245  0_gc0g 17247   Σ_g cgsu 17248  CMndccmn 19481  DivRingcdr 20093  metUnifcmetu 20694  ℤModczlm 20808  chrcchr 20809  TopSpctps 22187  UnifStcuss 23511  CUnifSpccusp 23555  NrmRingcnrg 23841  NrmModcnlm 23842  ℝHomcrrh 32241   ℝExt crrext 32242  sigAlgebracsiga 32374  sigaGencsigagen 32404  measurescmeas 32461  sitgcsitg 32596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-tpos 8112  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-dvds 16063  df-gcd 16301  df-numer 16536  df-denom 16537  df-gz 16728  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-mhm 18527  df-submnd 18528  df-grp 18676  df-minusg 18677  df-sbg 18678  df-mulg 18797  df-subg 18848  df-ghm 18928  df-cntz 19019  df-od 19232  df-cmn 19483  df-abl 19484  df-mgp 19816  df-ur 19833  df-ring 19880  df-cring 19881  df-oppr 19957  df-dvdsr 19978  df-unit 19979  df-invr 20009  df-dvr 20020  df-rnghom 20054  df-drng 20095  df-subrg 20127  df-abv 20183  df-lmod 20231  df-nzr 20635  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-metu 20702  df-cnfld 20704  df-zring 20777  df-zrh 20811  df-zlm 20812  df-chr 20813  df-refld 20916  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-cn 22484  df-cnp 22485  df-haus 22572  df-reg 22573  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-fcls 23198  df-cnext 23317  df-ust 23458  df-utop 23489  df-uss 23514  df-usp 23515  df-ucn 23534  df-cfilu 23545  df-cusp 23556  df-xms 23579  df-ms 23580  df-tms 23581  df-nm 23844  df-ngp 23845  df-nrg 23847  df-nlm 23848  df-cncf 24147  df-cfil 24525  df-cmet 24527  df-cms 24605  df-qqh 32221  df-rrh 32243  df-rrext 32247  df-esum 32294  df-siga 32375  df-sigagen 32405  df-meas 32462  df-mbfm 32516  df-sitg 32597

This theorem is referenced by:  sitgclbn  32610  sitmcl  32618