Theorems · Theorem · geometry

exists_eq_smul_of_parallel

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  p₂ ∉ line[k, p₁, p₃] →
    line[k, p₁, p₂].Parallel line[k, p₄, p₅] →
      line[k, p₅, p₆].direction ≤ line[k, p₂, p₃].direction →
        line[k, p₆, p₄].direction ≤ line[k, p₃, p₁].direction →
          ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Given two triples of non-collinear points, if the lines determined by corresponding pairs of points are parallel, then the vectors between corresponding pairs of points are all related by the same nonzero scale factor. (The formal statement is slightly more general.)

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Cited by

1 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleAddTorsor