Physlib.Mathematics.InnerProductSpace.Submodule

Imports

/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module

public import Mathlib.Analysis.InnerProductSpace.LinearPMap

Submodules of `E × F`

In this module we define submoduleToLp which reinterprets a submodule of E × F, where E and F are inner product spaces, as a submodule of WithLp 2 (E × F). This allows us to take advantage of the inner product structure, since otherwise by default E × F is given the sup norm.

@[expose] public section

The submodule of WithLp 2 (E × F) defined by M.

def submoduleToLp : Submodule ℂ (WithLp 2 (E × F)) where
  carrier := {x | x.ofLp ∈ M}
  add_mem' := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fg:F × E⊢ ∀ {a b : WithLp 2 (E × F)}, a ∈ {x | x.ofLp ∈ M} → b ∈ {x | x.ofLp ∈ M} → a + b ∈ {x | x.ofLp ∈ M}
    intro a b ha hbE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fg:F × Ea:WithLp 2 (E × F)b:WithLp 2 (E × F)ha:a ∈ {x | x.ofLp ∈ M}hb:b ∈ {x | x.ofLp ∈ M}⊢ a + b ∈ {x | x.ofLp ∈ M}
    exact Submodule.add_mem M ha hbAll goals completed! 🐙
  zero_mem' := Submodule.zero_mem M
  smul_mem' := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fg:F × E⊢ ∀ (c : ℂ) {x : WithLp 2 (E × F)}, x ∈ {x | x.ofLp ∈ M} → c • x ∈ {x | x.ofLp ∈ M}
    intro c x hxE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fg:F × Ec:ℂx:WithLp 2 (E × F)hx:x ∈ {x | x.ofLp ∈ M}⊢ c • x ∈ {x | x.ofLp ∈ M}
    exact Submodule.smul_mem M c hxAll goals completed! 🐙

              lemma mem_submodule_iff_mem_submoduleToLp : f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M :=
  Eq.to_iff rfl

