R : Type u_1
V : Type u_2
V' : Type ?u.244339
P : Type u_3
P' : Type ?u.244345
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ x ≠ y → (↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)
R : Type u_1
V : Type u_2
V' : Type ?u.244339
P : Type u_3
P' : Type ?u.244345
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ Sbtw R x (↑(lineMap x y) r) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1
rw [sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right]
R : Type u_1
V : Type u_2
V' : Type ?u.244339
P : Type u_3
P' : Type ?u.244345
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x ≠ y
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1
R : Type u_1
V : Type u_2
V' : Type ?u.244339
P : Type u_3
P' : Type ?u.244345
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ x ≠ y → (↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)
intro hxy
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.244339
P : Type u_3
P' : Type ?u.244345
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x ≠ y
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1
rw [(lineMap_injective R hxy).mem_set_image]