Given the equation $\sin(x^2+y)-2x=0$ for $x\in R$ with $y\in R$ as a parameter, I know that neighborhoods $V$ and $U$ of $0$ in $R$ exist such that for every $y\in V$ there exists a unique solution $x=\psi(y) \in U.$ I have already proven that $\psi$ is a $C^{\infty}$ mapping on $V$.
I have used the following notation: $x=\psi(y), x'=\psi \ ' (y)$ and $x''=\psi \ ''(y).$
After showing that $$2(x \cos(x^2+y)-1)x'+\cos(x^2+y)=0 \ \forall y \in V,$$ I derived that $$\psi \ ' (y) = \frac{-\cos(x^2+y)}{2(x \cos(x^2+y)-1)}.$$ In addition, I know that $\psi \ '(0)=\frac{1}{2}$ from the above equation.
Now, I am trying to prove that $$(x \cos (x^2+y)-1)x'' + (\cos(x^2+y)-4x^3)(x')^2-4x^2x'-x=0 \ \forall y \in V$$ in order to know what $\psi \ ''(y)$ is equal to. This can of course be derived from the equation above, but I have yet to prove that this equation is correct.
Any help in proving this equation would be appreciated.
Admitting that you are considering $$(x \cos (x^2+y)-1)x'' + \color{red}{(}\cos(x^2+y)-4x^3)\,(x')^2-4x^2\,x'-x \tag 1$$ it could be simpler to rewrite $$x' =\frac 1 {y'}\qquad\text{and} \qquad x''=-\frac{y''}{(y')^3}$$ which make, after simplifications, $$ y'' \left(1-x \cos \left(x^2+y\right)\right)-4 x^2 (y')^2+y' \left(\cos \left(x^2+y\right)-4 x^3\right)-x (y')^3 \tag 2$$ Now $$\sin(x^2+y)-2x=0 \implies y=\sin ^{-1}(2 x)-x^2$$ then $$y=\sin ^{-1}(2 x)-x^2\implies y'=\frac{2}{\sqrt{1-4 x^2}}-2 x \implies y''=\frac{8 x}{\left(1-4 x^2\right)^{3/2}}-2$$
Just replace in $(2)$ and simplify.