Theory Comments

Up to index of Isabelle/HOL/HOL-Algebra/Vector_Spaces

theory Comments
imports Examples
theory Comments
imports Examples
begin

section{*Comments*}

context vector_space
begin

text{*Now some properties of vector spaces.*}
text{*Halmos proposes some exercises, but most of them are properties already proved in abelian groups, rings...
  so they are in the library and using the inheritance of properties provided by locales we obtain them for vector spaces. 
  Lemmas in which the scalar product appears need to be proved and we make it here.*}

text{*We have two zeros: @{term "\<zero>V"} and @{term "\<zero>K"}. We need to define separately the closure property
  in order to avoid confusions. Alternatively, we could specify the structure writing @{text "V.zero_closed"} and @{text "K.zero_closed"}.*}

lemma zeroV_closed: "\<zero>V ∈ carrier V"
using V.zero_closed .

lemma zeroK_closed: "\<zero>K ∈ carrier K"
  using K.zero_closed .

text{*A variation of @{text r_neg} (@{thm r_neg[no_vars]}):*}
lemma r_neg': 
  assumes x_in_V: "x ∈ carrier V" 
  shows "x \<ominus>V x=\<zero>V"
proof -
  have "\<zero>V = x ⊕ V \<ominus>V x"
    using V.r_neg [OF x_in_V, symmetric] .
  also have "…=x \<ominus>V x" using a_minus_def [symmetric, OF x_in_V x_in_V] .
  finally show ?thesis by simp
qed

(*lemma r_zeroV:
  assumes x_in_V: "x ∈ carrier V" 
  shows "x ⊕V \<zero>V =x"
proof -
  have "x ⊕V \<zero>V = \<zero>V ⊕V x"
    using V.a_comm [OF x_in_V V.zero_closed] .
  also have "… = x"
    using V.l_zero [OF x_in_V] .
  finally show ?thesis .
qed

lemma minus_zeroV: "\<ominus>V \<zero>V = \<zero>V"
using V.minus_zero .*)

text{*We want to prove that @{term "a · \<zero>V = \<zero>V"}. First of all, we prove
  some auxiliary lemmas: *}

lemma mult_zero_descomposition [simp]:
  assumes a_in_K: "a ∈ carrier K "
  shows "a · \<zero>V ⊕V a · \<zero>V = a · \<zero>V"
proof -
  have "a· \<zero>V =a· (\<zero>V ⊕V \<zero>V)"
    using V.r_zero [symmetric, OF V.zero_closed] by simp
  also 
  have "…=a· \<zero> V ⊕ V a· \<zero> V"
    using add_mult_distrib1 [OF V.zero_closed V.zero_closed a_in_K] by simp
  finally show ?thesis by rule
qed

lemma plus_minus_assoc:
  assumes x_in_V: "x ∈ carrier V" 
  and y_in_V: "y ∈ carrier V" and z_in_V: "z ∈ carrier V" 
  shows "x ⊕V y \<ominus>V z = x ⊕V (y \<ominus>V z)"
proof -
  have minus_z_in_V:"\<ominus>V z ∈ carrier V"
    using V.a_inv_closed [OF z_in_V] . 
  have "x ⊕V y \<ominus>V z = x ⊕V y ⊕V \<ominus>V z"
    using a_minus_def [of "x ⊕V y", OF _ z_in_V]
    using V.a_closed [OF x_in_V y_in_V] .
  also have "x ⊕V y ⊕V \<ominus>V z = x ⊕V (y ⊕V \<ominus>V z)"
    using V.a_assoc [OF x_in_V y_in_V minus_z_in_V] .
  also have "… = x ⊕V (y \<ominus>V z)"
    unfolding a_minus_def [symmetric, OF y_in_V z_in_V] ..
  finally show ?thesis by simp
qed

text{*Now we can complete theorem that we want to prove. It corresponds with exercise 1C in section 4 in Halmos.*}
lemma scalar_mult_zeroV_is_zeroV: 
  assumes a_in_K:"a ∈ carrier K" 
  shows "a · \<zero>V = \<zero>V"
