A few isomorphisms between spaces obtained from a complex vector space with antilinear involution; in particular, $[[W]]\cong[W\oplus\overline W]$

Suppose $W$ is a complex vector space with an antilinear involution $\sigma:W\to W$. Set:

$$[W]:=\{w\in W:\sigma(w)=w\},$$

and denote the real vector space obtained by forgetting the complex structure on $W$ and only remembering multiplication by reals by $[[W]]$. Let $V$ be any real vector space. I want to prove the following:

1. $W\cong[W]\otimes_{\mathbb R}\mathbb C$;
2. $[V\otimes\mathbb C]=V$;
3. $[[W]]=[W\oplus\overline W]$;
4. $\dim_{\mathbb R}[W]=\dim_{\mathbb C}W$;
5. $\dim_{\mathbb R}[[W]]=2\dim_{\mathbb C}W$.

Item 2. is relatively simple. The involution on $V\otimes\mathbb C$ is $v\otimes\lambda\mapsto v\otimes\overline\lambda$, so $[V\otimes\mathbb C]=\operatorname{span}_{\mathbb R}\{v\otimes a:v\in V,a\in\mathbb R\}=\operatorname{span}_{\mathbb R}\{v\otimes1:v\in V\}=\{v\otimes1:v\in V\}$, so by identifying $v$ and $v\otimes1$ we have basically identified $[V\otimes\mathbb C]$ with $V$.

Sum-up: The real structure on $V\otimes\mathbb C$ fixes only the $v\otimes1$'s, so $v\mapsto v\otimes1$ is an isomorphism $V\cong[V\otimes\mathbb C]$. And item 2 is done.

My idea for item 1. was to set $v\otimes\lambda\mapsto\lambda v$. That is surely a homomorphism from $[W]\otimes_{\mathbb R}\mathbb C$ to $W$, since it is well-defined and linear on simple tensors, and can thus be extended to combinations of simple tensors by linearity. Proving it is an isomorphism is a horse of another colour though.

Let me try something. Take a basis of $W$ over $\mathbb C$. In fact, take a basis of $[W]$ and complete it to one of $W$.

But wait. Is that even possible? I mean, if I take a basis of $[W]$ over $\mathbb R$, when I view it as a subset of the complex vector space $W$, is it still linearly independent, so that I can complete it to a basis of $W$? Suppose $\sum(a_i+ib_i)e_i=0$. Then $\sum a_ie_i=\sum ib_ie_i$. $\sum ib_ie_i$ should therefore be in $[W]$, but $\sigma(\sum ib_ie_i)=\sum b_i\sigma(ie_i)=\sum b_i(-i)\sigma(e_i)=-\sum ib_ie_i$, so to belong to $[W]$ it must be 0. Hence $\sum a_ie_i=\sum b_ie_i=0$, and by real l.i. of the $e_i$'s we conclude $a_i=b_i=0$, hence $\{e_i\}$ is l.i. over the complex field as well.

Sum-up: Linearly independent over $\mathbb R$ + in $[W]$ $\implies$ linearly independent over $\mathbb C$. This more or less directly follows from $iv\in [W]\iff\sigma(v)=-v$.

Item 4. suggests these $e_i$ might actually span the whole of $W$, over the complex field. Take $w\in W$. We write $w=\frac12(w+\sigma(w))+\frac12(w-\sigma(w))$. The first vector is in $[W]$, the second vector is fixed by $-\sigma$. We can write $\frac12(w+\sigma(w))=\sum a_ie_i$ for some $a_i\in\mathbb R$ since the $e_i$'s are a real basis for $[W]$ and $\frac12(w+\sigma(w))\in[W]$. It is clear that the $ie_i$'s form a linearly independent subset of $i[W]=\{iw:w\in[W]\}$. In fact, they form a basis of said space over $\mathbb R$. That space is a subset of $\operatorname{Fix}(-\sigma)=\{w\in W:\sigma(w)=-w\}$. Let us see if $[W]$ is isomorphic to $\operatorname{Fix}(-\sigma)$, for if so we will conclude $\operatorname{Fix}(-\sigma)$ has $\{ie_i\}$ as a basis. Consider the map $w\mapsto iw$. This is a homomorphism from $[W]$ to $\operatorname{Fix}(-\sigma)$. Let $w\in\operatorname{Fix}(-\sigma)$. Then $-iw\in[W]$, since $\sigma(-iw)=-\sigma(iw)=-(-i)\sigma(w)=i(-w)=-iw$. So $w\mapsto-iw$ can be viewed as a homomorphism from $\operatorname{Fix}(-\sigma)$ to $[W]$. in fact, it is the inverse of $w\mapsto iw$, which is therefore an isomorphism from $[W]$ to $\operatorname{Fix}(-\sigma)$, as we wanted to obtain. This means $\frac12(w-\sigma(w))=it$ for $t\in[W]$, so $\frac12(w-\sigma(w))=i\sum b_ie_i$. So we have proven that $\{e_i\}$ is a complex basis for $W$, and item 4. follows.

