Funzione implicita vettoriale

[Reyzet]

Salve a tutti, ho questo esercizio: dato il sistema $f=xcosh(z)+ye^(z+y^2)=0,g=(arctan(x)+\pi/2)e^(-z-y)-y=0$, verificare che definisce implicitamente una $\phi(z)=(x(z),y(z))$ su tutto $\mathbb{R}$ unica e continua, precisando se è derivabile.

Io ho fatto così:
Fissato z reale dalla prima ottengo col teorema degli zeri una sola $x_{0}$ che la risolve indipendentemente da y, e dalla seconda una $y_{0}$ che risolve indipendentemente da x, accoppiandole ottengo una $\phi: z\rightarrow(x(z),y(z))$ in tutto R che risolve difatto il mio sistema.
Adesso questa punto per punto coincide con quella prescritta dal teorema vettoriale del Dini (le cui ipotesi sono verificate per ogni punto, cioè il jacobiano è invertibile sempre e blabla) che è unica e continua, e perciò ho concluso che la mia $\phi$ è continua (addirittura $C^\infty$) perché coincide globalmente con quella del Dini.
È corretto?

[dissonance]

Non penso. La x che trovi risolvendo la prima equazione dipende da z e anche da y. Stesso discorso con la seconda equazione. Non penso tu possa risolvere le equazioni una alla volta, ma se tu pensi sia possibile devi dimostrarlo.

[Reyzet]

Mmh non so, non ero convinto neanche io quindi forse hai ragione...
Unica altra cosa che ho in mente, ricavo x dalla prima come funzione di y e z, sostituendo nella seconda nasce una funzione solo di y e z a cui posso applicare il dini scalare (guarda caso quella derivata abominevole viene negativa) osservando che per ogni z ottengo una sola y che risolve perciò posso esplicitare una y(z), che è continua per gli stessi motivi del primo post. A questo punto non so, è possibile scrivere, sostituendo di nuovo nella prima la y e ottenendo: $x(y,z)=x(y(z),z)=x(z)$? (Non sono convintissimo di questo). Se fosse vero usando il dini vettoriale come nel primo post trovo la $\phi(z)$ cercata.

Il fatto è che con questi sistemi non ho mai avuto a che fare, e infatti nel libro è l'unico esercizio di questo tipo.

[dissonance]

Ma non credo. Sostanzialmente stai dicendo che la seconda equazione dà una funzione \(y=y(z)\) invece che \(y=y(x, z)\). Questo mi sembra proprio falso.

[Reyzet]

Allora non ho più idee, tu come lo faresti?

[dissonance]

Manipola un po' le due equazioni, sporcati le mani. Per esempio, io noto che, moltiplicando
\[
x\cosh(z)+ye^{z+y^2}=0\]
per \(e^{-z}\), si ottiene
\[
ye^{y^2}=-\frac x 2 -\frac{xe^{-2z}}{2}, \]
e siccome \(y\in \mathbb R\mapsto y e^{y^2}\in \mathbb R\) è una funzione invertibile, da qui si ottiene che per ogni \((x, z)\in\mathbb R^2\) esiste una unica \(y=y(x, z)\) che risolve l'equazione. Sostituisci questa \(y=y(x, z)\) nell'altra equazione e vedi se riesci a risolvere (implicitamente) la \(x\) in funzione di \(z\).