How to Formulate this Linear Algebra Fact in a Coordinate Free way? There is a result result given in the last paragraph of pg 15 in Hoffman And Kunze's Linear algebra (2nd Edition) which essentially says that

THEOREM. Let $F_1$ be a subfield of a field $F$.
  If the entries of an $m\times n$ matrix $M$ lie in $F_1$, and $\mathbf b\in F_1^m$, then the system of equations $M\mathbf x=\mathbf b$ has a solution $\mathbf x\in F_1^m$ if and only if it has a solution in $F^m$.

In other words, the theorem says:

THEOREM. Let $F_1$ be a subfield of a field $F$ and $V=F^m$ be a vector space over $F$.
  Let $\mathbf A, \mathbf A_1,\ldots, \mathbf A_n$ be vectors in $V$ each having all of it's entries in $F_1$.
  Let $x_1,\ldots,x_n\in F$ be such that $\sum_{i=1}^{n}x_i\mathbf A_i=\mathbf A$.
  Then there exist $y_1,\ldots,y_n\in F_1$ such that $\sum_{i=1}^{n}y_i\mathbf A_i=\mathbf A$.

I am looking for a "coordinate free" formulation of the above theorem, meaning, I don't want to take $F_1^m$ as my vector space $V$, whose elements are $m$-tuples. I'd like have a finite dimensional vector space $V$ over $F_1$.
Can somebody see how to do that?
Thanks.
 A: Well, let me try. Note that $V$ has both a vector space structure over $F$ and over $F_1$; I'll use terms like $F$-linear and $F_1$-linear to specify about which of them I'm writing in each case. For consistency I'll use $F_1$ also for the vector space $V_1$ (replacement for $F_1^n$), although there's no ambiguity there.
Also note that for convenience I'm making up one name, "field vector extension" ; probably there exists a correct mathematical term, which might be different, for the concept; also I cannot exclude that the term I use is already in use for a different concept.
OK, so let's first define the "field vector extension":

Definition: Given a field $F$ and a subfield $F_1$ of $F$, and given a vector space $V$ over $F$ and a vector space $V_1$ over $F_1$, I call a function $E: V_1\to V$ a "field vector extension" if it has the following properties:

*

*$E$ is $F_1$-linear

*For any set $M\subset V_1$ of $F_1$-linearly independent vectors, the vectors in the image $E(M)$ are $F$-linearly independent.

*The $F$-linear hull of $E(V_1)$ is $V$.


Note that these properties in particular guarantee that the image of any basis of $V_1$ will be a basis of $V$.
Now let us proof the following useful

Lemma: Given vector spaces $V$ over $F$ and $V_1$ over $F_1$ as above, with a "field vector extension" $E: V_1\to V$, there exists for every $F_1$-linear function $M_1:V_1\to V_1$ an unique $F$-linear function $M:V\to V$ such that $E\circ M_1 = M\circ E$.

Proof: Be $\{e_i\}$ a basis of $V_1$, and be $u_i = M_1(e_i)$. Define $M$ to be the $F$-linear map that maps $E(e_i)$ to $E(f_i)$. Since $\{E(e_i\}$ forms a basis of $V$ and a linear map is completely and uniquely defined by the values it takes on a basis, this $F$-linear function $M$ is well-defined and unique. Be $v\in V_1$. Then $v=\sum_i v_ie_i$, and thus by linearity of all involved functions,
$$(E\circ M_1)(v) = \sum_i v_i E(M_1(e_i)) = \sum_i v_i E(u_i) = \sum_i v_i M(E(e_i)) = (M\circ E)(v).$$
Now we are ready to write down the theorem in coordinate-free language:

THEOREM: Be $F$  a field, $F_1$ a subfield of that field, $V_1$ a  finite dimensional vector space over $F_1$, $V$ a finite-dimensional vector space over $F$ and $E$ a "field vector extension" from $V_1$ to $V$. Be further $M_1$ an $F_1$-linear function on $V_1$ and $M$ the corresponding $F$-linear function on $V$. Then the equation $M(x)=E(b)$ has a solution in $V$ if and only if $M_1(x)=b$ has a solution in $V_1$.

