∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) {x : E}, (((p.prodEquivOfIsCompl q h).symm x).1 = 0) = (x ∈ q)