In this assignment you will perform step-by-step algebraic manipulations involving vectors and vector operations. In doing
so, you will assemble machine-verifiable proofs of algebraic facts.
Your proofs must be automatically verifiable using the proof verifier.
Please submit a single text file
containing your proof scripts for each of the problem parts below.
Working with machine verification can be frustrating; minute operations that are normally implied must often be explicit.
However, the process should familiarize you with common practices of rigorous algebraic reasoning in mathematics: finding, applying,
or expanding definitions to reach a particular formula that represents a desired argument or solution.
- Finish the proof below by solving for a using a sequence of permitted algebraic manipulations.
- Finish the proof below by solving for b in terms of a.
- Finish the proof below to show that [1;2] and [-2;1] are linearly independent.
- Solve for x (the solution is an integer).
- Show that no [x; y] exists satisfying both of the below properties by deriving a contradiction (e.g.,
1 = 0).
- We have shown in lecture that R2, together with vector addition and scalar multiplication, satisfies some of the vector space axioms.
In this problem, you will show that the remaining axioms are satisfied.
- Finish the proof below showing that [0; 0] is a left identity for addition of vectors in R2.
- Finish the proof below showing that [0; 0] is a right identity for addition of vectors in R2.
- Finish the proof below showing that 1 is the identity for scalar multiplication of vectors in R2.
- Finish the proof below showing that the component-wise definition of inversion is consistent with the inversion axiom for vector spaces.
- Finish the proof below showing that the addition of vectors in R2 is associative.
- Finish the proof below showing that the distributive property applies to vector addition and scalar multiplication for R2.
Any point p on the line between vectors u and v can be expressed as a(u-v)+u for some scalar a. In fact, it can also be
expressed as b(u-v)+v for some other scalar b. In this problem, you will prove this fact for R3.
Given some p = a(u-v)+u, find a formula for b in terms of a so that p = b(u-v)+v. Add this formula to the beginning
of the proof (after
a = ) and then complete the proof.
The verifier's library contains
a variety of derived algebraic properties for R and R3 in addition to the vector space axioms for R3. Look over them
to see which might be useful.