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 29730 |
. 2
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) |
11 | | sitgclg.2 |
. . 3
⊢ (𝜑 → 𝑊 ∈ CMnd) |
12 | | rnexg 6990 |
. . . 4
⊢ (𝐹 ∈ dom (𝑊sitg𝑀) → ran 𝐹 ∈ V) |
13 | | difexg 4735 |
. . . 4
⊢ (ran
𝐹 ∈ V → (ran
𝐹 ∖ { 0 }) ∈
V) |
14 | 9, 12, 13 | 3syl 18 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ∈
V) |
15 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝜑) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfima 29727 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) |
17 | | sitgclg.d |
. . . . . . . . . . 11
⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) |
18 | | sitgclg.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (Scalar‘𝑊) |
19 | 18 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(dist‘𝐺) =
(dist‘(Scalar‘𝑊)) |
20 | 18 | fveq2i 6106 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘(Scalar‘𝑊)) |
21 | 20, 20 | xpeq12i 5061 |
. . . . . . . . . . . 12
⊢
((Base‘𝐺)
× (Base‘𝐺)) =
((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))) |
22 | 19, 21 | reseq12i 5315 |
. . . . . . . . . . 11
⊢
((dist‘𝐺)
↾ ((Base‘𝐺)
× (Base‘𝐺))) =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
23 | 17, 22 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐷 =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
25 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
26 | 18 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(TopOpen‘𝐺) =
(TopOpen‘(Scalar‘𝑊)) |
27 | 18 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(ℤMod‘𝐺)
= (ℤMod‘(Scalar‘𝑊)) |
28 | | sitgclg.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) |
29 | 18, 28 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ ℝExt ) |
30 | | rrextdrg 29374 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
DivRing) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ DivRing) |
32 | 18, 31 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
DivRing) |
33 | | rrextnrg 29373 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
NrmRing) |
34 | 29, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ NrmRing) |
35 | 18, 34 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
NrmRing) |
36 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ℤMod‘𝐺)
= (ℤMod‘𝐺) |
37 | 36 | rrextnlm 29375 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ ℝExt →
(ℤMod‘𝐺) ∈
NrmMod) |
38 | 29, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℤMod‘𝐺) ∈
NrmMod) |
39 | 18 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(chr‘𝐺) =
(chr‘(Scalar‘𝑊)) |
40 | | rrextchr 29376 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(chr‘𝐺) =
0) |
41 | 29, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (chr‘𝐺) = 0) |
42 | 39, 41 | syl5eqr 2658 |
. . . . . . . . . 10
⊢ (𝜑 →
(chr‘(Scalar‘𝑊)) = 0) |
43 | | rrextcusp 29377 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
CUnifSp) |
44 | 29, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ CUnifSp) |
45 | 18, 44 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
CUnifSp) |
46 | 18 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(UnifSt‘𝐺) =
(UnifSt‘(Scalar‘𝑊)) |
47 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
48 | 47, 17 | rrextust 29380 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(UnifSt‘𝐺) =
(metUnif‘𝐷)) |
49 | 29, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (UnifSt‘𝐺) = (metUnif‘𝐷)) |
50 | 46, 49 | syl5eqr 2658 |
. . . . . . . . . 10
⊢ (𝜑 →
(UnifSt‘(Scalar‘𝑊)) = (metUnif‘𝐷)) |
51 | 23, 24, 25, 26, 27, 32, 35, 38, 42, 45, 50 | rrhf 29370 |
. . . . . . . . 9
⊢ (𝜑 →
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
52 | 6 | feq1i 5949 |
. . . . . . . . 9
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
53 | 51, 52 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) |
54 | | ffun 5961 |
. . . . . . . 8
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) → Fun 𝐻) |
55 | 53, 54 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐻) |
56 | | rge0ssre 12151 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
57 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) → dom 𝐻 = ℝ) |
58 | 53, 57 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐻 = ℝ) |
59 | 56, 58 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → (0[,)+∞) ⊆ dom
𝐻) |
60 | | funfvima2 6397 |
. . . . . . 7
⊢ ((Fun
𝐻 ∧ (0[,)+∞)
⊆ dom 𝐻) →
((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
61 | 55, 59, 60 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
62 | 15, 16, 61 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))) |
63 | | dmmeas 29591 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
64 | 8, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
65 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘𝑊)
∈ V |
66 | 2, 65 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ V |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ V) |
68 | 67 | sgsiga 29532 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
69 | 3, 68 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
70 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfmbl 29724 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) |
71 | 64, 69, 70 | mbfmf 29644 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝑆) |
72 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:∪
dom 𝑀⟶∪ 𝑆
→ ran 𝐹 ⊆ ∪ 𝑆) |
73 | 71, 72 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝑆) |
74 | 3 | unieqi 4381 |
. . . . . . . . . . 11
⊢ ∪ 𝑆 =
∪ (sigaGen‘𝐽) |
75 | | unisg 29533 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
76 | 66, 75 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
77 | 74, 76 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝐽) |
78 | | sitgclg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ TopSp) |
79 | 1, 2 | tpsuni 20553 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
80 | 78, 79 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
81 | 77, 80 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑆 =
𝐵) |
82 | 73, 81 | sseqtrd 3604 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
83 | 82 | ssdifd 3708 |
. . . . . . 7
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 })) |
84 | 83 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
85 | 84 | eldifad 3552 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ 𝐵) |
86 | | simp2 1055 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))) |
87 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 ∈ (𝐻 “ (0[,)+∞)) ↔ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
88 | 87 | 3anbi2d 1396 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) ↔ (𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵))) |
89 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
90 | 89 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝑚 · 𝑥) ∈ 𝐵 ↔ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
91 | 88, 90 | imbi12d 333 |
. . . . . . 7
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ↔ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))) |
92 | | sitgclg.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) |
93 | 91, 92 | vtoclg 3239 |
. . . . . 6
⊢ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) → ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
94 | 86, 93 | mpcom 37 |
. . . . 5
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
95 | 15, 62, 85, 94 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
96 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
97 | 95, 96 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)):(ran 𝐹 ∖ { 0 })⟶𝐵) |
98 | | mptexg 6389 |
. . . . . 6
⊢ ((ran
𝐹 ∖ { 0 }) ∈ V
→ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
99 | 14, 98 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
100 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑊) ∈ V |
101 | 4, 100 | eqeltri 2684 |
. . . . 5
⊢ 0 ∈
V |
102 | | suppimacnv 7193 |
. . . . 5
⊢ (((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 }))) |
103 | 99, 101, 102 | sylancl 693 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 }))) |
104 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfrn 29726 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
105 | | cnvimass 5404 |
. . . . . . 7
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
106 | 96 | dmmptss 5548 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ⊆ (ran 𝐹 ∖ { 0 }) |
107 | 105, 106 | sstri 3577 |
. . . . . 6
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ (ran 𝐹 ∖ { 0 }) |
108 | | difss 3699 |
. . . . . 6
⊢ (ran
𝐹 ∖ { 0 }) ⊆
ran 𝐹 |
109 | 107, 108 | sstri 3577 |
. . . . 5
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹 |
110 | | ssfi 8065 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹) → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈
Fin) |
111 | 104, 109,
110 | sylancl 693 |
. . . 4
⊢ (𝜑 → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈
Fin) |
112 | 103, 111 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) ∈
Fin) |
113 | 1, 4, 11, 14, 97, 112 | gsumcl2 18138 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ 𝐵) |
114 | 10, 113 | eqeltrd 2688 |
1
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) |