𝕜 : 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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), u ∈ Submodule.comap f U → ∀ (v : E), v ∈ Submodule.comap 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 𝕜 F
h : U ⟂ V
⊢ Submodule.comap f U ⟂ Submodule.comap 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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → inner (↑f u) (↑f 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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), u ∈ Submodule.comap f U → ∀ (v : E), v ∈ Submodule.comap f V → inner u v = 0
simp_rw [mem_comap, ← f.inner_map_map]
𝕜 : 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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
u : E
hu : ↑f u ∈ U
v : E
hv : ↑f v ∈ V
⊢ inner (↑f u) (↑f 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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → inner (↑f u) (↑f v) = 0
intro u hu v hv
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 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
u : E
hu : ↑f u ∈ U
v : E
hv : ↑f v ∈ V
⊢ inner (↑f u) (↑f v) = 0
exact h _ hu _ hv