# Theory Vector_Space

theory Vector_Space
imports Bounds
```(*  Title:      HOL/Hahn_Banach/Vector_Space.thy
Author:     Gertrud Bauer, TU Munich
*)

section ‹Vector spaces›

theory Vector_Space
imports Complex_Main Bounds
begin

subsection ‹Signature›

text ‹
For the definition of real vector spaces a type @{typ 'a} of the sort
‹{plus, minus, zero}› is considered, on which a real scalar multiplication
‹⋅› is declared.
›

consts
prod :: "real ⇒ 'a::{plus,minus,zero} ⇒ 'a"  (infixr "⋅" 70)

subsection ‹Vector space laws›

text ‹
A ∗‹vector space› is a non-empty set ‹V› of elements from @{typ 'a} with the
following vector space laws: The set ‹V› is closed under addition and scalar
multiplication, addition is associative and commutative; ‹- x› is the
inverse of ‹x› wrt.\ addition and ‹0› is the neutral element of addition.
Addition and multiplication are distributive; scalar multiplication is
associative and the real number ‹1› is the neutral element of scalar
multiplication.
›

locale vectorspace =
fixes V
assumes non_empty [iff, intro?]: "V ≠ {}"
and add_closed [iff]: "x ∈ V ⟹ y ∈ V ⟹ x + y ∈ V"
and mult_closed [iff]: "x ∈ V ⟹ a ⋅ x ∈ V"
and add_assoc: "x ∈ V ⟹ y ∈ V ⟹ z ∈ V ⟹ (x + y) + z = x + (y + z)"
and add_commute: "x ∈ V ⟹ y ∈ V ⟹ x + y = y + x"
and diff_self [simp]: "x ∈ V ⟹ x - x = 0"
and add_zero_left [simp]: "x ∈ V ⟹ 0 + x = x"
and add_mult_distrib1: "x ∈ V ⟹ y ∈ V ⟹ a ⋅ (x + y) = a ⋅ x + a ⋅ y"
and add_mult_distrib2: "x ∈ V ⟹ (a + b) ⋅ x = a ⋅ x + b ⋅ x"
and mult_assoc: "x ∈ V ⟹ (a * b) ⋅ x = a ⋅ (b ⋅ x)"
and mult_1 [simp]: "x ∈ V ⟹ 1 ⋅ x = x"
and negate_eq1: "x ∈ V ⟹ - x = (- 1) ⋅ x"
and diff_eq1: "x ∈ V ⟹ y ∈ V ⟹ x - y = x + - y"
begin

lemma negate_eq2: "x ∈ V ⟹ (- 1) ⋅ x = - x"
by (rule negate_eq1 [symmetric])

lemma negate_eq2a: "x ∈ V ⟹ -1 ⋅ x = - x"
by (simp add: negate_eq1)

lemma diff_eq2: "x ∈ V ⟹ y ∈ V ⟹ x + - y = x - y"
by (rule diff_eq1 [symmetric])

lemma diff_closed [iff]: "x ∈ V ⟹ y ∈ V ⟹ x - y ∈ V"
by (simp add: diff_eq1 negate_eq1)

lemma neg_closed [iff]: "x ∈ V ⟹ - x ∈ V"
by (simp add: negate_eq1)

"x ∈ V ⟹ y ∈ V ⟹ z ∈ V ⟹ x + (y + z) = y + (x + z)"
proof -
assume xyz: "x ∈ V"  "y ∈ V"  "z ∈ V"
then have "x + (y + z) = (x + y) + z"
by (simp only: add_assoc)
also from xyz have "… = (y + x) + z" by (simp only: add_commute)
also from xyz have "… = y + (x + z)" by (simp only: add_assoc)
finally show ?thesis .
qed

text ‹
The existence of the zero element of a vector space follows from the
non-emptiness of carrier set.
›

lemma zero [iff]: "0 ∈ V"
proof -
from non_empty obtain x where x: "x ∈ V" by blast
then have "0 = x - x" by (rule diff_self [symmetric])
also from x x have "… ∈ V" by (rule diff_closed)
finally show ?thesis .
qed

lemma add_zero_right [simp]: "x ∈ V ⟹  x + 0 = x"
proof -
assume x: "x ∈ V"
from this and zero have "x + 0 = 0 + x" by (rule add_commute)
also from x have "… = x" by (rule add_zero_left)
finally show ?thesis .
qed

lemma mult_assoc2: "x ∈ V ⟹ a ⋅ b ⋅ x = (a * b) ⋅ x"
by (simp only: mult_assoc)

lemma diff_mult_distrib1: "x ∈ V ⟹ y ∈ V ⟹ a ⋅ (x - y) = a ⋅ x - a ⋅ y"
by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)

lemma diff_mult_distrib2: "x ∈ V ⟹ (a - b) ⋅ x = a ⋅ x - (b ⋅ x)"
proof -
assume x: "x ∈ V"
have " (a - b) ⋅ x = (a + - b) ⋅ x"
by simp
also from x have "… = a ⋅ x + (- b) ⋅ x"
also from x have "… = a ⋅ x + - (b ⋅ x)"
by (simp add: negate_eq1 mult_assoc2)
also from x have "… = a ⋅ x - (b ⋅ x)"
by (simp add: diff_eq1)
finally show ?thesis .
qed

lemmas distrib =
diff_mult_distrib1 diff_mult_distrib2

text ‹┉ Further derived laws:›

lemma mult_zero_left [simp]: "x ∈ V ⟹ 0 ⋅ x = 0"
proof -
assume x: "x ∈ V"
have "0 ⋅ x = (1 - 1) ⋅ x" by simp
also have "… = (1 + - 1) ⋅ x" by simp
also from x have "… =  1 ⋅ x + (- 1) ⋅ x"
also from x have "… = x + (- 1) ⋅ x" by simp
also from x have "… = x + - x" by (simp add: negate_eq2a)
also from x have "… = x - x" by (simp add: diff_eq2)
also from x have "… = 0" by simp
finally show ?thesis .
qed

lemma mult_zero_right [simp]: "a ⋅ 0 = (0::'a)"
proof -
have "a ⋅ 0 = a ⋅ (0 - (0::'a))" by simp
also have "… =  a ⋅ 0 - a ⋅ 0"
by (rule diff_mult_distrib1) simp_all
also have "… = 0" by simp
finally show ?thesis .
qed

lemma minus_mult_cancel [simp]: "x ∈ V ⟹ (- a) ⋅ - x = a ⋅ x"
by (simp add: negate_eq1 mult_assoc2)

lemma add_minus_left_eq_diff: "x ∈ V ⟹ y ∈ V ⟹ - x + y = y - x"
proof -
assume xy: "x ∈ V"  "y ∈ V"
then have "- x + y = y + - x" by (simp add: add_commute)
also from xy have "… = y - x" by (simp add: diff_eq1)
finally show ?thesis .
qed

lemma add_minus [simp]: "x ∈ V ⟹ x + - x = 0"
by (simp add: diff_eq2)

lemma add_minus_left [simp]: "x ∈ V ⟹ - x + x = 0"

lemma minus_minus [simp]: "x ∈ V ⟹ - (- x) = x"
by (simp add: negate_eq1 mult_assoc2)

lemma minus_zero [simp]: "- (0::'a) = 0"
by (simp add: negate_eq1)

lemma minus_zero_iff [simp]:
assumes x: "x ∈ V"
shows "(- x = 0) = (x = 0)"
proof
from x have "x = - (- x)" by simp
also assume "- x = 0"
also have "- … = 0" by (rule minus_zero)
finally show "x = 0" .
next
assume "x = 0"
then show "- x = 0" by simp
qed

lemma add_minus_cancel [simp]: "x ∈ V ⟹ y ∈ V ⟹ x + (- x + y) = y"

lemma minus_add_cancel [simp]: "x ∈ V ⟹ y ∈ V ⟹ - x + (x + y) = y"

lemma minus_add_distrib [simp]: "x ∈ V ⟹ y ∈ V ⟹ - (x + y) = - x + - y"

lemma diff_zero [simp]: "x ∈ V ⟹ x - 0 = x"
by (simp add: diff_eq1)

lemma diff_zero_right [simp]: "x ∈ V ⟹ 0 - x = - x"
by (simp add: diff_eq1)

assumes x: "x ∈ V" and y: "y ∈ V" and z: "z ∈ V"
shows "(x + y = x + z) = (y = z)"
proof
from y have "y = 0 + y" by simp
also from x y have "… = (- x + x) + y" by simp
also from x y have "… = - x + (x + y)" by (simp add: add.assoc)
also assume "x + y = x + z"
also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)
also from x z have "… = z" by simp
finally show "y = z" .
next
assume "y = z"
then show "x + y = x + z" by (simp only:)
qed

"x ∈ V ⟹ y ∈ V ⟹ z ∈ V ⟹ (y + x = z + x) = (y = z)"

"x ∈ V ⟹ y ∈ V ⟹ x' ∈ V ⟹ y' ∈ V ⟹ z ∈ V
⟹ x + y = x' + y' ⟹ x + (y + z) = x' + (y' + z)"
by (simp only: add_assoc [symmetric])

lemma mult_left_commute: "x ∈ V ⟹ a ⋅ b ⋅ x = b ⋅ a ⋅ x"
by (simp add: mult.commute mult_assoc2)

lemma mult_zero_uniq:
assumes x: "x ∈ V"  "x ≠ 0" and ax: "a ⋅ x = 0"
shows "a = 0"
proof (rule classical)
assume a: "a ≠ 0"
from x a have "x = (inverse a * a) ⋅ x" by simp
also from ‹x ∈ V› have "… = inverse a ⋅ (a ⋅ x)" by (rule mult_assoc)
also from ax have "… = inverse a ⋅ 0" by simp
also have "… = 0" by simp
finally have "x = 0" .
with ‹x ≠ 0› show "a = 0" by contradiction
qed

lemma mult_left_cancel:
assumes x: "x ∈ V" and y: "y ∈ V" and a: "a ≠ 0"
shows "(a ⋅ x = a ⋅ y) = (x = y)"
proof
from x have "x = 1 ⋅ x" by simp
also from a have "… = (inverse a * a) ⋅ x" by simp
also from x have "… = inverse a ⋅ (a ⋅ x)"
by (simp only: mult_assoc)
also assume "a ⋅ x = a ⋅ y"
also from a y have "inverse a ⋅ … = y"
by (simp add: mult_assoc2)
finally show "x = y" .
next
assume "x = y"
then show "a ⋅ x = a ⋅ y" by (simp only:)
qed

lemma mult_right_cancel:
assumes x: "x ∈ V" and neq: "x ≠ 0"
shows "(a ⋅ x = b ⋅ x) = (a = b)"
proof
from x have "(a - b) ⋅ x = a ⋅ x - b ⋅ x"
by (simp add: diff_mult_distrib2)
also assume "a ⋅ x = b ⋅ x"
with x have "a ⋅ x - b ⋅ x = 0" by simp
finally have "(a - b) ⋅ x = 0" .
with x neq have "a - b = 0" by (rule mult_zero_uniq)
then show "a = b" by simp
next
assume "a = b"
then show "a ⋅ x = b ⋅ x" by (simp only:)
qed

lemma eq_diff_eq:
assumes x: "x ∈ V" and y: "y ∈ V" and z: "z ∈ V"
shows "(x = z - y) = (x + y = z)"
proof
assume "x = z - y"
then have "x + y = z - y + y" by simp
also from y z have "… = z + - y + y"
by (simp add: diff_eq1)
also have "… = z + (- y + y)"
by (rule add_assoc) (simp_all add: y z)
also from y z have "… = z + 0"
by (simp only: add_minus_left)
also from z have "… = z"
by (simp only: add_zero_right)
finally show "x + y = z" .
next
assume "x + y = z"
then have "z - y = (x + y) - y" by simp
also from x y have "… = x + y + - y"
by (simp add: diff_eq1)
also have "… = x + (y + - y)"
by (rule add_assoc) (simp_all add: x y)
also from x y have "… = x" by simp
finally show "x = z - y" ..
qed

assumes x: "x ∈ V" and y: "y ∈ V" and xy: "x + y = 0"
shows "x = - y"
proof -
from x y have "x = (- y + y) + x" by simp
also from x y have "… = - y + (x + y)" by (simp add: add_ac)
also note xy
also from y have "- y + 0 = - y" by simp
finally show "x = - y" .
qed

assumes x: "x ∈ V" and y: "y ∈ V" and xy: "x - y = 0"
shows "x = y"
proof -
from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)
with _ _ have "x = - (- y)"
by (rule add_minus_eq_minus) (simp_all add: x y)
with x y show "x = y" by simp
qed

assumes vs: "a ∈ V"  "b ∈ V"  "c ∈ V"  "d ∈ V"
and eq: "a + b = c + d"
shows "a - c = d - b"
proof -
from assms have "- c + (a + b) = - c + (c + d)"
also have "… = d" using ‹c ∈ V› ‹d ∈ V› by (rule minus_add_cancel)
finally have eq: "- c + (a + b) = d" .
from vs have "a - c = (- c + (a + b)) + - b"
also from vs eq have "…  = d + - b"
also from vs have "… = d - b" by (simp add: diff_eq2)
finally show "a - c = d - b" .
qed

assumes vs: "x ∈ V"  "y ∈ V"  "z ∈ V"  "u ∈ V"
shows "(x + (y + z) = y + u) = (x + z = u)"
proof
from vs have "x + z = - y + y + (x + z)" by simp
also have "… = - y + (y + (x + z))"
also from vs have "y + (x + z) = x + (y + z)"
also assume "x + (y + z) = y + u"
also from vs have "- y + (y + u) = u" by simp
finally show "x + z = u" .
next
assume "x + z = u"
with vs show "x + (y + z) = y + u"
by (simp only: add_left_commute [of x])
qed

assumes vs: "x ∈ V"  "y ∈ V"  "z ∈ V"
shows "(x + (y + z) = y) = (x = - z)"
proof
assume "x + (y + z) = y"
with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)
with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)
with vs show "x = - z" by (simp add: add_minus_eq_minus)
next
assume eq: "x = - z"
then have "x + (y + z) = - z + (y + z)" by simp
also have "… = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)
also from vs have "… = y"  by simp
finally show "x + (y + z) = y" .
qed

end

end
```