feat(analysis/normed_space/inner_product): consequences of characteri…

…zation of orthogonal projection (#5558)

Reverse order of equality in the lemma `eq_orthogonal_projection_of_mem_of_inner_eq_zero`.  Add some variants.  Also add three consequences:
- the orthogonal projection onto `K` of an element of `K` is itself
- the orthogonal projection onto `K` of an element of `Kᗮ` is zero
- for a submodule `K` of an inner product space, the sum of the orthogonal projections onto `K` and `Kᗮ` is the identity.

Reverse order of `iff` in the lemma `submodule.eq_top_iff_orthogonal_eq_bot`, and rename to `submodule.orthogonal_eq_bot_iff`.

src/analysis/normed_space/dual.lean

@@ -181,7 +181,7 @@ begin
       exact h' },
     exact ⟨0, by simp [hℓ]⟩ },
   { have Ycomplete := is_complete_ker ℓ,
-    rw [submodule.eq_top_iff_orthogonal_eq_bot Ycomplete, ←hY] at htriv,
+    rw [← submodule.orthogonal_eq_bot_iff Ycomplete, ←hY] at htriv,
     change Yᗮ ≠ ⊥ at htriv,
     rw [submodule.ne_bot_iff] at htriv,
     obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv,