How to compute the image of a polyhedron under a linear transformation

Suppose $P$ is a polyhedron whose representation as a system of linear inequalities is given to us: $$ P = \{ x ~|~ Ax \leq b\}$$ Define $P'$ be the image of $P$ under the linear transformation which maps $x$ to $Cx$:
$$ P' = \{ Cx ~|~ x \in P \}.$$ Given $A,b,C$, our goal is to compute a representation of $P'$ as a system of linear inequalities, i.e., to compute $D,e$ satisfying $$ P' = \{ x ~|~ D x \leq e \}.$$ What is the complexity of this problem (i.e., how many arithmetic operations or bit operations are required)?

Let us adopt the convention that $A \in R^{m \times n}$ while $C \in R^{k \times n}$ so the answer should be in terms of $m,n,k$. Further, one may suppose that entries of $P$ are rational numbers whose numerators and denominators take $B$ bits to specify, so that in the bit-model answers should be in terms of $B$ as well.

You can switch from H-representation to V representation of $P$. Once you have the vertex $v_P$ of $P$ you can find the vertex in the co-domain as $v_{P^1}=Cv_P$. Then you can use any convex hull algorithm using the points $v_{P^1}$ to find the image.

I think the common approach is to use quantifier elimination. The image $P'$ is defined by the formula $$ \exists x. Ax \leq b \land x' = Cx $$ By eliminating the quantifiers for the $x$-variables, you get a system of inequalities on the variables $x'$ that define the resulting polyhedron $P'$.

Quantifier elimination for linear arithmetic can be done by Ferrante and Rackoff's method [1, Chapter 7.3]. The complexity of this method is $2^{2^{pn}}$ for a formula of length $n$ and some fixed constant $p$ [1, Theorem 2.24].

[1] Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)