lemma submoduleToLp_closure :
    (submoduleToLp M.topologicalClosure) = (submoduleToLp M).topologicalClosure := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ submoduleToLp M.topologicalClosure = (submoduleToLp M).topologicalClosure
  rw [Submodule.ext_iffE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ ∀ (x : WithLp 2 (E × F)), x ∈ submoduleToLp M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosureE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ ∀ (x : WithLp 2 (E × F)), x ∈ submoduleToLp M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosure]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ ∀ (x : WithLp 2 (E × F)), x ∈ submoduleToLp M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosure
  intro xE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ x ∈ submoduleToLp M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosure
  rw [← mem_submodule_iff_mem_submoduleToLpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ x.ofLp ∈ M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosureE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ x.ofLp ∈ M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosure]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ x.ofLp ∈ M.topologicalClosure ↔ x ∈ (submoduleToLp M).topologicalClosure
  change x.ofLp ∈ _root_.closure M ↔ x ∈ _root_.closure (submoduleToLp M)E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ x.ofLp ∈ _root_.closure ↑M ↔ x ∈ _root_.closure ↑(submoduleToLp M)
  repeat rw [mem_closure_iff_nhdsE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) ↔ x ∈ _root_.closure ↑(submoduleToLp M)E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) ↔ ∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonempty]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) ↔ x ∈ _root_.closure ↑(submoduleToLp M)E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) ↔ ∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).NonemptyE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) ↔ ∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonempty
  constructormpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) → ∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).NonemptymprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonempty) → ∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty
  ·mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty) → ∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonempty intro h t htmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))ht:t ∈ nhds x⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    apply mem_nhds_iff.mp at htmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))ht:∃ t_1 ⊆ t, IsOpen t_1 ∧ x ∈ t_1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    rcases ht with ⟨t1, ht1, ht1', hx⟩mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    have : ∃ t' ∈ nhds x.ofLp, (∀ y ∈ t', WithLp.toLp 2 y ∈ t1) := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ submoduleToLp M.topologicalClosure = (submoduleToLp M).topologicalClosurempE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1this:∃ t' ∈ nhds x.ofLp, ∀ y ∈ t', WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
      refine Filter.eventually_iff_exists_mem.mp ?_E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1⊢ ∀ᶠ (x : E × F) in nhds x.ofLp, WithLp.toLp 2 x ∈ t1mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1this:∃ t' ∈ nhds x.ofLp, ∀ y ∈ t', WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
      apply ContinuousAt.eventually_mem (byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1⊢ ContinuousAt (WithLp.toLp 2) x.ofLpmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1this:∃ t' ∈ nhds x.ofLp, ∀ y ∈ t', WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty fun_propAll goals completed! 🐙mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1this:∃ t' ∈ nhds x.ofLp, ∀ y ∈ t', WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty) (IsOpen.mem_nhds ht1' hx)mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1this:∃ t' ∈ nhds x.ofLp, ∀ y ∈ t', WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    rcases this with ⟨t2, ht2, ht2'⟩mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1t2:Set (E × F)ht2:t2 ∈ nhds x.ofLpht2':∀ y ∈ t2, WithLp.toLp 2 y ∈ t1⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    rcases h t2 ht2 with ⟨w, hw⟩mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1t2:Set (E × F)ht2:t2 ∈ nhds x.ofLpht2':∀ y ∈ t2, WithLp.toLp 2 y ∈ t1w:E × Fhw:w ∈ t2 ∩ ↑M⊢ (t ∩ ↑(submoduleToLp M)).Nonempty
    use WithLp.toLp 2 whE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonemptyt:Set (WithLp 2 (E × F))t1:Set (WithLp 2 (E × F))ht1:t1 ⊆ tht1':IsOpen t1hx:x ∈ t1t2:Set (E × F)ht2:t2 ∈ nhds x.ofLpht2':∀ y ∈ t2, WithLp.toLp 2 y ∈ t1w:E × Fhw:w ∈ t2 ∩ ↑M⊢ WithLp.toLp 2 w ∈ t ∩ ↑(submoduleToLp M)
    exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)),
      (mem_submodule_iff_mem_submoduleToLp M w).mpr hw.2⟩All goals completed! 🐙
  ·mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)⊢ (∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonempty) → ∀ t ∈ nhds x.ofLp, (t ∩ ↑M).Nonempty intro h t htmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)ht:t ∈ nhds x.ofLp⊢ (t ∩ ↑M).Nonempty
    apply mem_nhds_iff.mp at htmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)ht:∃ t_1 ⊆ t, IsOpen t_1 ∧ x.ofLp ∈ t_1⊢ (t ∩ ↑M).Nonempty
    rcases ht with ⟨t1, ht1, ht1', hx⟩mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty
    have : ∃ t' ∈ nhds x, (∀ y ∈ t', y.ofLp ∈ t1) := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)⊢ submoduleToLp M.topologicalClosure = (submoduleToLp M).topologicalClosuremprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1this:∃ t' ∈ nhds x, ∀ y ∈ t', y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty
      refine Filter.eventually_iff_exists_mem.mp ?_E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1⊢ ∀ᶠ (x : WithLp 2 (E × F)) in nhds x, x.ofLp ∈ t1mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1this:∃ t' ∈ nhds x, ∀ y ∈ t', y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty
      exact ContinuousAt.eventually_mem (byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1⊢ ContinuousAt WithLp.ofLp xmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1this:∃ t' ∈ nhds x, ∀ y ∈ t', y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty fun_propAll goals completed! 🐙mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1this:∃ t' ∈ nhds x, ∀ y ∈ t', y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty) (IsOpen.mem_nhds ht1' hx)mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1this:∃ t' ∈ nhds x, ∀ y ∈ t', y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty
    rcases this with ⟨t2, ht2, ht2'⟩mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1t2:Set (WithLp 2 (E × F))ht2:t2 ∈ nhds xht2':∀ y ∈ t2, y.ofLp ∈ t1⊢ (t ∩ ↑M).Nonempty
    rcases h t2 ht2 with ⟨w, hw⟩mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1t2:Set (WithLp 2 (E × F))ht2:t2 ∈ nhds xht2':∀ y ∈ t2, y.ofLp ∈ t1w:WithLp 2 (E × F)hw:w ∈ t2 ∩ ↑(submoduleToLp M)⊢ (t ∩ ↑M).Nonempty
    use w.ofLphE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)x:WithLp 2 (E × F)h:∀ t ∈ nhds x, (t ∩ ↑(submoduleToLp M)).Nonemptyt:Set (E × F)t1:Set (E × F)ht1:t1 ⊆ tht1':IsOpen t1hx:x.ofLp ∈ t1t2:Set (WithLp 2 (E × F))ht2:t2 ∈ nhds xht2':∀ y ∈ t2, y.ofLp ∈ t1w:WithLp 2 (E × F)hw:w ∈ t2 ∩ ↑(submoduleToLp M)⊢ w.ofLp ∈ t ∩ ↑M
    exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp M)).mp hw.2⟩All goals completed! 🐙

