Frobenius theorem for differential forms

Question

I have to check the next version of the theorem Frobenius:

Let $M$ a smooth manifold and $\{\omega^1,\ldots,\omega^k\}\subset\Omega^{1}(U)$ $l.i.$ on $U\subset M$ and $P(x)=\{ v\in T_x M\vert \omega^j_x(v)=0$ for $j=1,\ldots,k\}$ then $P$ is completely integrable iff for all $j=1,\ldots,k$ $$d\omega^j\wedge \omega^1\wedge\dots\wedge \omega^k=0.$$ According to my exercise should I try this result by the following steps:

1. $P(x)$ is a subspace of codimension $k$ of $T_x M$ and $P$ is a $\mathcal{C}^{r}$-distribution.

2. We can complete a basis of $(T_x M)^\ast$ with $\{\omega^1,\ldots,\omega^k\}\subset\Omega^{1}(V)$ ($V\subset U$). If $\eta\in \Omega^{2}(U)$ such that $\eta\wedge \omega^1\wedge\dots\wedge \omega^k=0$ then $$\eta=\sum_{1\leq i<j\leq k}\alpha_{ij} \omega^i\wedge\omega^j$$

3. For $\omega\in \Omega^1(U)$, $X,Y$ vector fields we have: $$d\omega(X,Y)=d\omega(X)(Y)-d\omega(Y)(X)-\omega[X,Y]$$

4. If $X,Y$ vector fields on $P$ and $d\omega^j\wedge \omega^1\wedge\dots\wedge \omega^k=0$ for all $j=1,\ldots,k$ then $[X,Y]\in P$.

5.If $P$ is involutive then $d\omega^j\wedge \omega^1\wedge\dots\wedge \omega^k=0$ for all $j=1,\ldots,k$.

I have already the first four steps but I dont know how to prove the last one

Answer 1

Choose vector fields on $U$ with $X_1,...,X_{k}$ spanning $P$ complement and $X_{k+1},...,X_{k+n}$ spanning $P$ at each point.

You can use this formula for the wedge of two forms (set $\eta=\omega^1\wedge...\wedge\omega^k$):

$d\omega^j\wedge\eta(v_1,...,v_{2+k})=\sum_{\sigma\in S_{2,k}} \text{sgn}(\sigma)d\omega^j(v_{\sigma(1)}, v_{\sigma(2)})\eta(v_{\sigma(3)},...,v_{\sigma(k+2)})$

to get that the form vanishes by showing that each term in the sum vanishes when applied to any $k+2$ vectors from the frame.

This is just because $\iota_{X}\eta=0$ for any $X\in P$ and since $P$ is involutive $d\omega^j(X,Y)=0$ for any $X,Y\in P$ by your (3).

For example $d\omega^j\wedge\eta(X_1,...,X_{k+2})=0$ since each term of the sum with $X_{k+1}$ or $X_{k+2}$ plugged into $\eta$ is zero and the remaining terms of the sum with $X_{k+1}, X_{k+2}$ plugged into $d\omega^j$ are zero.