Why is this true? How did they obtain it? In my book, I saw a very long proof of some theorem and I tried to understand their proof. But, I noticed a statement (actually an implication) which I couldn't understand. This is confusing part of the proof:

[...] and let $P$ be the set for which [...], then the statement
  $$\forall a\in\mathbb{R}\left(\left(a=0\lor\exists b\in P\left(a+b\in P\right)\right)\implies a\in P\right)$$
  is equivalent to
  $$0\in P\land\forall a\in\mathbb{R}\left(\exists b\in P\left(a+b\in P\right)\implies a\in P\right)$$

So, I cannot understand how they concluded that. The definition of set $P$ is irrelevant. They've somehow concluded that $0$ is element of $P$. Also, how did they pull that part out of the brackets?
Probably there is some logical tautology they've applied here. but I'm not sure which.
 A: $$\forall a\in\mathbb{R}((a=0\lor\exists b\in P (a+b\in P))\rightarrow a\in P) \Leftrightarrow$$
$$\forall a\in\mathbb{R}((a=0\rightarrow a\in P)\land(\exists b\in P (a+b\in P)\rightarrow a\in P)) \Leftrightarrow$$
$$\forall a\in\mathbb{R}(a=0\rightarrow a\in P)\land\forall a\in\mathbb{R}(\exists b\in P (a+b\in P)\rightarrow a\in P) \Leftrightarrow$$
$$0\in P\land\forall a\in\mathbb{R}\left(\exists b\in P\left(a+b\in P\right)\rightarrow a\in P\right)$$
Step 1 is because of the general equivalence: $(P \lor Q) \rightarrow R \Leftrightarrow (P \rightarrow R) \land (Q \rightarrow R)$
Step 2 is because of the general equivalence: $\forall x (P(x) \land Q(x)) \Leftrightarrow \forall x \ P(x) \land \forall x \ Q(x))$
Step 3 is because of the general equivalence: $\forall x (x = c \rightarrow P(x)) \Leftrightarrow P(c)$
A: From the first statement, if you take only the first part of the premiss, you get :
$\forall a\in\mathbb{R}, (a=0) \Rightarrow (a\in P)$ ; this is equivalent to $0\in P$.
The second part of the premiss goes :
$\forall a\in\mathbb{R}, (\exists b\in P$ s.t. $(a+b) \in P) \Rightarrow (a\in P)$
It is unchanged in the second statement.
So, the two statements are indeed equivalent.
A: I think that the logical tautology you are looking for is
$\left( p \lor q \right)\implies r$ is equivalent to $\left( p \implies r \right) \land \left( q \implies r \right)$