proof -
  have mclosed: "a· \<zero> V  ∈ carrier V"
    using mult_closed [OF V.zero_closed a_in_K] . 
  have "a · \<zero>V = a· \<zero>V ⊕V a· \<zero>V" 
    using mult_zero_descomposition [OF a_in_K] by simp
  hence "a · \<zero>V \<ominus>V a · \<zero>V = a· \<zero>V ⊕V a· \<zero>V \<ominus>V a · \<zero>V" 
    using mclosed by simp
  thus ?thesis
    unfolding plus_minus_assoc [OF mclosed mclosed mclosed]
    unfolding r_neg' [OF mclosed]
    using V.r_zero [OF  mclosed] by simp
qed
 

text{*We apply a similar reasoning to prove that @{term "\<zero>K · x = \<zero>V"} (this corresponds with exercise 1D in section 4 in Halmos):*}
lemma mult_zero_descomposition2:
  assumes x_in_V: "x ∈ carrier V"
  shows "\<zero>K · x ⊕V \<zero>K · x = \<zero>K · x"
proof -
  have "\<zero>K · x = (\<zero>K ⊕K \<zero>K)· x"
    using zeroK_closed
    using K.r_zero [OF zeroK_closed ,symmetric] by simp
  from this show ?thesis
    using add_mult_distrib2 [OF x_in_V zeroK_closed zeroK_closed,symmetric]
    by simp
qed

text{*The exercise 1D in section 4 in Halmos is proved as follows:*}
lemma zeroK_mult_V_is_zeroV:
  assumes x_in_V: "x ∈ carrier V"
  shows "\<zero>K · x = \<zero>V"
proof -
  have mclosed: "\<zero>K · x ∈ carrier V"
    using mult_closed [OF x_in_V zeroK_closed] .
  have "\<zero>K · x = \<zero>K · x ⊕V \<zero>K · x" 
    using mult_zero_descomposition2 [OF x_in_V,symmetric] .
  hence "\<zero>K · x \<ominus>V \<zero>K · x = \<zero>K · x ⊕V \<zero>K · x \<ominus>V \<zero>K · x" by simp
  thus ?thesis
    unfolding plus_minus_assoc [OF mclosed mclosed mclosed]
    unfolding r_neg' [OF mclosed]
    using V.r_zero [OF mclosed] by simp
qed

text{*Another relevant property permit us to relate the additive inverse of 
  the multiplicative unit with the additive inverse. It corresponds with exercise (1F) in
  section 4 in Halmos.*}
lemma negate_eq:
  assumes x_in_V: "x ∈ carrier V"
  shows "(\<ominus>K  \<one>K) · x = \<ominus>V x"
proof (rule V.minus_equality [symmetric, of "(\<ominus>K  \<one>K) · x" x])
  show "x ∈ carrier V" using x_in_V .
  have minus_oneK_closed: "\<ominus> K \<one> K  ∈ carrier K"
    using K.a_inv_closed [OF K.one_closed] .
  show "\<ominus> \<one> · x ∈ carrier V"
    using mult_closed [OF x_in_V minus_oneK_closed] .
  show "\<ominus>\<one> · x ⊕V x = \<zero>V"
  proof -
    have "\<zero>V = \<zero>K · x"
      using zeroK_mult_V_is_zeroV [symmetric, OF x_in_V] .
    also have "… = (\<ominus>K \<one>K ⊕K \<one>K)· x"
      unfolding K.l_neg [OF K.one_closed ] ..
    also have "… = \<ominus>K \<one> K· x ⊕V \<one> K · x"
      using add_mult_distrib2 [OF x_in_V minus_oneK_closed K.one_closed] .
    also have "… = \<ominus>K \<one> K· x ⊕V x"
      unfolding mult_1 [OF x_in_V] ..
    finally show ?thesis by rule
  qed
qed

