avewright/proofwiki-math huggingface dataset:
Theorem: Generalized Sum Restricted to Non-zero Summands/Necessary Condition

Let $G$ be a commutative topological semigroup with identity $0_G$.
Let $\family{g }_{i \in I}$ be an indexed family of elements of $G$.
Let $J = \set{i \in I : g_i \ne 0_G}$
Let $h \in G$.
Let the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converge to $h$.
Then:
:the generalized sum $\ds \sum_{j \mathop \in J} g_j$ converges to $h$

Proof:
Let $U \subseteq G$ be an open subset of $G$ such that $h \in U$.
By definition of convergent net:
:$(1) \quad \exists F \subseteq I : F \ne \O : \forall E \subseteq I : E \supseteq F \implies \ds \sum_{i \mathop \in E} g_i \in U$ 
where $\ds \sum_{i \mathop \in E} g_i$ is the summation over $E$.
Let:
:$F'= F \cap J$
From Set Difference and Intersection form Partition:
:$F = F' \cup F \setminus J$
Let $E' \subseteq J$:
:$E' \supseteq F'$
We have:
:$E' \cap F \setminus J = \O$
Let:
:$E = E' \cup F \setminus J$
From Set Union Preserves Subsets:
:$E \supseteq F$
From $(1)$:
:$\ds \sum_{i \mathop \in E} g_i \in U$
==== Case : $F \setminus J = \O$ ====
Let:
:$F \setminus J = \O$
From Union with Empty Set:
:$E = E'$
Hence:
:$\ds \sum_{i \mathop \in E'} g_i \in U$
{{qed|lemma}}
==== Case : $F \setminus J \ne \O$ ====
Let:
:$F \setminus J \ne \O$
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop \in E} g_i
      | r = \sum_{i \mathop \in E'} g_i + \sum_{i \mathop \in F \setminus J} g_i
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{eqn | r = \sum_{i \mathop \in E'} g_i + \sum_{i \mathop \in F \setminus J} 0_G
      | c = definitions of $F$ and $J$
}}
{{eqn | r = \sum_{i \mathop \in E'} g_i
      | c = {{Defof|Identity (Abstract Algebra)|identity}}
}}
{{end-eqn}}
Hence:
:$\ds \sum_{i \mathop \in E'} g_i \in U$
{{qed|lemma}}
In either case:
:$\ds \sum_{i \mathop \in E'} g_i \in U$
Since $U$ was arbitrary, it follows that  $\ds \sum_{j \mathop \in J} g_j$ converges to $h$ by definition.
Theorem: Generalized Sum Restricted to Non-zero Summands/Sufficient Condition

Let $G$ be a commutative topological semigroup with identity $0_G$.
Let $\family{g }_{i \in I}$ be an indexed family of elements of $G$.
Let $J = \set{i \in I : g_i \ne 0_G}$
Let $h \in G$.
Let the generalized sum $\ds \sum_{j \mathop \in J} g_j$ converge to $h$.
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converges to $h$.

Proof:
Let $U \subseteq G$ be an open subset of $G$ such that $h \in U$.
By definition of convergent net:
:$(2) \quad \exists F' \subseteq J : F' \ne \O : \forall E' \subseteq J : E' \supseteq F' \implies \ds \sum_{j \mathop \in E'} g_j \in U$ 
where $\ds \sum_{j \mathop \in E'} g_j$ is the summation over $E$.
We have:
:$F' \subseteq J \subseteq I$.
Let $E \subseteq I$:
:$E \supseteq F'$
Let:
:$E' = E \cap J$
From Set Intersection Preserves Subsets and Intersection with Subset is Subset:
:$E' \supseteq F'$
From $(2)$:
:$\ds \sum_{j \mathop \in E'} g_j \in U$
From Set Difference Union Intersection:
:$E = E' \cup E \setminus J$
From Set Difference and Intersection are Disjoint:
:$E' \cap E \setminus J = \O$
==== Case : $E \setminus J = \O$ ====
Let:
:$E \setminus J = \O$
From Union with Empty Set:
:$E = E'$
Hence:
:$\ds \sum_{i \mathop \in E} g_i \in U$
{{qed|lemma}}
==== Case : $E \setminus J \ne \O$ ====
Let:
:$E \setminus J \ne \O$
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop \in E} g_i
      | r = \sum_{i \mathop \in E'} g_i + \sum_{i \mathop \in E \setminus J} g_i
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{eqn | r = \sum_{i \mathop \in E'} g_i + \sum_{i \mathop \in E \setminus J} 0_G
      | c = definitions of $E$ and $J$
}}
{{eqn | r = \sum_{i \mathop \in E'} g_i
      | c = {{Defof|Identity (Abstract Algebra)|identity}}
}}
{{end-eqn}}
Hence:
:$\ds \sum_{i \mathop \in E} g_i \in U$
{{qed|lemma}}
In either case:
:$\ds \sum_{i \mathop \in E} g_i \in U$
Since $U$ was arbitrary, it follows that  $\ds \sum_{i \mathop \in I} g_i$ converges to $h$ by definition.
Theorem: Group of Units of Submonoid is Subgroup

Let $T$ be a monoid.
Let $S$ be a submonoid of $T$.
Let $\map G T$ and $\map G S$ be the groups of units of $T$ and $S$ respectively.
Then $\map G S \subseteq \map G T$ and $\map G S$ is a subgroup of $\map G T$.

Proof:
Let $x \in \map G S$.
Then $x \in S$ and there exists $y \in S$ such that $x y = y x = e$.
Since $S \subseteq T$, we have $y \in T$. 
So $x \in \map G T$.
So we have $\map G S \subseteq \map G T$.
From Group of Units is Group, $\map G S$ is a group. 
So $\map G S$ is a subgroup of $\map G T$.
{{qed}}
Category:Groups of Units
273u8cslw03bfq1b6ypxu2fr3h65ypz
Theorem: Spectrum of Element in Unital Subalgebra

Let $A$ be a unital algebra over $\C$. 
Let $B$ be a unital subalgebra of $A$.
Let $x \in B$.
Let $\map {\sigma_A} x$ and $\map {\sigma_B} x$ be the spectra of $x$ in $A$ and $B$ respectively. 
Then:
:$\map {\sigma_A} x \subseteq \map {\sigma_B} x$

Proof:
Let $\map G A$ and $\map G B$ be the group of units of $A$ and $B$ respectively.
From Group of Units of Submonoid is Subgroup, we have:
:$\map G B \subseteq \map G A$
From Set Complement inverts Subsets, we have:
:$A \setminus \map G A \subseteq A \setminus \map G B$
Then, we have:
{{begin-eqn}}
{{eqn	| l = \map {\sigma_A} x
		| r = \set {\lambda \in \C : \lambda {\mathbf 1}_A - x \in A \setminus \map G A}
		| c = {{Defof|Spectrum (Spectral Theory)}}
}}
{{eqn	| o = \subseteq 
		| r = \set {\lambda \in \C : \lambda {\mathbf 1}_A - x \in A \setminus \map G B}
}}
{{eqn	| r = \set {\lambda \in \C : \lambda {\mathbf 1}_A - x \in B \setminus \map G B}
		| c = since $B$ is a unital subalgebra
}}
{{eqn	| r = \map {\sigma_B} x
		| c = {{Defof|Spectrum (Spectral Theory)}}
}}
{{end-eqn}}
{{qed}}
Category:Spectra (Spectral Theory)
Category:Unital Subalgebras
Category:Spectrum of Element in Unital Subalgebra
hvqs1qtut66k0zxw1gllznufwbz0hc8
Theorem: Intersection of Subalgebras is Subalgebra

Let $K$ be a field.
Let $\struct {A, +, \cdot, \circ}_K$ be an algebra over $K$.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an $I$-indexed family of subalgebras of $A$.
Let:
:$\ds B = \bigcap_{\alpha \mathop \in I} A_\alpha$
Then $B$ is a subalgebra of $A$.

Proof:
From Set of Linear Subspaces is Closed under Intersection, $\struct {B, +, \cdot}_K$ is a vector subspace of $\struct {A, +, \cdot}_K$.
Now let $x, y \in B$.
That is, $x, y \in A_\alpha$ for each $\alpha \in I$.
Since $A_\alpha$ is a subalgebras of $A$ for each $\alpha \in I$, we have:
:$x y \in A_\alpha$ for each $\alpha \in I$.
So $x y \in B$. 
So $B$ is a subalgebra of $A$.
{{qed}}
Category:Algebras over Fields
Category:Set Intersection
az2fu0bkbo6jof72oddwyscmgydzpwc
Theorem: Associator of Associative Algebra is Zero

Let $\struct {A_R, \oplus}$ be an associative algebra.
Let $\sqbrk {a, b, c}$ denote the associator of $a, b, c \in A_R$.
Then:
:$\forall a, b, c \in A_R: \sqbrk {a, b, c} = \mathbf 0_R$

Proof:
{{begin-eqn}}
{{eqn | q = \forall a, b, c \in A_R
      | l = a \oplus \paren {b \oplus c}
      | r = \paren {a \oplus b} \oplus c
      | c = {{Defof|Associative Algebra}}
}}
{{eqn | ll= \leadsto
      | l = a \oplus \paren {b \oplus c} - \paren {a \oplus b} \oplus c
      | r = \mathbf 0_R
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Summation over Union of Disjoint Finite Index Sets

Let $\struct{G, +}$ be a commutative monoid.
Let $I$ and $J$ be disjoint finite indexing sets.
Let $K = I \cup J$.
Let $\family{g_k}_{k \mathop \in K}$ be an indexed family of elements of $G$.
Then:
:$\ds \sum_{k \mathop \in K} g_k = \paren{\sum_{i \mathop \in I} g_i} + \paren{\sum_{j \mathop \in J} g_j}$
where:
:$\ds \sum_{k \mathop \in K} g_k$ is the summation of $g$ over $K$
:$\ds \sum_{i \mathop \in I} g_i$ is the summation of the restriction of $g$ over $I$
:$\ds \sum_{j \mathop \in J} g_j$ is the summation of the restriction of $g$ over $J$

Proof:
Let $\set{i_1, i_2, \ldots, i_n}$ be an enumeration of $I$.
Let $\set{j_1, j_2, \ldots, j_m}$ be an enumeration of $J$.
Let $k: \closedint 1 {n+m}$ be the mapping defined by:
:$k_l = \begin{cases}
i_l & : \text{ if } 1 \le l \le n \\
j_{l-n} & : \text{ if } l > n \\ 
\end{cases}$
From Union of Bijections with Disjoint Domains and Codomains is Bijection
:$\set{k_1, k_2, \ldots, k_{n + m}}$ is an enumeration of $K$
We have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \in K} g_k
      | r = \sum_{l \mathop = 1}^{n \mathop + m} g_{k_l}
      | c = {{Defof|Summation over Finite Index}}
}}
{{eqn | r = \paren{\sum_{l \mathop = 1}^n g_{k_l} } + \paren{\sum_{l \mathop = n \mathop + 1}^{n \mathop + m} g_{k_l} }
      | c = {{MonoidAxiom|1}}
}}
{{eqn | r = \paren{\sum_{l \mathop = 1}^n g_{i_l} } + \paren{\sum_{l \mathop = n \mathop + 1}^{n \mathop + m} g_{j_{l \mathop - n} } }
      | c = definition of $k$
}}
{{eqn | r = \paren{\sum_{l \mathop = 1}^n g_{i_l} } + \paren{\sum_{l \mathop = 1 }^m g_{j_l} }
      | c = re-indexing second summation
}}
{{eqn | r = \paren{\sum_{i \mathop \in I} g_i } + \paren{\sum_{j \mathop \in J} g_j}
      | c = {{Defof|Summation over Finite Index}}
}}
{{end-eqn}}
{{qed}}
Category:Summations
4u70ejrpn8eax4n5bmgoqp4f6alxr5h
Theorem: Unitization of Commutative Algebra over Field is Commutative

Let $K$ be a field.
Let $A$ be a commutative algebra over $K$.
Let $A_+$ be the unitization of $A$.
Then $A_+$ is commutative.

Proof:
Let $\tuple {x, \lambda}, \tuple {y, \mu} \in A_+$. 
Then, we have:
{{begin-eqn}}
{{eqn	| l = \tuple {x, \lambda} \tuple {y, \mu}
		| r = \tuple {x y + \lambda y + \mu x, \lambda \mu}
}}
{{eqn	| r = \tuple {y x + \lambda y + \mu x, \mu \lambda}
		| c = $A$ is commutative, $K$ is a field
}}
{{eqn	| r = \tuple {y, \mu} \tuple {x, \lambda}
}}
{{end-eqn}}
So $A_+$ is commutative.
{{qed}}
Category:Unitizations of Algebras over Fields
6mhrcy499nnc6e1ub7txyx9n6u7jk26
Theorem: Existence of Choice Function for Family of Non-Empty Sets of Natural Numbers

Let $\FF$ be a family of non-empty sets of natural numbers.
Then there exists a choice function for $\FF$.

Proof:
{{ProofWanted|Not clear what axiom we are expected to use to start this.}}
Theorem: Existence of Choice Function for Family of Finite Non-Empty Sets of Real Numbers

Let $\FF$ be a family of finite non-empty sets of real numbers.
Then there exists a choice function for $\FF$.

Proof:
{{ProofWanted|Not clear what axiom we are expected to use to start this.}}
Theorem: Unitization of Algebra over Field preserves Subalgebra Relation

Let $K$ be a field.
Let $A$ be a non-unital commutative algebra over $K$.
Let $B$ be a subalgebra of $A$. 
Let $A_+$ and $B_+$ be the unitizations of $A$ and $B$ respectively.
Then $B_+$ is a unital subalgebra of $A_+$.

Proof:
Let $\struct {x, s}, \tuple {y, t} \in B_+$.
Let $\lambda \in K$.
Then, we have:
:$\tuple {x, s} + \lambda \tuple {y, t} = \tuple {x + \lambda y, s + \lambda t}$
Since $\tuple {x, s}, \tuple {y, t} \in B_+$, we have $x, y \in B$. 
Since $B$ is a subalgebra of $A$, we have that:
:$B$ is a vector subspace of $A$
and hence:
:$x + \lambda y \in B$
Hence, we have:
:$\tuple {x + \lambda y, s + \lambda t} \in B_+$
So, we have:
:$\tuple {x, s} + \lambda \tuple {y, t} \in B_+$
From One-Step Vector Subspace Test, we therefore have that $B_+$ is a vector subspace of $A_+$.
To show that $B_+$ is a  subalgebra of $A_+$, it remains to verify that:
:$\tuple {x, s} \tuple {y, t} \in B_+$ for all $\tuple {x, s}, \tuple {y, t} \in B_+$.
Let $\tuple {x, s}, \tuple {y, t} \in B_+$.
Then $x, y \in B$. 
From the definition of the unitization, we have:
:$\tuple {x, s} \tuple {y, t} = \tuple {x y + s y + t x, s t}$
Since $B$ is a subalgebra of $A$, we have:
:$x y \in B$
Since $B$ is a vector subspace of $A$, we have:
:$x y + s y + t x \in B$
Hence, we have:
:$\tuple {x y + s y + t x, s t} \in B_+$
and so:
:$\tuple {x, s} \tuple {y, t} \in B_+$
We therefore have that $B_+$ is a subalgebra of $A_+$.
It remains to show that $B_+$ is unital.
Since $B$ is a vector subspace of $A$, we have that:
:${\mathbf 0}_A \in B$
Hence, we have:
:$\tuple { {\mathbf 0}_A, 1_K} \in B_+$
From Unitization of Algebra over Field is Unital Algebra over Field, we conclude:
$B_+$ is a unital subalgebra of $A_+$.
{{qed}}
Category:Unitizations of Algebras over Fields
rhvldoo0ppzcfp2kexggcwh3gy2fwas
Theorem: Spectrum of Element in Unital Subalgebra/Corollary

Let $A$ be a non-unital algebra over $\C$. 
Let $B$ be a subalgebra of $A$.
Let $x \in B$.
Let $\map {\sigma_A} x$ and $\map {\sigma_B} x$ be the spectra of $x$ in $A$ and $B$ respectively. 
Then:
:$\map {\sigma_A} x \subseteq \map {\sigma_B} x$

Proof:
Let $A_+$ and $B_+$ be the unitizations of $A$ and $B$ respectively.
From Unitization of Algebra over Field preserves Subalgebra Relation, we have:
:$B_+$ is a unital subalgebra of $A_+$.
From Spectrum of Element in Unital Subalgebra, we have that:
:$\map {\sigma_{A_+} } {\tuple {x, 0} } \subseteq \map {\sigma_{B_+} } {\tuple {x, 0} }$
From the definition of the spectrum in a non-unital algebra, we have:
:$\map {\sigma_{A_+} } {\tuple {x, 0} } = \map {\sigma_A} x$
and:
:$\map {\sigma_{B_+} } {\tuple {x, 0} } = \map {\sigma_B} x$
So, we have:
:$\map {\sigma_A} x \subseteq \map {\sigma_B} x$
{{qed}}
Category:Spectrum of Element in Unital Subalgebra
emkutanpf2jrrj4fefneusm9404q65f
Theorem: Closure of Subalgebra in Normed Algebra is Subalgebra

Let $\GF \in \set {\R, \C}$.
Let $\struct {A, \norm {\, \cdot \,} }$ be a normed algebra over $\GF$.
Let $B$ be a subalgebra of $A$.
Then $B^-$ is a subalgebra of $A$.

Proof:
From Closure of Subspace of Normed Vector Space is Subspace, $B^-$ is a vector subspace of $A$. 
Now let $x, y \in B^-$.
From the definition of a closed set in a normed vector space, there exists sequences $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ valued in $B$ such that:
:$x_n \to x$ and $y_n \to y$.
From Product Rule for Sequence in Normed Algebra, we have:
:$x_n y_n \to x y$
From the definition of closure, we have $x y \in B^-$.
So $B^-$ is a vector subspace of $A$ that is closed under multiplication.
Hence $B^-$ is a subalgebra of $A$.
{{qed}}
Category:Normed Algebras
t61ea2gn0bya5iwz051a9rrgwfwz6rh
Theorem: Maximal Subalgebra in Normed Algebra is Closed

Let $\GF \in \set {\R, \C}$.
Let $\struct {A, \norm {\, \cdot \,} }$ be a normed algebra over $\GF$.
Let $B$ be a subalgebra of $A$ that is maximal with respect to set inclusion.
Then $B$ is closed.

Proof:
From Closure of Subalgebra in Normed Algebra is Subalgebra, the closure $B^-$ of $B$ is a subalgebra with $B \subseteq B^-$.
Since $B$ is maximal with respect to set inclusion, we have that $B = B^-$.
From Set is Closed iff Equals Topological Closure, we conclude that $B$ is closed.
{{qed}}
Category:Normed Algebras
kzkqluu0cepngzv6okn7rwonnvb8o78
Theorem: Existence of Vitali Set implies Subset of Unit Interval with Inner Measure Zero and Outer Measure 1

Let us posit the existence of a Vitali set.
Then there exists a subset of the closed unit interval which has an inner measure of $0$ and an outer measure of $1$.

Proof:
{{ProofWanted|But first we need to know what an inner measure is.}}
Theorem: Maximal Commutative Subalgebra of Unital Algebra is Unital

Let $K$ be a field.
Let $A$ be a unital algebra over $K$.
Let $B$ be a commutative subalgebra of $A$ that is maximal with respect to set inclusion.
Then $B$ is unital.

Proof:
We show that $B + K {\mathbf 1}_A$ is a subalgebra of $A$.
First we show that $B + K {\mathbf 1}_A$ is a vector subspace of $A$.
Let $x + t {\mathbf 1}_A, y + s {\mathbf 1}_A \in B + K {\mathbf 1}_A$ for $x, y \in B$ and $s, t \in K$.
Let $\lambda \in K$.
We have:
:$\paren {x + t {\mathbf 1}_A} + \lambda \paren {y + s {\mathbf 1}_A} = {x + \lambda y} + \paren {t + \lambda s} {\mathbf 1}_A$
Since $B$ is a subalgebra of $A$, it is in particular a vector subspace of $A$.
Then $x + \lambda y \in B$. 
So we have that $\paren {x + t {\mathbf 1}_A} + \lambda \paren {y + s {\mathbf 1}_A} \in B + K {\mathbf 1}_A$.
Hence $B + K {\mathbf 1}_A$ is a vector subspace of $A$.
We now show that $B + K {\mathbf 1}_A$ is closed under multiplication.
Let $x + t {\mathbf 1}_A, y + s {\mathbf 1}_A \in B + K {\mathbf 1}_A$ for $x, y \in B$ and $s, t \in K$.
We have:
:$\paren {x + t {\mathbf 1}_A} \paren {y + s {\mathbf 1}_A} = \paren {x y + s x + t y} + t s {\mathbf 1}_A$
Since $B$ is a subalgebra of $A$, we have $x y \in B$.
Since $B$ is a vector subspace of $A$, we have that $x y + s x + t y \in B$.
So, we have:
:$\paren {x + t {\mathbf 1}_A} \paren {y + s {\mathbf 1}_A} \in B + K {\mathbf 1}_A$
We conclude that $B + K {\mathbf 1}_A$ is a subalgebra of $A$.
Now note that we have:
:$B = B + 0_K {\mathbf 1}_A \subseteq B + K {\mathbf 1}_A$
Since $B$ is maximal with respect to set inclusion, we have:
:$B = B + K {\mathbf 1}_A$
Since ${\mathbf 0}_A \in B$, we have that ${\mathbf 1}_A \in B$.
{{qed}}
Category:Algebras over Fields
Category:Unital Algebras
Category:Commutative Algebras
Category:Subalgebras
st6ryq4v5tc1yxo75wv65d1m95tvgcs
Theorem: Absolute Net Convergence Equivalent to Absolute Convergence

Let $V$ be a Banach space.
Let $\sequence {v_n}_{n \mathop \in \N}$ be a sequence of elements in $V$.
Let $r \in \R_{\mathop \ge 0}$
Then the following two statements are equivalent:
:$(1): \quad$ the generalized sum $\ds \sum \set {v_n: n \in \N}$ is absolutely net convergent to $r$
:$(2): \quad$ the series $\ds \sum_{n \mathop = 1}^\infty v_n$ is absolutely convergent to $r$

Proof:
=== Statement $(1)$ implies Statement $(2)$ ===
Let the generalized sum $\ds \sum \set {v_n: n \in \N}$ be absolutely net convergent to $r$.
{{:Absolute Net Convergence Equivalent to Absolute Convergence/Absolute Net Convergence implies Absolute Convergence}}{{qed|lemma}}
Theorem: Absolute Net Convergence Equivalent to Absolute Convergence/Absolute Net Convergence implies Absolute Convergence

Let $V$ be a Banach space.
Let $\sequence {v_n}_{n \mathop \in \N}$ be a sequence of elements in $V$.
Let $r \in \R_{\mathop \ge 0}$
Let the generalized sum $\ds \sum \set {v_n: n \in \N}$ be absolutely net convergent to $r$.
Then:
:the series $\ds \sum_{n \mathop = 1}^\infty v_n$ is absolutely convergent to $r$.

Proof:
Let $\epsilon \in \R_{\mathop > 0}$.
From Characterization of Convergent Net in Metric Space:
:$(1) \quad \exists F \subset \N: F $ is finite $: \forall E \subseteq \N : E \supseteq F: E$ is finite $\implies \size{\ds \sum_{n \mathop \in E} \norm{v_n} - r} < \epsilon$
Let $N = \max \set{n : v_n \in F}$.
We have:
:$F \subseteq \closedint 0 N$
Let $m \ge N$.
We have:
:$\closedint 0 m \supseteq \closedint 0 N \supseteq F$
From $(1)$:
:$\size{\ds \sum_{n \mathop \in \closedint 0 m} \norm{v_n} - r} < \epsilon$
By definition of summation over finite index:
:$\size{\ds \sum_{n \mathop = 0}^m \norm{v_n} - r} < \epsilon$
Since $m \ge N$ was arbitrary, it follows that:
:$\forall m \ge N : \size{\ds \sum_{n \mathop = 0}^m \norm{v_n} - r} < \epsilon$
Since $\epsilon$ was arbitrary, it follows that the series $\ds \sum_{n \mathop = 1}^\infty v_n$ is absolutely convergent to $r$ by definition.
Theorem: Generalized Hilbert Sequence Space is Metric Space/Well-Defined

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $A$ be the set of all real-valued functions $x : I \to \R$ such that:
:$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
:$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $d_2: A \times A \to \R$ be the real-valued function defined as:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{i \mathop \in I} \paren {x_i- y_i}^2}^{\frac 1 2}$
Then $d_2$ is well-defined.

Proof:
From Characterization of Hausdorff Property in terms of Nets:
:a convergent net in $\R$ has a unique limit. 
To show that $d_2$ is well-defined, it is sufficient to show:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A:$ the generalized sum $\ds \sum_{i \mathop \in I} \paren {x_i - y_i}^2$ converges
Let $x = \family {x_i}, y = \family {y_i} \in A$.
Let $\ds \sum_{i \mathop \in I} x_i^2$ and $\ds \sum_{i \mathop \in I} y_i^2$ converge to $a, b \in \R$ respectively. 
From Characterization of Generalized Hilbert Sequence Space:
:there exists enumeration $J = \set{j_0, j_1, j_2, \ldots}$ of a countable set of $I$:
::$\set{i \in I : x_i \ne 0}, \set{i \in I : y_i \ne 0} \subseteq J$
::$\sequence{x_{j_n}}, \sequence{y_{j_n}} \in \ell^2$
::$\ds \sum_{n \mathop = 0}^\infty x_{j_n}^2 = a, \sum_{n \mathop = 0}^\infty y_{j_n}^2 = b$
From P-Sequence Space with Pointwise Addition and Pointwise Scalar Multiplication on Ring of Sequences forms Vector Space:
:$\sequence{x_{j_n} - y_{j_n}} \in {\ell^2}$
We have:
:$\forall i \in I \setminus J : x_i = y_i = 0$
Hence:
:$\forall i \in I \setminus J : x_i - y_i = 0$
It follows:
:$\set{i : x_i - y_i \ne 0} \subseteq J$
From Characterization of Generalized Hilbert Sequence Space:
:$\family{x_i - y_i}_{i \mathop \in I} \in A$
By definition of $A$:
:the generalized sum $\ds \sum_{i \mathop \in I} \paren {x_i - y_i}^2$ converges
The result follows.
Theorem: Generalized Hilbert Sequence Space is Metric Space/Metric Space Axiom M1

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $A$ be the set of all real-valued functions $x : I \to \R$ such that:
:$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
:$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $d_2: A \times A \to \R$ be the real-valued function defined as:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{i \mathop \in I} \paren {x_i- y_i}^2}^{\frac 1 2}$
Then $d_2$ satisfies {{Metric-space-axiom|1}}.

Proof:
Let $x \in A$.
From Lemma:
:$\exists y \in \ell^2 :$
::$\map {d_2} {x, x} = \map {d_{\ell^2}} {y, y}$
We have:
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, x}
      | r = \map {d_{\ell^2} } {y, y}
      | c = Lemma
}}
{{eqn | r = 0
      | c = {{Metric-space-axiom|4}} applied to $d_{\ell^2}$
}}
{{end-eqn}}
The result follows.
Theorem: Generalized Hilbert Sequence Space is Metric Space/Metric Space Axiom M2

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $A$ be the set of all real-valued functions $x : I \to \R$ such that:
:$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
:$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $d_2: A \times A \to \R$ be the real-valued function defined as:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{i \mathop \in I} \paren {x_i- y_i}^2}^{\frac 1 2}$
Then $d_2$ satisfies {{Metric-space-axiom|2}}.

