Theory Determinants_More

section‹Determinants›

theory Determinants_More
  imports "HOL-Analysis.Starlike"
begin

lemma hyperplane_subset_imp_scaled:
  fixes a :: "'a::euclidean_space"
  assumes "{x. a ∙ x = b} ⊆ {x. a' ∙ x = b'}"
      and "a ≠ 0"
      and "a' ≠ 0"
  shows "∃c. a' = c *⇩R a ∧ b' = c * b ∧ c ≠ 0"
proof -
  let ?c = "(a ∙ a') / (a ∙ a)"
  let ?v = "a' - ?c *⇩R a"
  have "a ∙ ?v = 0"
    by (simp add: inner_diff)
  let ?w = "(b / (a ∙ a)) *⇩R a"
  have "a ∙ ?w = b"
    using assms(2) by simp
  then have "a' ∙ ?w = b'"
    using assms(1) by blast
  have "a ∙ (?w + ?v) = b"
    using ‹a ∙ ?w = b› ‹a ∙ ?v = 0›
    by (simp add: inner_add_right)
  then have "a' ∙ (?w + ?v) = b'"
    using assms(1) by blast
  then have "a' ∙ ?v = 0"
    using ‹a' ∙ ?w = b'›
    by (simp add: inner_add_right)
  have "?v ∙ ?v = 0"
    using ‹a' ∙ ?v = 0› ‹a ∙ ?v = 0›
    by (simp add: inner_diff_left)
  then have "?v = 0"
    by simp
  then have "a' = ?c *⇩R a"
    by auto
  moreover have "b' = ?c * b"
    by (metis (mono_tags, lifting) assms(1) Collect_mono_iff ‹a' = ?c *⇩R a› hyperplane_eq_Ex
        inner_scaleR_left assms(2))
  moreover have "?c ≠ 0"
    using ‹a' = ?c *⇩R a› assms(3) by fastforce
  ultimately show ?thesis
    by blast
qed

lemma subset_hyperplanes:
  fixes a :: "'a::euclidean_space"
  shows "({x. a ∙ x = b} ⊆ {x. a' ∙ x = b'}) =
         ({x. a ∙ x = b} = {} ∨ {x. a' ∙ x = b'} = UNIV ∨
          {x. a ∙ x = b} = {x. a' ∙ x = b'})"
  (is "?lhs = ?rhs")
proof
  assume *: "?lhs"
  consider
    (a_zero) "a = 0" |
    (a'_zero) "a' = 0" |
    (nonzero) "a ≠ 0" "a' ≠ 0"
    by blast
  then show "?rhs"
  proof (cases)
    case a_zero
    then show ?thesis using * by auto
  next
    case a'_zero
    then show ?thesis using * by force
  next
    case nonzero
    then obtain c where ‹a' = c *⇩R a› ‹b' = c * b›
      using * hyperplane_subset_imp_scaled by blast
    then show ?thesis
      by (smt (verit, ccfv_threshold) Collect_cong inner_scaleR_left
          nonzero(2) scaleR_eq_0_iff vector_space_over_itself.scale_left_imp_eq)
  qed
next
  assume "?rhs"
  then show "?lhs" by blast
qed

end