𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (u : F), u ∈ Submodule.map f U → ∀ (v : F), v ∈ Submodule.map f V → inner u v = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ Submodule.map f U ⟂ Submodule.map f V
rw [isOrtho_iff_inner_eq] at *
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (a : E), a ∈ U → ∀ (a_2 : E), a_2 ∈ V → inner a a_2 = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (u : F), u ∈ Submodule.map f U → ∀ (v : F), v ∈ Submodule.map f V → inner u v = 0
simp_rw [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  LinearIsometry.inner_map_map]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (a : E), a ∈ U → ∀ (a_2 : E), a_2 ∈ V → inner a a_2 = 0
exact h