text{*The previous property can be proved not only for the multiplicative unit of $\mathbb{K}$ but for every element in its carrier. 
We redo the demonstration (the previous lemma could be proved as a corollary of this):*}
lemma negate_eq2:
  assumes x_in_V: "x ∈ carrier V"
  and a_in_K: "a ∈ carrier K"
  shows "(\<ominus>K a) · x = \<ominus>V (a·x)"
proof(rule V.minus_equality [symmetric, of "(\<ominus>K  a)· x" "a·x"])
  show "a·x ∈ carrier V" using mult_closed[OF x_in_V a_in_K] .
  show "\<ominus> a · x ∈ carrier V"
    using mult_closed [OF x_in_V K.a_inv_closed[OF a_in_K]] .
  show "\<ominus>a·x ⊕V a·x = \<zero>V"
  proof -
    have "\<zero>V = \<zero>K · x"
      using zeroK_mult_V_is_zeroV [symmetric, OF x_in_V] .
    also have "… = (\<ominus>K a⊕K a)· x"
      unfolding K.l_neg [OF a_in_K ] ..
    also have "… = \<ominus>K a· x ⊕V a · x"
      using add_mult_distrib2 
      [OF x_in_V K.a_inv_closed[OF a_in_K] a_in_K] .
    finally show ?thesis by rule
  qed
qed

text{*The next two lemmas prove exercise 1E, which says that the scalar product also satisfies an integral
property (if $a \cdot b=0_V$, either $a=0_{\mathbb{K}}$ or $b=0_V$):*}      
lemma mult_zero_uniq: 
  assumes x_in_V: "x ∈ carrier V" and x_not_zero: "x ≠ \<zero>V" 
  and a_in_K: "a ∈ carrier K" and m_ax_0: "a · x = \<zero>V"
  shows "a = \<zero>K"
proof (rule classical)
  assume a_not_zero: "a ≠ \<zero>K"
  have a_un: "a ∈ Units K"
    using a_not_zero
    using a_in_K
    using K.field_Units by simp
  have inv_a_in_K: "inv a ∈ carrier K"
    using K.Units_inv_closed [OF a_un] .
  have "x = (inv a ⊗ a)· x"
    using K.Units_l_inv [OF a_un]
    using mult_1 [OF x_in_V]
    by simp
  also have "…= inv a · (a · x)"
    using mult_assoc [OF x_in_V inv_a_in_K a_in_K] .
  also have "…= inv a · \<zero>V" using m_ax_0 by simp
  also have "…= \<zero>V"
    using scalar_mult_zeroV_is_zeroV [OF inv_a_in_K] .
  finally have "x = \<zero>V" .
  with x_not_zero show "a=\<zero>K" by contradiction
qed


lemma integral: 
  assumes x_in_V: "x∈ carrier V" 
  and a_in_K: "a ∈ carrier K" 
  and m_ax_0: "a · x= \<zero>V"
  shows "a = \<zero>K | x=\<zero>V"
proof (cases "x ≠ \<zero>V")
  case False show ?thesis using False by simp
next
  case True
  note x_not_zero = True
  show ?thesis
  proof (cases "a ≠ \<zero>K")
    case False show ?thesis using False by simp
  next
    case True
    note a_not_zero=True
    show ?thesis
      using mult_zero_uniq [OF x_in_V x_not_zero a_in_K m_ax_0]
      using a_not_zero by contradiction
  qed
qed

text{*We present here some other properties which don't appear in Halmos but that will be useful in our development.
For instance, distributivity of substraction with respect to the scalar product:*}

lemma diff_mult_distrib1: 
  assumes x_in_V: "x∈ carrier V" 
  and y_in_V: "y ∈ carrier V" 
  and a_in_K: "a ∈ carrier K" 
  shows "a · (x \<ominus>V y) = a · x \<ominus>V a · y"
