Hecke-module structure implicit in definition of automorphic forms in Borel-Jacquet's Corvallis article

Let $G$ be a connected reductive group over a number field $F$, $G_\infty=\prod_{v\mid\infty} G(F_v)$, $\mathbf{A}$ the adèles of $F$, $\mathbf{A}_f$ the finite adèles of $F$. Fix a maximal compact subgroup $K$ of $G_\infty$. We have Hecke algebras $H_\infty$ of $G_\infty$ (relative to $K$) and $H_f$ of $G(\mathbf{A}_f)$. The former is the one used by Flath and Borel-Jacquet in their Corvallis Volume 1 articles (not the one from Jacquet-Langlands) and is described in great detail in Chapter 1 of Knapp-Vogan's giant book on cohomological induction. It is the convolution algebra of left $K$-finite distributions on $G_\infty$ with support in $K$ (see Appendix B of Knapp-Vogan for distributions on manifolds). The algebra $H_f$ is the convolution algebra of $\mathbf{C}$-valued, locally constant, compactly supported functions on $G(\mathbf{A}_f)$. The important facts about these $\mathbf{C}$-algebras are that they have an "approximate identity" (a certain collection of idempotents) and a resulting notion of "smooth module" (see Chapter 1 of Knapp-Vogan for the definitions, although they use the term "approximately unital module"). One can prove that

(1) smooth $\mathbf{C}$-representations of $G(\mathbf{A}_f)$ are the same as smooth $H_f$-modules (which are automatically $\mathbf{C}$-vector spaces because $H_f$ has an "approximate identity"), and

(2) smooth $H_\infty$-modules are the same as $(\mathfrak{g},K)$-modules, where $\mathfrak{g}=\mathrm{Lie}(G_\infty)$, and the definition of $(\mathfrak{g},K)$-modules I'm using is from Knapp-Vogan's book, or equivalently, Wallach's Corvallis Volume 1 article.

In Borel-Jacquet's Corvallis article, they define an automorphic form on $G(\mathbf{A})$ by a list of properties (see the top of page 195 of Corvallis Volume 1 for the properties). In particular, automorphic forms are complex-valued functions on $G(\mathbf{A})$ which are smooth in the sense that they are continuous, $C^\infty$ in the Archimedean variable, and locally constant in the finite adelic variable.

My question is as follows. The conditions imposed on such a function by B-J to make it an automorphic form involve a right action of the Hecke algebra $H:=H_\infty\otimes_\mathbf{C}H_f$. For this to make sense, automorphic forms should live in some large $\mathbf{C}$-vector space which is simultaneously an $H_\infty$-module and an $H_f$-module, i.e., simultaneously a $(\mathfrak{g},K)$-module and a smooth $G(\mathbf{A}_f)$-representation. What space is this?

I think that the right regular representation of $G(\mathbf{A})$ on the space of all $\mathbf{C}$-valued functions on $G(\mathbf{A})$ preserves the space $C^\infty(G(\mathbf{A}))$ of smooth functions defined above, and we must at least take the subspace of $K$-finite vectors (in the sense of Chapter 1 of Knapp-Vogan, which includes a continuity condition for the $K$-action) to get a $(\mathfrak{g},K)$-module structure (property (b) of B-J implies that automorphic forms are right $K$-finite anyway). We should also take the $G(\mathbf{A}_f)$-smooth vectors (I don't think smoothness is automatic, despite the terminology, again property (b) forces smoothness of automorphic forms in the sense of representations of locally profinite groups). Because the $K$ and $G(\mathbf{A}_f)$-actions commute, I think the order in which we take these subspaces doesn't matter, and we end up with a $K$-finite representation which is also a smooth representation of $G(\mathbf{A}_f)$, hence an $H(K)\otimes_\mathbf{C}H_f$-module, where $H(K)$ is the Hecke algebra of $K$ (left and right $K$-finite distributions on $K$). We'll have a differentiated action of $\mathfrak{k}=\mathrm{Lie}(K)$, but how do we get one of $\mathfrak{g}$? It doesn't quite make sense to ask if $K$-finite vectors in our space are $C^\infty$-vectors for the $G$-action, because there is no topology on the space (if all the vectors were $G$-finite, we could differentiate the $G$-action, but this is not going to be the case).

If I'm on the right track, my question then boils down to: how do we get an action of $\mathfrak{g}$ on the space of $K$-finite, $G(\mathbf{A}_f)$-smooth vectors in $C^\infty(G(\mathbf{A}))$?

This kind of thing has often confused me because, for example, $K$-finiteness of automorphic forms is part of the definition, but the way it is phrased in B-J (in terms of being fixed by a standard idempotent in $H$) only makes sense if we have an action of $H$, and if we need to take $K$-finite vectors to get the $H$-action in the first place, the logic is out of order!

EDIT: It occurs to me that maybe we can differentiate the $G_\infty$-action from the very beginning (in $C^\infty(G(\mathbf{A}))$), using the usual formula. Namely, for $g=(g_\infty,g_f)\in G_\infty\times G(\mathbf{A}_f)$, and $X\in\mathfrak{g}$, if $f\in C^\infty(G(\mathbf{A}))$, then the function

$$t\mapsto f(g_\infty\exp(tX),g_f):\mathbf{R}\to\mathbf{C}$$

will be smooth, and we can define $(Xf)(g_\infty,g_f)$ to be the derivative of this function at $t=0$. Is this the correct way to get the $\mathfrak{g}$-action and hence the $(\mathfrak{g},K)$-module structure on the subspace of $K$-finite vectors? If so, is there a less ad hoc way to get the $\mathfrak{g}$-action? The fact this isn't an actual vector-valued derivative, like what you'd have with a smooth vector in e.g. a Banach space representation of $G_\infty$, is somehow unsatisfying to me, but perhaps I shouldn't expect anything like that since the point of view here does not involve a locally convex topology on the space $C^\infty(G(\mathbf{A}))$...of which I'm aware.

The definition on the top of page 195 in B-J's article (in Corvallis 1) is ok, because $f\ast\xi$ is well-defined for any smooth $f:G(\mathbf{A})\to\mathbf{C}$ and any $\xi\in H$.
It suffices to verify the claim for pure tensors $\xi=\xi_\infty\otimes\xi_f$, in which case $f\ast\xi$ is $f\ast\xi_\infty$ convolved with $\xi_f\in H_f$ in the usual sense. The function $f\ast\xi_\infty$ exists by the smoothness assumption, while the integral defining the convolution converges, because $\xi_f:G(\mathbf{A}_f)\to\mathbf{C}$ is compactly supported and locally constant by definition.