lemma mem_submodule_closure_iff_mem_submoduleToLp_closure :
    f ∈ M.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp M).topologicalClosure := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ f ∈ M.topologicalClosure ↔ WithLp.toLp 2 f ∈ (submoduleToLp M).topologicalClosure
  rw [← submoduleToLp_closureE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ f ∈ M.topologicalClosure ↔ WithLp.toLp 2 f ∈ submoduleToLp M.topologicalClosureE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ f ∈ M.topologicalClosure ↔ WithLp.toLp 2 f ∈ submoduleToLp M.topologicalClosure]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ f ∈ M.topologicalClosure ↔ WithLp.toLp 2 f ∈ submoduleToLp M.topologicalClosure
  rflAll goals completed! 🐙

lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal :
    g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ
  constructormpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.adjoint → WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ → g ∈ M.adjoint <;>mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.adjoint → WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ → g ∈ M.adjoint intro hmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ⊢ g ∈ M.adjoint
  ·mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:g ∈ M.adjoint⊢ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ rw [mem_orthogonalmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:g ∈ M.adjoint⊢ ∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:g ∈ M.adjoint⊢ ∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0]mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:g ∈ M.adjoint⊢ ∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
    intro u humpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:g ∈ M.adjointu:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
    rw [mem_adjoint_iffmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0] at hmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
    have h' : inner ℂ u.snd g.1 = inner ℂ u.fst g.2 := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp Mh':inner ℂ u.snd g.1 = inner ℂ u.fst g.2⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
      rw [← sub_eq_zeroE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u.snd g.1 - inner ℂ u.fst g.2 = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u.snd g.1 - inner ℂ u.fst g.2 = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp Mh':inner ℂ u.snd g.1 = inner ℂ u.fst g.2⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp M⊢ inner ℂ u.snd g.1 - inner ℂ u.fst g.2 = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp Mh':inner ℂ u.snd g.1 = inner ℂ u.fst g.2⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
      exact h u.fst u.snd humpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp Mh':inner ℂ u.snd g.1 = inner ℂ u.fst g.2⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0u:WithLp 2 (E × F)hu:u ∈ submoduleToLp Mh':inner ℂ u.snd g.1 = inner ℂ u.fst g.2⊢ inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0
    simp [h']All goals completed! 🐙
  ·mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ⊢ g ∈ M.adjoint rw [mem_adjoint_iffmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ⊢ ∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ⊢ ∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0]mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ⊢ ∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b g.1 - inner ℂ a g.2 = 0
    intro a b habmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮa:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
    rw [mem_orthogonalmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0] at hmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
    have hab' := (mem_submodule_iff_mem_submoduleToLp M (a, b)).mp habmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
    have h' : inner ℂ a g.2 = inner ℂ b g.1 := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
      rw [← sub_eq_zero,E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 - inner ℂ b g.1 = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + inner ℂ b (-g.1) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0 sub_eq_add_neg,E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + -inner ℂ b g.1 = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + inner ℂ b (-g.1) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0 ← inner_neg_rightE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + inner ℂ b (-g.1) = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + inner ℂ b (-g.1) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp M⊢ inner ℂ a g.2 + inner ℂ b (-g.1) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
      exact h (WithLp.toLp 2 (a, b)) hab'mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × Eh:∀ u ∈ submoduleToLp M, inner ℂ u (WithLp.toLp 2 (g.2, -g.1)) = 0a:Eb:Fhab:(a, b) ∈ Mhab':WithLp.toLp 2 (a, b) ∈ submoduleToLp Mh':inner ℂ a g.2 = inner ℂ b g.1⊢ inner ℂ b g.1 - inner ℂ a g.2 = 0
    simp [h']All goals completed! 🐙

lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal :
    f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ
  simp only [mem_adjoint_iff]E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0) ↔
  WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ
  trans ∀ v, (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0) ↔
  ∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0) ↔
  WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ
  ·E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0) ↔
  ∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 constructormpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0) →
  ∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0) →
  ∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0 <;>mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0) →
  ∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × F⊢ (∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0) →
  ∀ (a : F) (b : E),
    (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0 intro hmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0⊢ ∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0
    ·mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0⊢ ∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 intro v hwmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0
      have h' := h (-v.snd) v.fstmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) →
  inner ℂ v.fst f.1 - inner ℂ (-v.snd) f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0
      rw [inner_neg_left,mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 - -inner ℂ v.snd f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0 sub_neg_eq_addmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0] at h'mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0⊢ inner ℂ v (WithLp.toLp 2 f) = 0
      apply h'mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0⊢ ∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0
      intro a b habmpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ b (-v.snd) - inner ℂ a v.fst = 0
      rw [inner_neg_right,mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ -inner ℂ b v.snd - inner ℂ a v.fst = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ a v.fst + inner ℂ b v.snd = 0 neg_sub_left,mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ -(inner ℂ a v.fst + inner ℂ b v.snd) = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ a v.fst + inner ℂ b v.snd = 0 neg_eq_zerompE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ a v.fst + inner ℂ b v.snd = 0mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ a v.fst + inner ℂ b v.snd = 0]mpE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0v:WithLp 2 (E × F)hw:∀ w ∈ submoduleToLp M, inner ℂ w v = 0h':(∀ (a : E) (b : F), (a, b) ∈ M → inner ℂ b (-v.snd) - inner ℂ a v.fst = 0) → inner ℂ v.fst f.1 + inner ℂ v.snd f.2 = 0a:Eb:Fhab:(a, b) ∈ M⊢ inner ℂ a v.fst + inner ℂ b v.snd = 0
      exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab)All goals completed! 🐙
    ·mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0⊢ ∀ (a : F) (b : E),
  (∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0) → inner ℂ b f.1 - inner ℂ a f.2 = 0 intro a b h'mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 - inner ℂ a f.2 = 0
      rw [sub_eq_add_neg,mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 + -inner ℂ a f.2 = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 + inner ℂ (-a) f.2 = 0 ← inner_neg_leftmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 + inner ℂ (-a) f.2 = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 + inner ℂ (-a) f.2 = 0]mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ inner ℂ b f.1 + inner ℂ (-a) f.2 = 0
      apply h (WithLp.toLp 2 (b, -a))mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0⊢ ∀ w ∈ submoduleToLp M, inner ℂ w (WithLp.toLp 2 (b, -a)) = 0
      intro w hwmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0w:WithLp 2 (E × F)hw:w ∈ submoduleToLp M⊢ inner ℂ w (WithLp.toLp 2 (b, -a)) = 0
      have hw' := h' w.fst w.snd hwmprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0w:WithLp 2 (E × F)hw:w ∈ submoduleToLp Mhw':inner ℂ w.snd a - inner ℂ w.fst b = 0⊢ inner ℂ w (WithLp.toLp 2 (b, -a)) = 0
      rw [sub_eq_zeromprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0w:WithLp 2 (E × F)hw:w ∈ submoduleToLp Mhw':inner ℂ w.snd a = inner ℂ w.fst b⊢ inner ℂ w (WithLp.toLp 2 (b, -a)) = 0mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0w:WithLp 2 (E × F)hw:w ∈ submoduleToLp Mhw':inner ℂ w.snd a = inner ℂ w.fst b⊢ inner ℂ w (WithLp.toLp 2 (b, -a)) = 0] at hw'mprE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)f:E × Fh:∀ (v : WithLp 2 (E × F)), (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0a:Fb:Eh':∀ (a_1 : E) (b_1 : F), (a_1, b_1) ∈ M → inner ℂ b_1 a - inner ℂ a_1 b = 0w:WithLp 2 (E × F)hw:w ∈ submoduleToLp Mhw':inner ℂ w.snd a = inner ℂ w.fst b⊢ inner ℂ w (WithLp.toLp 2 (b, -a)) = 0
      simp [hw']All goals completed! 🐙
  simp only [← mem_orthogonal]All goals completed! 🐙

lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal :
    g ∈ M.topologicalClosure.adjoint ↔
    WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮ := byE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ g ∈ M.topologicalClosure.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮ
  rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal,E:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M.topologicalClosure)ᗮ ↔
  WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮAll goals completed! 🐙 submoduleToLp_closureE:Type u_1inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace ℂ EF:Type u_2inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace ℂ FM:Submodule ℂ (E × F)g:F × E⊢ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮ ↔
  WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮAll goals completed! 🐙]All goals completed! 🐙

Submodules of E × F

Submodules of `E × F`