proposition: Lemma extension_image_density : forall {Tm: Tarski_neutral_dimensionless} {TmEQD : Tarski_neutral_dimensionless_with_decidable_point_equality Tm} P Q (f : @Tpoint Tn -> @Tpoint Tm), @archimedes_axiom Tm -> line_extension f P Q -> forall A B, Col (f P) (f Q) A -> Col (f P) (f Q) B -> A <> B -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B.
proof: Proof. intros Tm TmEQD P Q f archi HPQ A B; revert P Q A B HPQ. cut(forall P Q A B, line_extension f P Q -> Col (f P) (f Q) A -> Col (f P) (f Q) B -> A <> B -> Lt (f P) (f Q) A B -> Bet (f P) A B -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B). { intros HX P Q A B fPQ HColA HColB HAB. assert (Hf' := fPQ); destruct Hf' as [HPQ [fInj [fBet fCong]]]. assert (HfPfQ : f P <> f Q) by (intro; apply HPQ, fInj; Col). destruct (reach__ex_gradexp_lt (f P) (f Q) A B) as [fQ' [HGrad' HLt]]; auto. destruct (extension_gradexp P Q f fPQ P Q fQ') as [Q' [_ [HGrad]]]; Col. subst fQ'; apply gradexp__grad in HGrad; apply gradexp__grad in HGrad'. assert (HPQ' : P <> Q') by (intro; subst; apply grad112__eq in HGrad; auto). assert (fPQ' : line_extension f P Q') by (apply line_extension_stability with Q; Col). assert (HCols : Col (f P) (f Q') A /\ Col (f P) (f Q') B /\ Col (f P) A B) by (split; [|split]; apply col_transitivity_1 with (f Q); Col). assert (HColX : forall X, Col P Q' X -> Col P Q X) by (intros; apply col_transitivity_1 with Q'; Col). destruct HCols as [HColA' [HColB' HE]]. assert (HH : Bet (f P) A B \/ Bet (f P) B A -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B). { intros [|]; [destruct (HX P Q' A B) as [X]|destruct (HX P Q' B A) as [X]]; Col; [exists X; intuition|apply lt_right_comm, HLt|exists X; intuition]. } destruct HE as [|[|]]; [apply HH; Between..|]. destruct (eq_dec_points (f P) A); [subst; apply HH; Between|]. destruct (eq_dec_points (f P) B); [subst; apply HH; Between|]. exists P; repeat split; finish. } { intros P Q A B fPQ HColA HColB HAB HLt HBet. assert (Hf' := fPQ); destruct Hf' as [HPQ [fInj [fBet fCong]]]. destruct (eq_dec_points (f P) A); [treat_equalities|]. { assert (f P <> f Q) by (intro; apply HPQ, fInj; Col). destruct (or_bet_out (f Q) (f P) B) as [HBet|[HOut|]]; [..|exfalso; Col]; [destruct (segment_construction Q P P Q) as [Q' []]; exists Q'|exists Q]; [assert (f Q' <> f P) by (intro; cut (P = Q'); assert_diffs; finish)|]; repeat split; Col; [| |apply l6_13_1; Le|]; [|intro; subst; destruct HLt; intuition..]. assert (Bet (f Q) (f P) (f Q')) by (apply fBet; Col). assert (Cong (f P) (f Q') (f P) (f Q)) by (apply fCong; Col). apply l6_13_1; [apply l6_2 with (f Q); Between|]. apply le_transitivity with (f P) (f Q); Le. } { cut (forall P Q A B, line_extension f P Q -> A <> B -> Lt (f P) (f Q) A B -> Bet (f P) (f Q) A -> Bet (f P) A B -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B). { intro HX; destruct HColA as [|[]]; [destruct (HX P Q A B) as [X]; Col|..]. { destruct (eq_dec_points (f Q) A); [treat_equalities|exists Q]. { destruct (segment_construction P Q P Q) as [Q' []]; exists Q'. assert (Bet (f P) (f Q) (f Q')) by (apply fBet; Col). assert (Cong (f Q) (f Q') (f P) (f Q)) by (apply fCong; Col). assert (f Q <> f Q') by (assert_diffs; auto). assert (HLt2 : Lt (f Q) (f Q') (f Q) B) by (apply (cong2_lt__lt (f P) (f Q) (f Q) B); Cong). repeat split; Col; [|intro; subst; destruct HLt2; Cong]. apply l6_13_1; Le; apply l6_2 with (f P); Between. } { assert (HLt2 : Lt A (f Q) A B) by (apply le1234_lt__lt with (f P) (f Q); Le). repeat split; Col; [|intro; subst; destruct HLt2; Cong]. apply l6_13_1; Le; apply l6_2 with (f P); Between. } } { destruct (HX Q P A B) as [X]; [..|exists X; repeat split; intuition]; [apply line_extension_symmetry|Between|apply lt_left_comm, HLt|..]; [auto| |apply outer_transitivity_between2 with (f P)]; Between. } } { clear dependent P; clear Q; clear dependent A; clear B. intros P Q A B fPQ HAB HLt HBet1 HBet2. cut (exists C, Grad (f P) (f Q) C /\ Bet A C B /\ C <> A /\ C <> B); [intros [C []]; destruct (extension_grad _ _ _ fPQ P Q C) as [X]; Col; exists X; spliter; subst; auto|]. assert (Hdiff : f P <> f Q) by (intro; destruct fPQ as [? []]; Col). destruct (reach__grad_min (f P) (f Q) A) as [D [E]]; auto; spliter. assert (Bet D A E) by (apply (between_exchange3 (f P)); assumption). exists E; repeat split; [apply grad_stab with D| | |intro; subst E]; auto; [|apply lt__nle in HLt; apply HLt, le_transitivity with D B; spliter; Le]. apply l6_13_1; [destruct (eq_dec_points A D); [subst D|]|]; [apply l6_2 with (f P); assert_diffs|apply l6_2 with D|]; eBetween. apply le_transitivity with D E; Le. apply le_transitivity with (f P) (f Q); Le. } } } Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.completeness GeoCoq.Meta_theory.Continuity.grad GeoCoq.Tarski_dev.Ch08_orthogonality