Proof:
Let $x_1, x_2, x_3 \in A$.
From Lemma:
:$\exists y_1, y_2, y_3 \in \ell^2 : $
::$\forall i, j \in \set{1, 2, 3} : \map {d_2} {x_i, x_j} = \map {d_{\ell^2}} {y_i, y_j}$
We have:
{{begin-eqn}}
{{eqn | l = \map {d_2} {x_1, x_3}
      | r = \map {d_{\ell^2} } {y_1, y_3}
      | c = Lemma
}}
{{eqn | o = \le
      | r = \map {d_{\ell^2} } {y_1, y_2} + \map {d_{\ell^2} } {y_2, y_3}
      | c = {{Metric-space-axiom|2}} applied to $d_{\ell^2}$
}}
{{eqn | r = \map {d_2} {x_1, x_2} + \map {d_2} {x_2, x_3} 
      | c = Lemma
}}
{{end-eqn}}
The result follows.
Theorem: Generalized Hilbert Sequence Space is Metric Space/Metric Space Axiom M3

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $A$ be the set of all real-valued functions $x : I \to \R$ such that:
:$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
:$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $d_2: A \times A \to \R$ be the real-valued function defined as:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{i \mathop \in I} \paren {x_i- y_i}^2}^{\frac 1 2}$
Then $d_2$ satisfies {{Metric-space-axiom|3}}.

Proof:
Let $x_1, x_2 \in A$.
From Lemma:
:$\exists y_1, y_2 \in \ell^2 : $
::$\map {d_2} {x_1, x_2} = \map {d_{\ell^2}} {y_1, y_2}$ and $\map {d_2} {x_2, x_1} = \map {d_{\ell^2}} {y_2, y_1}$
We have:
{{begin-eqn}}
{{eqn | l = \map {d_2} {x_1, x_2}
      | r = \map {d_{\ell^2} } {y_1, y_2}
      | c = Lemma
}}
{{eqn | r = \map {d_{\ell^2} } {y_2, y_1}
      | c = {{Metric-space-axiom|3}} applied to $d_{\ell^2}$
}}
{{eqn | r = \map {d_2} {x_2, x_1} 
      | c = Lemma
}}
{{end-eqn}}
The result follows.