proof -
  have minus_y_in_V: "\<ominus>V y ∈ carrier V"
    using V.a_inv_closed [OF y_in_V] .
  have minus_one_in_K: "\<ominus>K \<one> ∈ carrier K"
    using K.a_inv_closed[OF K.one_closed] .
  have mclosed: "a · y ∈ carrier V" 
    using mult_closed [OF y_in_V a_in_K] .
  have mclosed2: "a · x ∈ carrier V" 
    using mult_closed [OF x_in_V a_in_K] .
  have "a · (x \<ominus>V y)=a · (x ⊕V  \<ominus>V y)" 
    using a_minus_def[OF x_in_V y_in_V] by simp
  also have "…= a · x ⊕ V a · (\<ominus>V y)" 
    using add_mult_distrib1 [OF x_in_V minus_y_in_V a_in_K] .
  also have "…= a · x ⊕ V a · (\<ominus>K \<one>K · y)" 
    using negate_eq [OF y_in_V] by simp
  also have "…= a · x ⊕ V (a ⊗K (\<ominus>K \<one>K))· y" 
    using mult_assoc [OF y_in_V a_in_K minus_one_in_K ,symmetric] 
    by simp
  also have "…= a · x ⊕ V ((\<ominus>K \<one>K)⊗K a)· y" 
    using K.m_comm [OF minus_one_in_K a_in_K] by simp
  also have "…= a · x ⊕ V (\<ominus>K \<one>K) · a · y" 
    using mult_assoc [OF y_in_V minus_one_in_K a_in_K] by simp
  also have "…= a · x ⊕ V \<ominus>V (a · y)" 
    using negate_eq [OF mclosed] by simp
  also have "…= a · x \<ominus>V a· y" 
    using a_minus_def [OF mclosed2 mclosed,symmetric] .
  finally show ?thesis .
qed

text{*The following result proves distributivity of substraction (of $\mathbb{K}$) with respect to the scalar product:*}
lemma diff_mult_distrib2: 
  assumes x_in_V: "x∈ carrier V" 
  and a_in_K: "a ∈ carrier K" 
  and b_in_K: "b ∈ carrier K"
  shows "(a \<ominus>K b) · x = a·x \<ominus>V b·x"
proof -
  have minus_b_in_K: "\<ominus>K b ∈ carrier K" 
    using K.a_inv_closed [OF b_in_K] .
  have bx_in_V: "b·x ∈  carrier V" 
    using mult_closed [OF x_in_V b_in_K] .
  have "(a \<ominus>K b) · x=(a ⊕K \<ominus>K b)·x " 
    using K.minus_eq [OF a_in_K b_in_K] by simp
  also have "…=a·x ⊕V (\<ominus>K b)·x"
    using add_mult_distrib2 [OF x_in_V a_in_K minus_b_in_K] .
  also have "…=a·x ⊕V (\<ominus>K (\<one>K ⊗K b))·x"
    using K.l_one [OF b_in_K] by simp
  also have "…=a·x ⊕V (\<ominus>K \<one>K ⊗K b)·x"
    using K.l_minus [OF K.one_closed b_in_K,symmetric] by simp
  also have "…=a·x ⊕V (\<ominus>K \<one>K)·b·x" 
    using mult_assoc [OF x_in_V K.a_inv_closed[OF K.one_closed] b_in_K] 
    by simp
  also have "…=a·x  ⊕V  \<ominus>V (b·x)" 
    using negate_eq [OF bx_in_V] by simp
  also have "…=a·x \<ominus>V b·x" 
    using a_minus_def[OF mult_closed[OF x_in_V a_in_K] bx_in_V,symmetric] .
  finally show ?thesis by simp
qed

text{*The following result proves that the unary substraction of $\mathbb{K}$ and $V$ is a
  self-cancelling operation by means of the scalar product:*}
lemma minus_mult_cancel: 
  assumes x_in_V: "x ∈ carrier V" and a_in_K:"a∈ carrier K" 
  shows "(\<ominus>K a) · (\<ominus>V x) = a · x" 
proof -
  have "(\<ominus>Ka) · (\<ominus>Vx) = (\<ominus>Ka ⊗ (\<ominus>K\<one>K)) · x" 
    using negate_eq[OF x_in_V] 
      mult_assoc[OF x_in_V K.a_inv_closed[OF a_in_K] 
      K.a_inv_closed[OF K.one_closed]] 
    by auto
  also have "…=(a⊗\<one>) · x" 
    using K.prod_minus [OF a_in_K K.one_closed] by auto
  finally show ?thesis using K.r_one [OF a_in_K] by auto
