Preuve : dimension de l'orthogonal

Soit $\vv{x}\in F\times F^{\perp}$. Alors : $$\ds\left\langle \vv{x},\vv{x}\right\rangle =0$$ donc $\vv{x}=\vv{0_E}$ et la somme est bien directe.

Soit $(\vv{e_1},\dots,\vv{e_p})$ une base orthonormale de $F$. On peut compléter cette base de $F$ en une base orthonormale $(\vv{e_1},\dots,\vv{e_p},\vv{e_{p+1}},\dots,\vv{e_n})$ de $E$. Alors le sous-espace $G=\mathrm{Vect}(\vv{e_{p+1}},\dots,\vv{e_n})$ est un supplémentaire de $F$ inclus dans $F^{\perp}$. Ainsi, par inclusion puis somme directe, on a : $$\ds\dim(E)=\dim(F)+\dim(G)\leqslant\dim(F)+\dim(F^{\perp})\leqslant\dim(E)$$ On en déduit que $\dim(G)=\dim(F^{\perp})$ ce qui nous assure que $G=F^{\perp}$.