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 34343 |
. 2
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) |
| 11 | | sitgclg.2 |
. . 3
⊢ (𝜑 → 𝑊 ∈ CMnd) |
| 12 | | rnexg 7924 |
. . . 4
⊢ (𝐹 ∈ dom (𝑊sitg𝑀) → ran 𝐹 ∈ V) |
| 13 | | difexg 5329 |
. . . 4
⊢ (ran
𝐹 ∈ V → (ran
𝐹 ∖ { 0 }) ∈
V) |
| 14 | 9, 12, 13 | 3syl 18 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ∈
V) |
| 15 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝜑) |
| 16 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfima 34340 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) |
| 17 | | sitgclg.d |
. . . . . . . . . . 11
⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) |
| 18 | | sitgclg.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (Scalar‘𝑊) |
| 19 | 18 | fveq2i 6909 |
. . . . . . . . . . . 12
⊢
(dist‘𝐺) =
(dist‘(Scalar‘𝑊)) |
| 20 | 18 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘(Scalar‘𝑊)) |
| 21 | 20, 20 | xpeq12i 5713 |
. . . . . . . . . . . 12
⊢
((Base‘𝐺)
× (Base‘𝐺)) =
((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))) |
| 22 | 19, 21 | reseq12i 5995 |
. . . . . . . . . . 11
⊢
((dist‘𝐺)
↾ ((Base‘𝐺)
× (Base‘𝐺))) =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
| 23 | 17, 22 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐷 =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
| 24 | | eqid 2737 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 25 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 26 | 18 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(TopOpen‘𝐺) =
(TopOpen‘(Scalar‘𝑊)) |
| 27 | 18 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(ℤMod‘𝐺)
= (ℤMod‘(Scalar‘𝑊)) |
| 28 | | sitgclg.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) |
| 29 | 18, 28 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ ℝExt ) |
| 30 | | rrextdrg 34003 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
DivRing) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ DivRing) |
| 32 | 18, 31 | eqeltrrid 2846 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
DivRing) |
| 33 | | rrextnrg 34002 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
NrmRing) |
| 34 | 29, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ NrmRing) |
| 35 | 18, 34 | eqeltrrid 2846 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
NrmRing) |
| 36 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℤMod‘𝐺)
= (ℤMod‘𝐺) |
| 37 | 36 | rrextnlm 34004 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ ℝExt →
(ℤMod‘𝐺) ∈
NrmMod) |
| 38 | 29, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℤMod‘𝐺) ∈
NrmMod) |
| 39 | 18 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(chr‘𝐺) =
(chr‘(Scalar‘𝑊)) |
| 40 | | rrextchr 34005 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(chr‘𝐺) =
0) |
| 41 | 29, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (chr‘𝐺) = 0) |
| 42 | 39, 41 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (𝜑 →
(chr‘(Scalar‘𝑊)) = 0) |
| 43 | | rrextcusp 34006 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
CUnifSp) |
| 44 | 29, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ CUnifSp) |
| 45 | 18, 44 | eqeltrrid 2846 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
CUnifSp) |
| 46 | 18 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(UnifSt‘𝐺) =
(UnifSt‘(Scalar‘𝑊)) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 48 | 47, 17 | rrextust 34009 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(UnifSt‘𝐺) =
(metUnif‘𝐷)) |
| 49 | 29, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (UnifSt‘𝐺) = (metUnif‘𝐷)) |
| 50 | 46, 49 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (𝜑 →
(UnifSt‘(Scalar‘𝑊)) = (metUnif‘𝐷)) |
| 51 | 23, 24, 25, 26, 27, 32, 35, 38, 42, 45, 50 | rrhf 33999 |
. . . . . . . . 9
⊢ (𝜑 →
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
| 52 | 6 | feq1i 6727 |
. . . . . . . . 9
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
| 53 | 51, 52 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) |
| 54 | 53 | ffund 6740 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐻) |
| 55 | | rge0ssre 13496 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
| 56 | 53 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐻 = ℝ) |
| 57 | 55, 56 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝜑 → (0[,)+∞) ⊆ dom
𝐻) |
| 58 | | funfvima2 7251 |
. . . . . . 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 34202 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
| 62 | 8, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
| 63 | 2 | fvexi 6920 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ V |
| 64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ V) |
| 65 | 64 | sgsiga 34143 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
| 66 | 3, 65 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
| 67 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfmbl 34337 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) |
| 68 | 62, 66, 67 | mbfmf 34255 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝑆) |
| 69 | 68 | frnd 6744 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝑆) |
| 70 | 3 | unieqi 4919 |
. . . . . . . . . . 11
⊢ ∪ 𝑆 =
∪ (sigaGen‘𝐽) |
| 71 | | unisg 34144 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
| 72 | 63, 71 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
| 73 | 70, 72 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝐽) |
| 74 | | sitgclg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ TopSp) |
| 75 | 1, 2 | tpsuni 22942 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
| 77 | 73, 76 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑆 =
𝐵) |
| 78 | 69, 77 | sseqtrd 4020 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
| 79 | 78 | ssdifd 4145 |
. . . . . . 7
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 })) |
| 80 | 79 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
| 81 | 80 | eldifad 3963 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ 𝐵) |
| 82 | | simp2 1138 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))) |
| 83 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 ∈ (𝐻 “ (0[,)+∞)) ↔ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
| 84 | 83 | 3anbi2d 1443 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) ↔ (𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵))) |
| 85 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
| 86 | 85 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝑚 · 𝑥) ∈ 𝐵 ↔ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
| 87 | 84, 86 | imbi12d 344 |
. . . . . . 7
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ↔ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))) |
| 88 | | sitgclg.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) |
| 89 | 87, 88 | vtoclg 3554 |
. . . . . 6
⊢ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) → ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
| 90 | 82, 89 | mpcom 38 |
. . . . 5
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
| 91 | 15, 60, 81, 90 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
| 92 | 91 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)):(ran 𝐹 ∖ { 0 })⟶𝐵) |
| 93 | | mptexg 7241 |
. . . . . 6
⊢ ((ran
𝐹 ∖ { 0 }) ∈ V
→ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
| 94 | 14, 93 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
| 95 | 4 | fvexi 6920 |
. . . . 5
⊢ 0 ∈
V |
| 96 | | suppimacnv 8199 |
. . . . 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 34339 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
| 99 | | cnvimass 6100 |
. . . . . . 7
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
| 100 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
| 101 | 100 | dmmptss 6261 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ⊆ (ran 𝐹 ∖ { 0 }) |
| 102 | 99, 101 | sstri 3993 |
. . . . . 6
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ (ran 𝐹 ∖ { 0 }) |
| 103 | | difss 4136 |
. . . . . 6
⊢ (ran
𝐹 ∖ { 0 }) ⊆
ran 𝐹 |
| 104 | 102, 103 | sstri 3993 |
. . . . 5
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹 |
| 105 | | ssfi 9213 |
. . . . 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 2841 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) ∈
Fin) |
| 108 | 1, 4, 11, 14, 92, 107 | gsumcl2 19932 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ 𝐵) |
| 109 | 10, 108 | eqeltrd 2841 |
1
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) |