Linear independence and bases: proving an ordered basis of ℝ² by exact elimination, with two counterexamples that separate the two obligations

Goal and scope

In ℝ² let v_1=(1,2), v_2=(3,5), v_3=(1,1), w=(4,7). (1) Prove by exact elimination that (v_1,v_2) is linearly independent; (2) find the coefficients for an arbitrary (p,q), proving span(v_1,v_2)=ℝ², so that (v_1,v_2) is an ordered basis; (3) find the unique coordinates of w; (4) prove that (v_1) is independent but does not span ℝ², while (v_1,v_2,v_3) spans ℝ² but is not independent, and w has more than one representation in it.

Treats only the integer-coordinate vector families of G1, computed by exact rational elimination (MKO assumption a1). The determinant is used only as a cross-check for the ordered square ℝ² family (v_1,v_2), not for non-square families (a2), and the general determinant criterion is not proved. Dimension, change of basis and matrices of linear maps are out of scope. The canonical MKO and its English edition are not changed.

Givens and symbols

• vector_space_axioms
• cartesian_product_def
• eq_congruence
• set_extensionality
• numeric_evaluation

• G1 — V=ℝ² with coordinatewise addition and scalar multiplication. v_1=(1,2), v_2=(3,5), v_3=(1,1), w=(4,7) (MKO assumption a1: finite integer-coordinate vector families).

• v_1=(1,2),\ v_2=(3,5),\ v_3=(1,1) — the given integer vectors
• w=(4,7) — the target vector whose coordinates are sought
• a,b,c — coefficients of linear combinations
• (p,q) — an arbitrary target in ℝ²
• \operatorname{span}(\cdot) — the set of all finite linear combinations
• B=(v_1,v_2),\ B'=(v_1,v_2,v_3) — the ordered basis and the family with too many vectors

Rules and sources

• vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• add_zero · prerequisite — Additive identity: u+0=u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_basis_def · cited — A finite vector family is linearly independent if a weighted sum equal to zero requires every coefficient to be zero. To be a basis of a space V, it must be independent and have span equal to V. Neither obligation replaces the other. · mko-linear-independence-basis
• p_span_def · prerequisite — The span of a finite family (u_i) is the set of all linear combinations Σ a_i u_i (a_i∈ℝ); it is a subset of V.
• L_row_op · lemma — For a system of real equations {E_1, E_2} and any real t: replacing E_2 by E_2−tE_1 gives an equivalent system (the same solution set).
• L_unique_coords · lemma — If (u_1,u_2) is linearly independent and a u_1+b u_2=a' u_1+b' u_2, then a=a' and b=b'.

Main derivation

(u_1,u_2)\ \text{a finite family in}\ V

(u_1,u_2)\ \text{independent}\iff\big(a u_1+b u_2=0\Rightarrow a=b=0\big)

B\ \text{basis of}\ V

B\ \text{independent}\ \land\ \operatorname{span}(B)=V

a(1,2)+b(3,5)=(0,0)

a+3b=0\ \land\ 2a+5b=0

a+3b=0\ \land\ 2a+5b=0

a+3b=0\ \land\ b=0

a+3b=0\ \land\ b=0

a=0\ \land\ b=0

a v_1+b v_2=0

a=b=0:\ (v_1,v_2)\ \text{independent}

a(1,2)+b(3,5)=(p,q)

a=-5p+3q,\ \ b=2p-q

\forall (p,q)\in\mathbb{R}^2:\ (p,q)\in\operatorname{span}(v_1,v_2)

\operatorname{span}(v_1,v_2)=\mathbb{R}^2

(v_1,v_2)\ \text{independent},\ \operatorname{span}(v_1,v_2)=\mathbb{R}^2

B=(v_1,v_2)\ \text{is an ordered basis of}\ \mathbb{R}^2

w=(4,7)

w=1\cdot v_1+1\cdot v_2,\ \ [w]_B=(1,1)\ \text{unique}