qed

text{*A result proving that the scalar product is commutative over the elements of $\mathbb{K}$:*}
lemma mult_left_commute: 
  assumes x_in_V: "x ∈ carrier V" 
  and a_in_K: "a∈ carrier K" 
  and b_in_K:"b∈ carrier K"
  shows "a · b · x = b · a · x"
proof -
  have "a·b·x=(a⊗b)·x" 
    using mult_assoc[OF x_in_V a_in_K b_in_K, symmetric] .
  also have "…=(b⊗a)·x" using K.m_comm[OF a_in_K b_in_K] by simp
  finally show ?thesis 
    using mult_assoc[OF x_in_V b_in_K a_in_K] by simp
qed

text{*A result proving that the scalar product is left-cancelling for the elements of $\mathbb{K}$ different from $0$:*}
lemma mult_left_cancel: 
  assumes x_in_V: "x ∈ carrier V" 
  and y_in_V: "y∈carrier V" 
  and a_in_K: "a∈carrier K" 
  and a_not_zero: "a≠\<zero>K"
  shows "(a · x = a · y) = (x = y)"
proof
  assume ax_ay:"a·x=a·y"
  have a_in_Units: "a ∈ Units K" 
    using K.field_Units and a_in_K and a_not_zero by simp
  have "x=\<one>K · x" using mult_1[OF x_in_V, symmetric] .
  also have "…=((inv a)⊗K a)·x" 
    using K.Units_l_inv [OF a_in_Units] by simp
  also have "…=(inv a)· a·x" 
    using mult_assoc[OF x_in_V 
      K.Units_inv_closed[OF a_in_Units] a_in_K] 
    by simp
  also have "…=(inv a)· a·y" using ax_ay by simp
  also have "…=((inv a)⊗K a)·y" 
    using mult_assoc[OF y_in_V K.Units_inv_closed
      [OF a_in_Units] a_in_K] by simp
  also have "…=\<one>K · y"
    using K.Units_l_inv [OF a_in_Units, symmetric] by simp
  finally show "x=y" using mult_1[OF y_in_V] by simp
next
  assume x_y: "x=y"
  then show "a·x=a·y" by simp
qed

text{*A similar result to the previous one but proving that the element of $V$ can be also cancelled:*}
lemma mult_right_cancel: 
  assumes x_in_V: "x ∈ carrier V" 
  and a_in_K: "a ∈ carrier K" 
  and b_in_K: "b∈carrier K" 
  and x_not_zero: "x≠\<zero>V"
  shows "(a · x = b · x) = (a = b)"
proof
  assume ax_by:"a·x=b·x"
  have "(a \<ominus> K b)· x=a·x \<ominus> V b·x" 
    using diff_mult_distrib2[OF x_in_V a_in_K b_in_K] .
  also have "…=a·x \<ominus> V a·x" using ax_by by simp
  also have "…=\<zero>V" 
    using r_neg'[OF mult_closed[OF x_in_V a_in_K]] .
  finally have "(a \<ominus> K b)· x=\<zero>V" by simp
  hence ab_zero: "a \<ominus> K b=\<zero>K" 
    using x_not_zero 
    using integral[OF x_in_V K.minus_closed[OF a_in_K b_in_K]] 
    by simp
  thus "a=b"
   proof -
     have a_min_b: "a ⊕K \<ominus> Kb=\<zero>K" 
       using ab_zero and a_minus_def[OF a_in_K b_in_K] by simp
     have "\<ominus> K(\<ominus> K b)=a" 
       using K.minus_equality
       [OF a_min_b K.a_inv_closed[OF b_in_K] a_in_K] .
     thus ?thesis using K.minus_minus[OF b_in_K] by simp
   qed
next
  assume "a=b"
  then show "a·x=b·x" by simp
qed

end
end