English
The lineMap of slopes expresses the affine combination property: lineMap (slope f a b) (slope f b c) ((c - b)/(c - a)) = slope f a c, given a ≠ c.
Русский
LineMap наклонов выражает аффинную комбинацию: lineMap (slope f a b) (slope f b c) ((c - b)/(c - a)) = slope f a c при a ≠ c.
LaTeX
$$$\mathrm{lineMap}(\operatorname{slope} f a b, \operatorname{slope} f b c)\left(\frac{c-b}{c-a}\right) = \operatorname{slope} f a c$$$
Lean4
/-- `slope f a c` is an affine combination of `slope f a b` and `slope f b c`. This version uses
`lineMap` to express this property. -/
theorem lineMap_slope_slope_sub_div_sub (f : k → PE) (a b c : k) (h : a ≠ c) :
lineMap (slope f a b) (slope f b c) ((c - b) / (c - a)) = slope f a c :=
by
simp only [lineMap_apply_module, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c, add_left_inj]
match_scalars
field_simp [sub_ne_zero.2 h.symm]
ring
