span_singleton_inf_orthogonal_eq_bot

English

A lemma about simplification of negations with IsAlt.

Русский

Лемма упрощения отрицания при условии IsAlt.

LaTeX

$$$(H.neg) \;\text{and related simplicities}$$$

Lean4

theorem span_singleton_inf_orthogonal_eq_bot (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁) (hx : ¬B.IsOrtho x x) :
    (K₁ ∙ x) ⊓ Submodule.orthogonalBilin (K₁ ∙ x) B = ⊥ :=
  by
  rw [← Finset.coe_singleton]
  refine eq_bot_iff.2 fun y h ↦ ?_
  obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1
  replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({ x } : Finset V₁))
  rw [Finset.sum_singleton] at h ⊢
  suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]
  rw [isOrtho_def, map_smulₛₗ] at h
  exact
    Or.elim (smul_eq_zero.mp h) (fun y ↦ by simpa using y)
      (fun hfalse ↦ False.elim <| hx hfalse)
        -- ↓ This lemma only applies in fields since we use the `mul_eq_zero`

Похожие утверждения