\det\begin{pmatrix}1&3\\2&5\end{pmatrix}

1\cdot5-3\cdot2=-1\neq0

(v_1)=((1,2))

(v_1)\ \text{independent, but}\ (1,0)\notin\operatorname{span}(v_1)

B'=(v_1,v_2,v_3)

(p,q)=(-5p+3q)v_1+(2p-q)v_2+0\cdot v_3:\ \operatorname{span}(B')=\mathbb{R}^2

v_3=(1,1)

-2v_1+v_2-v_3=(0,0)\ \text{with nonzero coefficients}

w=1\cdot v_1+1\cdot v_2+0\cdot v_3

w=-1\cdot v_1+2\cdot v_2-1\cdot v_3\ \ (\text{a second representation})

\text{S09, S10, S12, S14, S15}

\text{basis}=\text{independent}\land\text{spanning};\ \text{neither replaces the other}

Substeps and lemmas

E_1:\ \ell_1=0,\quad E_2:\ \ell_2=0

E_1,\ E_2\ \Longleftrightarrow\ E_1,\ \ell_2-t\,\ell_1=0

(2a+5b)-2(a+3b)=0

-b=0\ \Longleftrightarrow\ b=0

a+3b=p\ \land\ 2a+5b=q

a+3b=p\ \land\ b=2p-q

a+3b=p,\ b=2p-q

a=p-3(2p-q)=-5p+3q,\quad b=2p-q

(-5p+3q)(1,2)+(2p-q)(3,5)

(p,q)

a u_1+b u_2=a' u_1+b' u_2

(a-a')u_1+(b-b')u_2=0\ \Rightarrow\ a=a',\ b=b'

-2(1,2)+(3,5)-(1,1)

(-2+3-1,\ -4+5-1)=(0,0)

Reverse audits

• S16 · premise_audit · S09, S12, S14 — Only conjoins conclusions already proved.
• S15 · premise_audit · S14, vector_space_axioms — Adding the zero vector changes nothing; a nontrivial zero combination gives every vector infinitely many representations (add any multiple of it).
• S14.1 · inverse_equivalence · numeric_evaluation, cartesian_product_def — Exact integer computation; both sides are the same vector.
• S14 · premise_audit · S01, quantifier_negation, numeric_evaluation — Refuting independence needs one nontrivial set of coefficients; equivalently, elimination gives rank 2, less than the 3 vectors.
• S13 · premise_audit · S07, p_span_def — Adding vectors cannot shrink the span; only spanning is claimed here, not independence.
• S12 · premise_audit · contradiction, cartesian_product_def — Refuting spanning needs one target outside the span; the two coordinate equations require the same a and may not use different values.
• S11 · premise_audit · numeric_evaluation, S07 — Only a consistency check; the general criterion 'det≠0 ⇔ the columns form a basis' is not proved here and is not used for non-square families.
• S10.1 · premise_audit · S01, vector_space_axioms — Uniqueness rests entirely on independence; for a dependent family S15 shows that representations need not be unique.
• S10 · premise_audit · S07, L_unique_coords, S06 — Existence comes from S07 (spanning) and uniqueness from S06 (independence); the two do different jobs.
• S09 · premise_audit · S06, S08, and_intro_elim — Both obligations are used; S12 and S14 show that neither can be missing.
• S08 · premise_audit · S07, forall_intro, set_extensionality — Spanning is a universal statement over all targets; checking finitely many targets would not suffice, and the formula used here is for arbitrary (p,q).
• S07.3 · inverse_equivalence · distributive, numeric_evaluation — The identities hold for all p, q; N2 and N3 check these degree-1 identities on a sufficient grid.
• S07.2 · inverse_equivalence · eq_replace, distributive — Substitution and moving terms are both reversible.
• S07.1 · inverse_equivalence · L_row_op, neg_mul — The same reversible row operation as in S04, now with an arbitrary real right-hand side (p,q), including (0,0).
• S07 · inverse_equivalence · L_row_op, eq_congruence — Every step is an equivalence, so these coefficients are not only a solution but the only one; S07.3, which follows, is an extra direct check.
• S06 · premise_audit · S05, S01, logic_chain — Only the ⇒ direction is used; independence by itself says nothing about the span, which is proved separately in S08.
• S05 · inverse_equivalence · eq_replace, mul_zero — Backward: a=0, b=0 satisfy a+3b=0.
• S04.2 · inverse_equivalence · distributive, neg_mul — The expansion is an identity; multiplication by −1 is reversible.
• S04.1 · inverse_equivalence · eq_congruence, mul_zero — Both directions are written out; the key is that E_1 is kept, otherwise E_2 could not be recovered.
• S04 · inverse_equivalence · L_row_op, neg_mul — The row operation is reversible (add back twice the first equation), and so is multiplying by −1, so the solution set is unchanged.
• S03 · inverse_equivalence · cartesian_product_def, vector_space_axioms — The equality condition for ordered pairs is itself two-way; coordinatewise operations are fixed by G1.
• S02 · premise_audit · mko_basis_def, p_span_def — Both sides of the conjunction must hold; proving one side does not make a basis.
• S01 · premise_audit · mko_basis_def — Only unfolds the definition; the trivial solution a=b=0 always works, and what must be shown is that there is no other.

Error controls and negative controls

Spanning alone or independence alone is not a basis

The misconception named by the MKO is to call vectors a basis just because they span, or just because they are independent. In S12, (v_1) is independent but does not span; in S14, (v_1,v_2,v_3) spans but is not independent. A basis must pass both obligations (S09).

Keep the original equation during elimination

A row operation is an equivalence only if the equation used for elimination is kept (S04.1). If 2a+5b=0 is replaced by −b=0 and a+3b=0 is dropped, only b=0 remains, suggesting that a is free and wrongly indicating dependence.

Spanning must cover every target

Spanning is a universal statement: only the formula of S07 for arbitrary (p,q) gives span=ℝ². Checking that a few targets (such as w and v_3) are representable does not prove spanning; (v_1) can represent (2,4) and (−1,−2) but not (1,0).

• (v_1,v_2,v_3) spans ℝ², so it is a basis of ℝ² → reject — −2v_1+v_2−v_3=0 is a nontrivial zero combination, so the family is not independent (S14).
• (v_1) is linearly independent, so it is a basis of ℝ² → reject — (1,0) is not in span(v_1) (S12).
• The coordinates of w in (v_1,v_2,v_3) are unique and equal (1,1,0) → reject — (−1,2,−1) also gives w (S15).
• The 'determinant' of the non-square family (v_1,v_2,v_3) is zero, so it does not span ℝ² → reject — A 2×3 matrix has no determinant (MKO assumption a2 uses it only for square ℝ² families), and this family does span ℝ² (S13).

Result and limitations

(v_1,v_2)=((1,2),(3,5)) is linearly independent (elimination gives only the trivial solution), and every (p,q)=(−5p+3q)v_1+(2p−q)v_2, so it spans ℝ² and is an ordered basis; the unique coordinates of w=(4,7) are (1,1); det=−1 serves as a cross-check. (v_1) is independent but (1,0) is not in its span; (v_1,v_2,v_3) spans ℝ² but −2v_1+v_2−v_3=0, and w can also be written −v_1+2v_2−v_3.

• The determinant of S11 is only a cross-check; the general criterion '2×2 determinant nonzero ⇔ the columns form a basis' is not proved here.
• Dimension, change of basis and matrices of linear maps (the MKO's formal next) are out of scope.

Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 3daf790affb7a390725ee178abf97c6c54700877e37d65703477e3327f0019fb
• original source SHA-256: e338f1259740f85df598d8def495be6c4b80bc2cbfa19ac852cf13ab5a744260
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)