Smoothness of horizontal bundle defined by connection one-form

Question

Let $G$ denote a Lie group and $\mathfrak{g}$ its Lie algebra. $P$ is a smooth principal bundle.

Given a smooth $\mathfrak{g}$-valued one-form $\omega_p: TP_p \to \mathfrak{g}$, which fulfils the properties listed below, is there an easy way to see that $p \mapsto ker(\omega_p) =: H_p$ is smooth?

1. For all $p \in P$ and $X \in \mathfrak{g}$, $\omega_p(\underline{X}_p) = X$, where $\underline{X}_p$ denotes the fundamental vector field to $X$.
2. For all $p \in P$ and $g \in G$, $$\omega_{p \cdot g} \circ (dR_g)_p = Ad_{g^{-1}} \circ \omega_{p}.$$ Here, $R_g$ denotes the right action of $g$ on P and $Ad_g$ the adjoint representation.

Answer 1

The general theorem is the following (Theorem 10.34 in J.M. Lee's book "Introduction to smooth manifolds", 2nd edition)

Let $E,E'$ be smooth vector bundles over a smooth manifold $M$ and $F:E\to E'$ be a smooth bundle homomorphism over $M$. Then $\ker F\subset E$ is a smooth subbundle if and only if $F$ has constant rank.

To apply the theorem you can view $\omega$ as a smooth bundle map $TP\to P\times\mathfrak g$ between smooth vector bundles over $P$. Then by the first property $F$ has constant rank $\dim\mathfrak g$, so $\ker\omega\subset TP$ is a smooth subbundle.