A proper vector subspace of a topological vector space has no interior

Statement

Let [ilmath](X,\mathcal{J},[/ilmath][ilmath]\mathbb{K} [/ilmath][ilmath])[/ilmath] be a topological vector space and let [ilmath](Y,\mathbb{K})[/ilmath] be a vector subspace of [ilmath](X,\mathbb{K})[/ilmath] (so [ilmath]Y\subseteq X[/ilmath]), then[1]:

Proof

Let [ilmath](X,\mathcal{J},\mathbb{K})[/ilmath] and let [ilmath](Y,\mathbb{K})[/ilmath] be a vector subspace of [ilmath](X,\mathbb{K})[/ilmath], so [ilmath]Y\subseteq X[/ilmath]. We have 2 cases:

1. Suppose [ilmath]Y\eq X[/ilmath] - by the nature of logical implication we do not care about the truth or falsity of the RHS and we're done
2. Suppose [ilmath]Y\subset X[/ilmath] - by the nature of logical implication we must show the RHS holds.
• Recall: "For a vector subspace of a topological vector space if there exists a non-empty open set contained in the subspace then the spaces are equal"
• Symbolically: [ilmath](\exists U\in(\mathcal{J}-\{\emptyset\})[U\subseteq Y])\implies X\eq Y[/ilmath]
• Recall also that the contrapositive of an implication is logically equivalent to the original statement, that is:
• [ilmath](A\implies B)\iff(\neg B\implies\neg A)[/ilmath]
• So we use the earlier statement to see:
• [ilmath]\big[(\exists U\in(\mathcal{J}-\{\emptyset\})[U\subseteq Y])\implies X\eq Y\big][/ilmath]
[ilmath]\iff[/ilmath]
[ilmath]\big[X\neq Y\implies(\forall U\in(\mathcal{J}-\{\emptyset\})[U\nsubseteq Y])\big][/ilmath]
• We have [ilmath]X\neq Y[/ilmath] (as [ilmath]Y\subset X[/ilmath] is a proper subset there must be something in [ilmath]X[/ilmath] that is not in [ilmath]Y[/ilmath]
• So we see [ilmath]X\neq Y[/ilmath]
• [ilmath]\implies \forall U\in(\mathcal{J}-\{\emptyset\})[U\nsubseteq Y][/ilmath] - in words, for all non-empty open sets of [ilmath]X[/ilmath], that open set is not contained in [ilmath]Y[/ilmath].
• Recall the definition of interior:
• $\text{Int}(Y):\eq\bigcup_{U\in\{V\in\mathcal{J}\ \vert\ V\subseteq Y\} } U$
• blah blah blah
• We see [ilmath]\text{Int}(Y)\eq\emptyset[/ilmath]