[proofplan]
We first prove that the bracket on cosets is independent of the representatives chosen. The only point is that replacing $x$ and $y$ by $x+a$ and $y+b$, with $a,b\in\mathfrak i$, changes the bracket by terms lying in $\mathfrak i$, exactly because $\mathfrak i$ is an ideal. Once well-definedness is established, bilinearity, alternation, and the Jacobi identity are inherited from the corresponding [Lie algebra](/page/Lie%20Algebra) axioms in $\mathfrak g$ by passing to cosets modulo $\mathfrak i$.
[/proofplan]
[step:Show that changing representatives changes the bracket by an element of $\mathfrak i$]
Let $x,y\in\mathfrak g$. Suppose $x',y'\in\mathfrak g$ are alternative representatives of the same cosets, so that $x'+\mathfrak i=x+\mathfrak i$ and $y'+\mathfrak i=y+\mathfrak i$. By the definition of equality in the quotient [vector space](/page/Vector%20Space), there exist elements $a,b\in\mathfrak i$ such that
\begin{align*}
x'=x+a
\end{align*}
and
\begin{align*}
y'=y+b.
\end{align*}
Using bilinearity of $[\cdot,\cdot]_{\mathfrak g}$, we compute
\begin{align*}
[x',y']_{\mathfrak g}-[x,y]_{\mathfrak g}=[x,b]_{\mathfrak g}+[a,y]_{\mathfrak g}+[a,b]_{\mathfrak g}.
\end{align*}
Since $\mathfrak i$ is an ideal of $\mathfrak g$, the elements $[x,b]_{\mathfrak g}$, $[a,y]_{\mathfrak g}$, and $[a,b]_{\mathfrak g}$ all lie in $\mathfrak i$. Since $\mathfrak i$ is a vector subspace of $\mathfrak g$, their sum lies in $\mathfrak i$. Therefore
\begin{align*}
[x',y']_{\mathfrak g}-[x,y]_{\mathfrak g}\in\mathfrak i,
\end{align*}
which is equivalent to
\begin{align*}
[x',y']_{\mathfrak g}+\mathfrak i=[x,y]_{\mathfrak g}+\mathfrak i.
\end{align*}
Thus $[\cdot,\cdot]_{\mathfrak g/\mathfrak i}$ is well-defined.
[guided]
We must check that the formula for the quotient bracket does not depend on the chosen representatives. This is the essential point: a coset $x+\mathfrak i$ has many representatives, and the expression $[x,y]_{\mathfrak g}+\mathfrak i$ is meaningful only if every choice gives the same coset.
Let $x,y\in\mathfrak g$, and let $x',y'\in\mathfrak g$ be different representatives of the same two cosets. The equalities $x'+\mathfrak i=x+\mathfrak i$ and $y'+\mathfrak i=y+\mathfrak i$ mean precisely that the differences $x'-x$ and $y'-y$ lie in $\mathfrak i$. Define $a:=x'-x\in\mathfrak i$ and $b:=y'-y\in\mathfrak i$. Then
\begin{align*}
x'=x+a
\end{align*}
and
\begin{align*}
y'=y+b.
\end{align*}
Now expand the bracket using bilinearity in $\mathfrak g$:
\begin{align*}
[x',y']_{\mathfrak g}=[x+a,y+b]_{\mathfrak g}=[x,y]_{\mathfrak g}+[x,b]_{\mathfrak g}+[a,y]_{\mathfrak g}+[a,b]_{\mathfrak g}.
\end{align*}
Subtracting $[x,y]_{\mathfrak g}$ gives
\begin{align*}
[x',y']_{\mathfrak g}-[x,y]_{\mathfrak g}=[x,b]_{\mathfrak g}+[a,y]_{\mathfrak g}+[a,b]_{\mathfrak g}.
\end{align*}
Each extra term lies in $\mathfrak i$. Indeed, $b\in\mathfrak i$ and $x\in\mathfrak g$, so the ideal property gives $[x,b]_{\mathfrak g}\in\mathfrak i$. Similarly, $a\in\mathfrak i$ and $y\in\mathfrak g$, so $[a,y]_{\mathfrak g}\in\mathfrak i$. Finally, since $a,b\in\mathfrak i\subset\mathfrak g$, the ideal property also gives $[a,b]_{\mathfrak g}\in\mathfrak i$. Because $\mathfrak i$ is a vector subspace, the sum of these three elements remains in $\mathfrak i$. Hence
\begin{align*}
[x',y']_{\mathfrak g}-[x,y]_{\mathfrak g}\in\mathfrak i.
\end{align*}
This says exactly that $[x',y']_{\mathfrak g}$ and $[x,y]_{\mathfrak g}$ determine the same coset modulo $\mathfrak i$:
\begin{align*}
[x',y']_{\mathfrak g}+\mathfrak i=[x,y]_{\mathfrak g}+\mathfrak i.
\end{align*}
Therefore the quotient bracket is independent of representatives and is well-defined.
[/guided]
[/step]
[step:Verify bilinearity of the quotient bracket]
Let $\alpha,\beta\in F$ and let $x_1,x_2,y\in\mathfrak g$. Using the vector space operations in $\mathfrak g/\mathfrak i$ and the bilinearity of $[\cdot,\cdot]_{\mathfrak g}$, we have
\begin{align*}
[\alpha(x_1+\mathfrak i)+\beta(x_2+\mathfrak i),y+\mathfrak i]_{\mathfrak g/\mathfrak i}=[\alpha x_1+\beta x_2,y]_{\mathfrak g}+\mathfrak i.
\end{align*}
The bracket in $\mathfrak g$ is $F$-linear in the first variable, so
\begin{align*}
[\alpha x_1+\beta x_2,y]_{\mathfrak g}+\mathfrak i=\alpha[x_1,y]_{\mathfrak g}+\beta[x_2,y]_{\mathfrak g}+\mathfrak i.
\end{align*}
Therefore
\begin{align*}
[\alpha(x_1+\mathfrak i)+\beta(x_2+\mathfrak i),y+\mathfrak i]_{\mathfrak g/\mathfrak i}=\alpha[x_1+\mathfrak i,y+\mathfrak i]_{\mathfrak g/\mathfrak i}+\beta[x_2+\mathfrak i,y+\mathfrak i]_{\mathfrak g/\mathfrak i}.
\end{align*}
The same computation in the second variable, using $F$-linearity of $[\cdot,\cdot]_{\mathfrak g}$ in the second variable, proves linearity in the second variable. Hence $[\cdot,\cdot]_{\mathfrak g/\mathfrak i}$ is $F$-bilinear.
[/step]
[step:Pass alternation and skew-symmetry to the quotient]
Let $x\in\mathfrak g$. Since $\mathfrak g$ is a Lie algebra, its bracket is alternating, so $[x,x]_{\mathfrak g}=0$. Therefore
\begin{align*}
[x+\mathfrak i,x+\mathfrak i]_{\mathfrak g/\mathfrak i}=[x,x]_{\mathfrak g}+\mathfrak i=0+\mathfrak i.
\end{align*}
Thus the quotient bracket is alternating. In particular, for all $x,y\in\mathfrak g$, bilinearity and alternation give
\begin{align*}
[x+\mathfrak i,y+\mathfrak i]_{\mathfrak g/\mathfrak i}+[y+\mathfrak i,x+\mathfrak i]_{\mathfrak g/\mathfrak i}=0+\mathfrak i.
\end{align*}
So the quotient bracket has the corresponding skew-symmetry consequence under the local convention for Lie brackets.
[/step]
[step:Pass the Jacobi identity to the quotient]
Let $x,y,z\in\mathfrak g$. By the definition of the quotient bracket,
\begin{align*}
[x+\mathfrak i,[y+\mathfrak i,z+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}=[x,[y,z]_{\mathfrak g}]_{\mathfrak g}+\mathfrak i.
\end{align*}
Applying the same computation to the other two cyclic terms gives
\begin{align*}
[y+\mathfrak i,[z+\mathfrak i,x+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}=[y,[z,x]_{\mathfrak g}]_{\mathfrak g}+\mathfrak i
\end{align*}
and
\begin{align*}
[z+\mathfrak i,[x+\mathfrak i,y+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}=[z,[x,y]_{\mathfrak g}]_{\mathfrak g}+\mathfrak i.
\end{align*}
Adding these three identities in the quotient vector space yields
\begin{align*}
[x+\mathfrak i,[y+\mathfrak i,z+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}+[y+\mathfrak i,[z+\mathfrak i,x+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}+[z+\mathfrak i,[x+\mathfrak i,y+\mathfrak i]_{\mathfrak g/\mathfrak i}]_{\mathfrak g/\mathfrak i}=([x,[y,z]_{\mathfrak g}]_{\mathfrak g}+[y,[z,x]_{\mathfrak g}]_{\mathfrak g}+[z,[x,y]_{\mathfrak g}]_{\mathfrak g})+\mathfrak i.
\end{align*}
The Jacobi identity in $\mathfrak g$ says that the element inside the parentheses is $0$. Hence the displayed sum is $0+\mathfrak i$, which is the zero element of $\mathfrak g/\mathfrak i$. Thus the quotient bracket satisfies the Jacobi identity.
[/step]
[step:Conclude that the quotient vector space is a Lie algebra]
The quotient $\mathfrak g/\mathfrak i$ is a vector space over $F$ because $\mathfrak i$ is a vector subspace of $\mathfrak g$. The map $[\cdot,\cdot]_{\mathfrak g/\mathfrak i}$ is well-defined, $F$-bilinear, alternating, and satisfies the Jacobi identity. Therefore $\mathfrak g/\mathfrak i$, equipped with this bracket, is a Lie algebra over $F$.
[/step]
