Proof of Linear Subspaces Are Vector Spaces; Intersections

Routine facts about restricted operations and about sums and linear combinations formed in a smaller space are used without comment (Toolkit for AL2). Let $W$ be a linear subspace of $V$. By Linear Subspaces (i), $u+w\in W$ and $\lambda w\in W$ for $u,w\in W$ and $\lambda\in K$. Hence the restrictions of the two operations of $V$ are a binary operation on $W$ and a map from $K\times W$ to $W$, with the same values as the operations of $V$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix)); and $W$ is a set, being a subset of $V$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)).

Since the operations of $W$ have the same values as those of $V$, the conditions Vector Space over a Field (i), Vector Space over a Field (ii), Vector Space over a Field (v), Vector Space over a Field (vi), Vector Space over a Field (vii) and Vector Space over a Field (viii) for $W$ are instances of the same conditions for $V$. For Vector Space over a Field (iii), $0\in W$ and $x+0=x$ for every $x\in W$. For Vector Space over a Field (iv), let $z\in W$ satisfy $x+z=x$ for every $x\in W$; as $0\in W$, we get $z=z+0=0+z=0$. So it suffices to give each $v\in W$ a vector of $W$ whose sum with $v$ is $0$, and $(-1)v$, which lies in $W$, is one:

$$v+(-1)v=v+(-v)=0$$

by Elementary Identities in a Vector Space (iv) and The Zero Vector, Negatives and Differences in a Vector Space (ii). Thus $W$ is a vector space over $K$ by Vector Space over a Field (ix), and since $0$ is its only zero, its zero vector is $0$ (The Zero Vector, Negatives and Differences in a Vector Space (i)). This proves (i).

For intersections, let $I$ and $(W_{i})_{i\in I}$ be as in (ii), and fix $i_{0}\in I$. By Indexed Families of Sets and Their Union, Intersection and Product (iii), $\bigcap_{i\in I}W_{i}\subseteq W_{i_{0}}\subseteq V$, so the intersection is a subset of $V$. It contains $0$, since every $W_{i}$ does; and if $u$ and $w$ lie in every $W_{i}$ and $\lambda\in K$, then $u+w$ and $\lambda w$ lie in every $W_{i}$, by Linear Subspaces (i) for each $W_{i}$. This proves (ii).

The set $\{0\}$ contains $0$, and it is closed under the operations because $0+0=0$ (The Zero Vector, Negatives and Differences in a Vector Space (i)) and $\lambda0=0$ (Elementary Identities in a Vector Space (iii)); so it satisfies Linear Subspaces (i). The space $V$ satisfies it because its operations take values in $V$. This proves (iii).

Finally, let $W$, $n$ and $(w_{1},\dots,w_{n})$ be as in (iv). The identity of $W$ is a map $\iota$ from $W$ to $V$ with $\iota(w)=w$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii), as $W\subseteq V$). By the first paragraph and (i), $\iota$ carries the zero vector of $W$ to $0$ and sums and scalar multiples in $W$ to the corresponding ones in $V$. Applied to the map $i\mapsto\lambda_{i}w_{i}$ on $[n]$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi) therefore shows that $\sum_{i=1}^{n}\lambda_{i}w_{i}$ is the same vector whether it is computed in $W$ or in $V$. Both spans are the sets of these vectors for $(\lambda_{1},\dots,\lambda_{n})\in K^{n}$ (Span of a Finite Family; Spanning Families (ii)), so they are equal; and as the zero vectors of $W$ and $V$ agree, the condition of Linearly Independent and Linearly Dependent Finite Families (i) reads the same in $W$ as in $V$. This proves (iv).