Given two solutions to a second-order homogeneous linear DE, how to show they form a basis for the solution set?

Question

Define functions $f_1,f_2 : \mathbb{R} \rightarrow \mathbb{R}$ by asserting that for all $x \in \mathbb{R}$ it holds that: $$f_1(x) = e^{2x}\cos x, f_2(x) = e^{2x}\sin x.$$

Also, define a set $$F = \{f : \mathbb{R} \rightarrow \mathbb{R}\,|\,f''-4f'+5f=0\}.$$

It is easy to see that for all $i \in \{1,2\}$ it holds that $f_i \in F$. How can I show that $\{f_1,f_2\}$ is a basis for $F$?

Edit: Here's an incomplete attempt at a proof. The starred lines (namely, 2 and 5) are the ones I need help with.

1. Let $F' = \{c_1 f_1 + c_2 f_2 \,|\,c_1,c_2 \in \mathbb{R}\}$.
2. Prove that $\{f_1,f_2\}$ are linearly independent.*
3. Conclude that $\{f_1,f_2\}$ is a basis for $F'$, and therefore that that $\mathrm{dim}(F')=2$.
4. Prove that $F' \subseteq F$. (This is easy.)
5. Use a theorem to show that $\mathrm{dim}(F)=2$.*
6. Conclude that $F'=F$, and therefore that $\{f_1,f_2\}$ is a basis for $F$.

Line 5 is the really interesting one. What's the name of the theorem that tells us that $\mathrm{dim}(F) = 2$?

Edit 2: Line 5 follows from Theorem 3.4 in this document. (Thank you muzzlater.) So all that remains to show is Line 2.

Answer 1

Below is a proof of the uniqueness theorem, using Wronskians and variation of parameters.

Theorem $\ $ If $\rm\:f,g,h\: $ are solutions on an interval I of

$$\rm y'' =\ p\ y' + q\ y,\ \ \ \ p,q\ \ continuous\ on\ I $$

and the Wronskian $\rm\ \ W = g\:h'-g'h \ne 0\:$ for all $\rm\:x\in I$

then $\,\exists\,$ constants $\rm\: c,d\:$ such that $\rm\: f = c\: g + d\: h\:$ on $\rm\,I.$

Proof $\ $ The equations $[0],[1]$ below have unique solution $\rm\:(c,d)\:$ via det $\rm = W \ne 0\:$ on $\rm\,I.$

$\rm[0]\qquad f\ =\ c\: g \: + d\: h $

$\rm[1]\qquad f' =\ c\: g' + d\: h'$

Now $\rm\:q\:[0] + p\:[1]\ $ yields, $ $ on $ $ LHS: $\rm\,\ q\:f+p\:f'\: =\ f'',\ $ similar on RHS below

$\rm[2]\qquad f'' =\ c\: g'' + d\: h''\ $ via RHS: $\rm\ \, q\:g+p\:g'\: =\ g'',\,\ \ q\:h+p\:h'\: =\ h''$

$\rm[3]\qquad 0\ =\ c'\:g \:+ d'\:h\:\ \ $ via $\ \ [0]'-[1]$

$\rm[4]\qquad 0\ =\ c'\:g' + d'\:h'\ \ $ via $\ \ [1]'-[2]$

$[3],[4]\:$ have solution $\rm\:(c',d') = (0,0),\:$ which is unique by $\rm\ det = W = g\:h'-g'\:h \ne 0\:$ on $\rm\,I.\:$ Therefore $\rm\:c,d\:$ are constants. $\ \ $ QED

Answer 2

If you solve ODE to find that functional space $F$, you'll get that all functions of the type $$ f(x) = C_1 f_1(x)+C_2 f_2(x) $$ are solutions, where $C_1$ and $C_2$ are some real constants. On the other hand, if any $f \in F$ can be decomposed as $f(x) = \sum_{i = 1}^N C_i f_i(x)$ (where in general $N$ can be infinity), then $\{f_i(x)\}$ are basis. In your case you have only 2 functions of such a kind, i.e. they are basis.