Let $A$ be a unital commutative and associative $\mathbb{Q}$-algebra.
Define $exp(f):=\sum_{n=0}^\infty \frac{f^n}{n!}$ for each $f\in XA[[X]]$.
Define $log(f):=\sum_{n=1}^\infty \frac{(-1)^{n+1}}{n} (f-1)^n$ for each $f\in 1+XA[[X]]$.
Hence, we have two maps $exp:XA[[X]]\rightarrow 1+XA[[X]]$ and $log:1+XA[[X]]\rightarrow XA[[X]]$.
I am trying to prove that $log$ map is the inverse of the $exp$ map.
The first thing I tried is to directly show $log\circ exp=id$ and $exp\circ log = id$ by checking if the identities hold for every element $f$, but this does not work well since this way involves too many calculations. For example, $$[X^n]exp(log(f))=[X^n]\sum_{k=0}^n log(f)^k/k! = \sum_{k=0}^n \frac{1}{k!} [X^n]log(f)^k= \sum_{k=0}^n \frac{1}{k!} [X^n](\sum_{l=1}^k \frac{(-1)^{l+1}}{l} (f-1)^l)^k$$.
Thus, we have to show that $$\sum_{k=0}^n \frac{1}{k!} [X^n](\sum_{l=1}^k \frac{(-1)^{l+1}}{l} (f-1)^l)^k=[X^n]f$$.
But this calculation is really a nightmare.. Is there a clever way to show this? If not, how do I wisely calculate to show the above identity?
Thank you in advance.
Here is one possible argument. One way to define the exponential $\exp(x)$ as a formal power series is that it is the unique formal power series $f(x)$ (over any commutative $\mathbb{Q}$-algebra) satisfying $f(0) = 1$ and
$$f'(x) = f(x).$$
Repeatedly differentiating this identity easily gives $[x^n] \exp(x) = \frac{1}{n!}$ as expected. Similarly, one way to define the logarithm $\log (1 + x)$ as a formal power series is that it is the unique formal power series $g(x)$ satisfying $g(0) = 0$ and
$$g'(x) = \frac{1}{1 + x} = \sum_{n=0}^{\infty} (-1)^n x^n.$$
So what can we say about the composite $\exp \log (1 + x)$? Well, by the formal chain rule, we have
$$\frac{d}{dx} f(g(x)) = f'(g(x)) g'(x) = f(g(x)) \frac{1}{1 + x}.$$
So $f(g(x))$ is a solution $h(x)$ to the differential equation $h'(x) = h(x) \frac{1}{1 + x}$ with initial condition $h(0) = f(g(0)) = 1$. We clearly have $h(x) = 1 + x$ is a solution, and we can appeal to a formal version of the Picard-Lindelof theorem to assert that formal solutions to ODEs exist and are unique, so we conclude that
$$\exp \log (1 + x) = 1 + x.$$
Similarly, what can we say about $\log \exp x = \log ((\exp x - 1) + 1)$? Well, again by the formal chain rule, we have
$$\frac{d}{dx} g(f(x) - 1) = g'(f(x) - 1) f'(x) = \frac{f'(x)}{f(x)} = 1.$$
So $g(f(x) - 1)$ is a solution to the ODE $\frac{d}{dx} h(x) = 1$ with initial condition $h(0) = g(f(0) - 1) = 0$. Here it's a bit simpler to see that we must have $h(x) = x$, so
$$\log \exp(x) = x.$$