# vecspaces_verybasic.v

Section MAIN.
Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Field_facts.
Require Export equal_syntax.
Require Export more_syntax.
Require Export Module_facts.

• The definition of a vectorspace, and some very easy lemma's. This file is basically the book's Section 1.2

Section vecfielddef.

Definition vectorspace (F : field) : Type := MODULE F.
Definition VECSP (F : field) : category :=
full_subcat (fun V : vectorspace FV:MODULE F).

End vecfielddef.

Section jargon.
Variable F : field.
Variable V : vectorspace F.
Definition carrier := module_carrier.
Definition scalar_mult (a : F) (x : V) : V := a mX x.
• Since scalar_mult is exactly the same as module_mult, ie mX, we will continue to use that notation instead
Definition scalar_mult_comp :
(x x' : F) (y y' : carrier V),
x =' x' in _ y =' y' in _ x mX y =' x' mX y' in _ :=
MODULE_comp (R:=F) (Mod:=V).
Definition one_acts_as_unit : x : carrier V, one mX x =' x in _ :=
MODULE_unit_l (R:=F) (Mod:=V).
Definition quasi_associativity :
(a b : F) (x : carrier V), (a rX b) mX x =' a mX b mX x in _ :=
MODULE_assoc (R:=F) (Mod:=V).
Definition distributivity :
(a : F) (x y : carrier V), a mX (x +' y) =' a mX x +' a mX y in _ :=
MODULE_dist_l (R:=F) (Mod:=V).
Definition distributivity' :
(a b : F) (x : carrier V), (a +' b) mX x =' a mX x +' b mX x in _ :=
MODULE_dist_r (R:=F) (Mod:=V).
End jargon.

Variable F : field.
Variable V : vectorspace F.
Hint Unfold carrier module_carrier.
Hint Resolve scalar_mult_comp distributivity distributivity': algebra.

Section Lemmas1.
• ; the corollaries are immediate by construction/definition
Lemma vector_cancellation :
x y z : V, x +' z =' y +' z in _ x =' y in _.
intros.
apply GROUP_reg_right with z; auto with algebra.
Qed.

• , split into several separate lemmas
Lemma Zero_times_a_vector_gives_zero :
v : V, (zero F) mX v =' (zero V) in _.
auto with algebra.
Qed.

Lemma a_scalar_times_zero_gives_zero :
f : F, f mX (zero V) =' (zero V) in _.
auto with algebra.
Qed.

Section Lemmas1_2.

Lemma Mince_minus1 :
(f : F) (v : V), (min f) mX v =' (min f mX v) in _.
auto with algebra.
Qed.

Lemma Mince_minus2 :
(f : F) (v : V), (min f mX v) =' f mX (min v) in _.
auto with algebra.
Qed.

Lemma Mince_minus3 :
(f : F) (v : V), (min f) mX v =' f mX (min v) in _.
intros.
apply Trans with (min f mX v); auto with algebra.
Qed.

Lemma vecspace_op_reg_l :
(f : F) (v : V),
¬ f =' (zero F) in _ f mX v =' (zero V) in _ v =' (zero V) in _.
intros.
apply Trans with (one mX v); auto with algebra.
apply Trans with ((field_inverse f rX f) mX v).
apply MODULE_comp; auto with algebra.
apply Sym; auto with algebra.
apply Trans with (field_inverse f mX f mX v); auto with algebra.
apply Trans with (field_inverse f mX (zero V)); auto with algebra.
Qed.

End Lemmas1_2.
End Lemmas1.

End MAIN.

Hint Resolve vector_cancellation Zero_times_a_vector_gives_zero
a_scalar_times_zero_gives_zero Mince_minus1 Mince_minus2 Mince_minus3:
algebra.