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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
	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	sitgclg	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 )

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		sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10		sitgclg.g	⊢ 𝐺 = ( Scalar ‘ 𝑊 )
11		sitgclg.d	⊢ 𝐷 = ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
12		sitgclg.1	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
13		sitgclg.2	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
14		sitgclg.3	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt )
15		sitgclg.4	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 )
16	1 2 3 4 5 6 7 8 9	sitgfval	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
17		rnexg	⊢ ( 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) → ran 𝐹 ∈ V )
18		difexg	⊢ ( ran 𝐹 ∈ V → ( ran 𝐹 ∖ { 0 } ) ∈ V )
19	9 17 18	3syl	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ∈ V )
20		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝜑 )
21	1 2 3 4 5 6 7 8 9	sibfima	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
22	10	fveq2i	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ ( Scalar ‘ 𝑊 ) )
23	10	fveq2i	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
24	23 23	xpeq12i	⊢ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) = ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) × ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
25	22 24	reseq12i	⊢ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) = ( ( dist ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) × ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
26	11 25	eqtri	⊢ 𝐷 = ( ( dist ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) × ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
27		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
29	10	fveq2i	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ ( Scalar ‘ 𝑊 ) )
30	10	fveq2i	⊢ ( ℤMod ‘ 𝐺 ) = ( ℤMod ‘ ( Scalar ‘ 𝑊 ) )
31	10 14	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ ℝExt )
32		rrextdrg	⊢ ( 𝐺 ∈ ℝExt → 𝐺 ∈ DivRing )
33	31 32	syl	⊢ ( 𝜑 → 𝐺 ∈ DivRing )
34	10 33	eqeltrrid	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ DivRing )
35		rrextnrg	⊢ ( 𝐺 ∈ ℝExt → 𝐺 ∈ NrmRing )
36	31 35	syl	⊢ ( 𝜑 → 𝐺 ∈ NrmRing )
37	10 36	eqeltrrid	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ NrmRing )
38		eqid	⊢ ( ℤMod ‘ 𝐺 ) = ( ℤMod ‘ 𝐺 )
39	38	rrextnlm	⊢ ( 𝐺 ∈ ℝExt → ( ℤMod ‘ 𝐺 ) ∈ NrmMod )
40	31 39	syl	⊢ ( 𝜑 → ( ℤMod ‘ 𝐺 ) ∈ NrmMod )
41	10	fveq2i	⊢ ( chr ‘ 𝐺 ) = ( chr ‘ ( Scalar ‘ 𝑊 ) )
42		rrextchr	⊢ ( 𝐺 ∈ ℝExt → ( chr ‘ 𝐺 ) = 0 )
43	31 42	syl	⊢ ( 𝜑 → ( chr ‘ 𝐺 ) = 0 )
44	41 43	eqtr3id	⊢ ( 𝜑 → ( chr ‘ ( Scalar ‘ 𝑊 ) ) = 0 )
45		rrextcusp	⊢ ( 𝐺 ∈ ℝExt → 𝐺 ∈ CUnifSp )
46	31 45	syl	⊢ ( 𝜑 → 𝐺 ∈ CUnifSp )
47	10 46	eqeltrrid	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ CUnifSp )
48	10	fveq2i	⊢ ( UnifSt ‘ 𝐺 ) = ( UnifSt ‘ ( Scalar ‘ 𝑊 ) )
49		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
50	49 11	rrextust	⊢ ( 𝐺 ∈ ℝExt → ( UnifSt ‘ 𝐺 ) = ( metUnif ‘ 𝐷 ) )
51	31 50	syl	⊢ ( 𝜑 → ( UnifSt ‘ 𝐺 ) = ( metUnif ‘ 𝐷 ) )
52	48 51	eqtr3id	⊢ ( 𝜑 → ( UnifSt ‘ ( Scalar ‘ 𝑊 ) ) = ( metUnif ‘ 𝐷 ) )
53	26 27 28 29 30 34 37 40 44 47 52	rrhf	⊢ ( 𝜑 → ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
54	6	feq1i	⊢ ( 𝐻 : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
55	53 54	sylibr	⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
56	55	ffund	⊢ ( 𝜑 → Fun 𝐻 )
57		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
58	55	fdmd	⊢ ( 𝜑 → dom 𝐻 = ℝ )
59	57 58	sseqtrrid	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ dom 𝐻 )
60		funfvima2	⊢ ( ( Fun 𝐻 ∧ ( 0 [,) +∞ ) ⊆ dom 𝐻 ) → ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
61	56 59 60	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
62	20 21 61	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) )
63		dmmeas	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra )
64	8 63	syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
65	2	fvexi	⊢ 𝐽 ∈ V
66	65	a1i	⊢ ( 𝜑 → 𝐽 ∈ V )
67	66	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
68	3 67	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
69	1 2 3 4 5 6 7 8 9	sibfmbl	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
70	64 68 69	mbfmf	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝑆 )
71	70	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ∪ 𝑆 )
72	3	unieqi	⊢ ∪ 𝑆 = ∪ ( sigaGen ‘ 𝐽 )
73		unisg	⊢ ( 𝐽 ∈ V → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
74	65 73	mp1i	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
75	72 74	syl5eq	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐽 )
76	1 2	tpsuni	⊢ ( 𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽 )
77	12 76	syl	⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
78	75 77	eqtr4d	⊢ ( 𝜑 → ∪ 𝑆 = 𝐵 )
79	71 78	sseqtrd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
80	79	ssdifd	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ( 𝐵 ∖ { 0 } ) )
81	80	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
82	81	eldifad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
83		simp2	⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) )
84		eleq1	⊢ ( 𝑚 = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ↔ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
85	84	3anbi2d	⊢ ( 𝑚 = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) ) )
86		oveq1	⊢ ( 𝑚 = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( 𝑚 · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) )
87	86	eleq1d	⊢ ( 𝑚 = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( ( 𝑚 · 𝑥 ) ∈ 𝐵 ↔ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ∈ 𝐵 ) )
88	85 87	imbi12d	⊢ ( 𝑚 = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ∈ 𝐵 ) ) )
89	88 15	vtoclg	⊢ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) → ( ( 𝜑 ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ∈ 𝐵 ) )
90	83 89	mpcom	⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ∈ 𝐵 )
91	20 62 82 90	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ∈ 𝐵 )
92	91	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) : ( ran 𝐹 ∖ { 0 } ) ⟶ 𝐵 )
93		mptexg	⊢ ( ( ran 𝐹 ∖ { 0 } ) ∈ V → ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ∈ V )
94	19 93	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ∈ V )
95	4	fvexi	⊢ 0 ∈ V
96		suppimacnv	⊢ ( ( ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) supp 0 ) = ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) )
97	94 95 96	sylancl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) supp 0 ) = ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) )
98	1 2 3 4 5 6 7 8 9	sibfrn	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
99		cnvimass	⊢ ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ⊆ dom ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) )
100		eqid	⊢ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) )
101	100	dmmptss	⊢ dom ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ⊆ ( ran 𝐹 ∖ { 0 } )
102	99 101	sstri	⊢ ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ⊆ ( ran 𝐹 ∖ { 0 } )
103		difss	⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
104	102 103	sstri	⊢ ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ⊆ ran 𝐹
105		ssfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ⊆ ran 𝐹 ) → ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ∈ Fin )
106	98 104 105	sylancl	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) “ ( V ∖ { 0 } ) ) ∈ Fin )
107	97 106	eqeltrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) supp 0 ) ∈ Fin )
108	1 4 13 19 92 107	gsumcl2	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ 𝐵 )
109	16 108	eqeltrd	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 )

Metamath Proof Explorer

Theorem sitgclg

Proof