Prove $(\exists x)A\to((\exists x)(A\wedge(B\vee C))\equiv B \vee (\exists x)(A\wedge C))$, if $x$ is not free in $B$

Question

Prove $(\exists x)A\to\big((\exists x)(A\wedge(B\vee C))\equiv B \vee (\exists x)(A\wedge C)\big)$, if $x$ is not free in $B$.

I've tried multiple different ways and I'm not able to see a good path forward. I feel like my best bet is to start from:

$$A[x:=z]\vdash\big((\exists x)(A\wedge (B\vee C))\equiv B\vee (\exists x)(A\wedge C)\big)[x:=z]$$

Answer 1

Long comment : it works.

The trick is to prove that $A \vdash A \land (B \lor C) \equiv B \lor (A \land C)$.

So, using Coroll.6.1.11 :

$A[x := z] \vdash (\exists x) (A \land (B \lor C)) \equiv (\exists x)(B \lor (A \land C))$, with $z$ fresh.

Now we can distribute $\exists x$ over $\lor$ in the RHS, and - taking into account the fact that if $x$ is not free in $B$, then $\exists x B \equiv B$ [Ex.11, page 188] - we get :

$A[x := z] \vdash (\exists x) (A \land (B \lor C)) \equiv B \lor (\exists x)(A \land C)$.

Now, using Coroll. 6.5.8 we get :

$(\exists x)A \vdash (\exists x) (A \land (B \lor C)) \equiv B \lor (\exists x)(A \land C)$.