Sum-up: $v\mapsto iv$ is an isomorphism from $[W]$ to $\operatorname{Fix}(-\sigma)=\{v:\sigma(v)=-v\}$. $[[W]]=[W]\oplus\operatorname{Fix}(-\sigma)$, as is easy to show. Hence, taking $e_i$ as a basis for $[W]$ over $\mathbb R$, the $ie_i$ span $\operatorname{Fix}(-\sigma)$, so $\{e_i\}$ is a generating set for $W$ over $\mathbb C$, and being l.i. they are a basis. And item 4 is done. (Extra: Indeed, $\{e_i,ie_i\}$ form a real basis (or a basis for $[[W]]$). This gives item 5.)

Let us go back to item 1. now. We have $w=\sum\lambda_ie_i$, and that is the image of $\sum e_i\otimes\lambda_i$ under the homomorphism I defined right after proving item 2. So that homomorphism is surjective.

In the case of finite dimension, surjectivity equates to bijectivity and injectivity, so we'd be done with proving that is an isomorphism. In general, suppose something in $[W]\otimes\mathbb C$ is in the kernel of that morphism, which we will henceforth call $\phi$ whenever we need to refer to it. By finding a real basis $\{e_i\}$ of $[W]$, we can reduce that item to being $\sum e_i\otimes\lambda_i$. This maps to $\sum\lambda_ie_i$. However, as proven above, the $e_i$ are complex-l.i., so that being zero gives $\lambda_i=0$ for all $i$. That, in turns, gives $\sum e_i\otimes\lambda_i=0$, hence proving injectivity.

Sum-up: $v\otimes\lambda\mapsto\lambda v$ is an isomorphism as required by item 1.

So we are left with items 3. and 5. $W$ and $\overline W$ are the same real space, so they have the same real dimension, hence item 5. is a direct consequence of item 3., since $W\oplus\overline W$ has complex dimensione the sum of the dimensione, hence $2\dim_{\mathbb C}W$, and item 4. gives us $\dim_{\mathbb R}[W]=\dim_{\mathbb C}W$ for any complex space with an antilinear involution.

So the question is: how do I obtain item 3.? What is the isomorphism between those two?

Any comments on the rest of the post are welcome, of course. In particular if they point out mistakes or smarter ways to achieve the results.

Note: The square-bracket notation, justified by facts 4. and 5., is a nonstandard notation taken from the notes of my Complex Geometry professor.

The involution on $W\oplus\overline W$ is $(w_1,w_2)\mapsto(\sigma(w_1),\sigma(w_2))$. Hence, $[W\oplus\overline W]=[W]\oplus[W]$. Now set:
$$(w_1,w_2)\mapsto w_1+iw_2.$$
This map, which we will call $\phi$, is evidently a homomorphism of real vector spaces $[W]\oplus[W]\to[[W]]$.
Choosing a basis $\{e_i\}$ of $[W]$, we find $(e_i,e_j)\mapsto e_i+ie_j$. In particular, $e_i=\phi(e_i,0)\in\operatorname{Im}\phi$ and $ie_i=\phi(0,e_i)\in\operatorname{Im}\phi$. So the image of $\phi$ contains a basis of $[[W]]$, and $\phi$ is hence surjective.
If the dimension is finite, we are done. In general, let $(\sum a_ie_i,\sum b_ie_i)\mapsto0$. This means $\sum(a_i+ib_i)e_i=0$, but $\{e_i,ie_i\}$ are l.i., so this gives $a_i=b_i=0$, which means $(\sum a_ie_i,\sum b_ie_j)$ was zero in the first place, and proves injectivity, concluding the proof of item 3.