Parallel lines divide segments proportionally #
theorem
EuclidGeom.divratio_eq_of_para₁₂₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio X A C = EuclidGeom.divratio X B D
theorem
EuclidGeom.divratio_eq_of_para₁₃₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio X C A = EuclidGeom.divratio X D B
theorem
EuclidGeom.divratio_eq_of_para₂₁₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio A X C = EuclidGeom.divratio B X D
theorem
EuclidGeom.divratio_eq_of_para₂₃₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio A C X = EuclidGeom.divratio B D X
theorem
EuclidGeom.divratio_eq_of_para₃₁₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio C X A = EuclidGeom.divratio D X B
theorem
EuclidGeom.divratio_eq_of_para₃₂₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.divratio C A X = EuclidGeom.divratio D B X
theorem
EuclidGeom.divratio_eq_of_para_of_para
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{l₃ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{E : P}
{F : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(he : EuclidGeom.lies_on E l₃)
(hf : EuclidGeom.lies_on F l₃)
(h₁₂ : EuclidGeom.Parallel l₁ l₂)
(h₁₃ : EuclidGeom.Parallel l₁ l₃)
(ne : l₁ ≠ l₂)
(hace : EuclidGeom.Collinear A C E)
(hbdf : EuclidGeom.Collinear B D F)
:
EuclidGeom.divratio A C E = EuclidGeom.divratio B D F
theorem
EuclidGeom.line_inx_lies_on_seg_iff_of_para
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.lies_on X { source := A, target := C } ↔ EuclidGeom.lies_on X { source := B, target := D }
theorem
EuclidGeom.line_inx_lies_int_seg_iff_of_para
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.lies_int X { source := A, target := C } ↔ EuclidGeom.lies_int X { source := B, target := D }
theorem
EuclidGeom.lies_on_seg_line_inx_iff_of_para
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.lies_on A { source := C, target := X } ↔ EuclidGeom.lies_on B { source := D, target := X }
theorem
EuclidGeom.lies_int_seg_line_inx_iff_of_para
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₂)
(hd : EuclidGeom.lies_on D l₂)
(h : EuclidGeom.Parallel l₁ l₂)
(ne : l₁ ≠ l₂)
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
:
EuclidGeom.lies_int A { source := C, target := X } ↔ EuclidGeom.lies_int B { source := D, target := X }
theorem
EuclidGeom.divratio_eq_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
(h : EuclidGeom.Parallel (LIN A B) (LIN C D))
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.divratio X A C = EuclidGeom.divratio X B D
theorem
EuclidGeom.divratio_eq_of_para_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{E : P}
{F : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
[EuclidGeom.PtNe E F]
(habcd : EuclidGeom.Parallel (LIN A B) (LIN C D))
(habef : EuclidGeom.Parallel (LIN A B) (LIN E F))
(hace : EuclidGeom.Collinear A C E)
(hbdf : EuclidGeom.Collinear B D F)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.divratio A C E = EuclidGeom.divratio B D F
theorem
EuclidGeom.line_inx_lies_on_seg_iff_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
(h : EuclidGeom.Parallel (LIN A B) (LIN C D))
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.lies_on X { source := A, target := C } ↔ EuclidGeom.lies_on X { source := B, target := D }
theorem
EuclidGeom.line_inx_lies_int_seg_iff_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
(h : EuclidGeom.Parallel (LIN A B) (LIN C D))
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.lies_int X { source := A, target := C } ↔ EuclidGeom.lies_int X { source := B, target := D }
theorem
EuclidGeom.lies_on_seg_line_inx_iff_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
(h : EuclidGeom.Parallel (LIN A B) (LIN C D))
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.lies_on A { source := C, target := X } ↔ EuclidGeom.lies_on B { source := D, target := X }
theorem
EuclidGeom.lies_int_seg_line_inx_iff_of_para'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
[EuclidGeom.PtNe A B]
[EuclidGeom.PtNe C D]
(h : EuclidGeom.Parallel (LIN A B) (LIN C D))
(hxac : EuclidGeom.Collinear A C X)
(hxbd : EuclidGeom.Collinear B D X)
(hn : LIN A B ≠ LIN C D)
:
EuclidGeom.lies_int A { source := C, target := X } ↔ EuclidGeom.lies_int B { source := D, target := X }