# Library GeoCoq.Elements.OriginalProofs.lemma_linereflectionisometry

Require Export GeoCoq.Elements.OriginalProofs.proposition_10.

Require Export GeoCoq.Elements.OriginalProofs.lemma_rightreverse.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearright.

Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_linereflectionisometry :

∀ A B C D E F,

Per B A C → Per A B D → BetS C A E → BetS D B F → Cong A C A E → Cong B D B F →

Cong C D E F.

Proof.

intros.

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS B A H ∧ Cong B A H A ∧ Cong B C H C ∧ neq A C)) by (conclude_def Per );destruct Tf as [H];spliter.

let Tf:=fresh in

assert (Tf:∃ G, (BetS A B G ∧ Cong A B G B ∧ Cong A D G D ∧ neq B D)) by (conclude_def Per );destruct Tf as [G];spliter.

assert (neq A B) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ M, (BetS A M B ∧ Cong M A M B)) by (conclude proposition_10);destruct Tf as [M];spliter.

assert (Per D B A) by (conclude lemma_8_2).

assert (neq B A) by (conclude lemma_inequalitysymmetric).

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Out B A M) by (conclude lemma_ray4).

assert (Per D B M) by (conclude lemma_8_3).

assert (nCol D B M) by (conclude lemma_rightangleNC).

assert (¬ eq D M).

{

intro.

assert (Col D B M) by (conclude_def Col ).

contradict.

}

assert (neq M D) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ R, (BetS D M R ∧ Cong M R M D)) by (conclude postulate_extension);destruct Tf as [R];spliter.

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Cong D B B F) by (forward_using lemma_congruenceflip).

assert (Cong D A F A) by (conclude lemma_rightreverse).

assert (Cong F A D A) by (conclude lemma_congruencesymmetric).

assert (Col D B F) by (conclude_def Col ).

assert (Col B D F) by (forward_using lemma_collinearorder).

assert (neq B F) by (forward_using lemma_betweennotequal).

assert (neq F B) by (conclude lemma_inequalitysymmetric).

assert (Per D B A) by (conclude lemma_8_2).

assert (Per F B A) by (conclude lemma_collinearright).

assert (Per F B M) by (conclude lemma_8_3).

assert (nCol F B M) by (conclude lemma_rightangleNC).

assert (nCol D B M) by (conclude lemma_rightangleNC).

assert (¬ eq F M).

{

intro.

assert (Col F B M) by (conclude_def Col ).

contradict.

}

assert (neq M F) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS F M Q ∧ Cong M Q M F)) by (conclude postulate_extension);destruct Tf as [Q];spliter.

assert (Cong M D M R) by (conclude lemma_congruencesymmetric).

assert (Cong D M M R) by (forward_using lemma_congruenceflip).

assert (Midpoint D M R) by (conclude_def Midpoint ).

assert (Cong M F M Q) by (conclude lemma_congruencesymmetric).

assert (Cong F M M Q) by (forward_using lemma_congruenceflip).

assert (Midpoint F M Q) by (conclude_def Midpoint ).

assert (Cong M B M A) by (conclude lemma_congruencesymmetric).

assert (Cong B M M A) by (forward_using lemma_congruenceflip).

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Midpoint B M A) by (conclude_def Midpoint ).

assert (¬ Col D M B).

{

intro.

assert (Col D B M) by (forward_using lemma_collinearorder).

assert (Col D B F) by (conclude_def Col ).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (Col B M F) by (conclude lemma_collinear4).

assert (Col F B M) by (forward_using lemma_collinearorder).

contradict.

}

assert (Cong D B R A) by (conclude lemma_pointreflectionisometry).

assert (¬ Col F M B).

{

intro.

assert (Col F B M) by (forward_using lemma_collinearorder).

assert (Col D B F) by (conclude_def Col ).

assert (Col F B D) by (forward_using lemma_collinearorder).

assert (neq B F) by (forward_using lemma_betweennotequal).

assert (neq F B) by (conclude lemma_inequalitysymmetric).

assert (Col B M D) by (conclude lemma_collinear4).

assert (Col D B M) by (forward_using lemma_collinearorder).

contradict.

}

assert (Cong F B Q A) by (conclude lemma_pointreflectionisometry).

assert (Cong B F F B) by (conclude cn_equalityreverse).

assert (Cong B D F B) by (conclude lemma_congruencetransitive).

assert (Cong B D Q A) by (conclude lemma_congruencetransitive).

assert (Cong R A D B) by (conclude lemma_congruencesymmetric).

assert (Cong R A B D) by (forward_using lemma_congruenceflip).

assert (Cong R A Q A) by (conclude lemma_congruencetransitive).

assert (Per C A B) by (conclude lemma_8_2).

assert (Out A B M) by (conclude lemma_ray4).

assert (Per C A M) by (conclude lemma_8_3).

assert (Cong C A A E) by (forward_using lemma_congruenceflip).

assert (Cong C M E M) by (conclude lemma_rightreverse).

assert (nCol C A M) by (conclude lemma_rightangleNC).

assert (¬ eq C M).

{

intro.

assert (Col C A M) by (conclude_def Col ).

contradict.

}

assert (BetS Q M F) by (conclude axiom_betweennesssymmetry).

assert (BetS R M D) by (conclude axiom_betweennesssymmetry).

assert (Cong D B B F) by (forward_using lemma_congruenceflip).

assert (Cong D M F M) by (conclude lemma_rightreverse).

assert (Cong F M D M) by (conclude lemma_congruencesymmetric).

assert (Cong F M M Q) by (forward_using lemma_congruenceflip).

assert (Cong M Q F M) by (conclude lemma_congruencesymmetric).

assert (Cong Q M F M) by (forward_using lemma_congruenceflip).

assert (Cong Q M D M) by (conclude lemma_congruencetransitive).

assert (Cong Q M M R) by (conclude lemma_congruencetransitive).

assert (Cong Q M R M) by (forward_using lemma_congruenceflip).

assert (Cong M F M D) by (forward_using lemma_congruenceflip).

assert (Cong C A A E) by (forward_using lemma_congruenceflip).

assert (Cong C M E M) by (conclude lemma_rightreverse).

assert (Cong E M C M) by (conclude lemma_congruencesymmetric).

assert (Cong M E M C) by (forward_using lemma_congruenceflip).

assert (Midpoint C A E) by (conclude_def Midpoint ).

assert (Midpoint D M R) by (conclude_def Midpoint ).

assert (Midpoint F M Q) by (conclude_def Midpoint ).

assert (Cong M B M A) by (conclude lemma_congruencesymmetric).

assert (Cong B M M A) by (forward_using lemma_congruenceflip).

assert (Midpoint B M A) by (conclude_def Midpoint ).

assert (Cong F B Q A) by (conclude lemma_pointreflectionisometry).

assert (Cong D B R A) by (conclude lemma_pointreflectionisometry).

assert (Cong Q A F B) by (conclude lemma_congruencesymmetric).

assert (Cong B F D B) by (conclude lemma_congruencesymmetric).

assert (Cong F B D B) by (forward_using lemma_congruenceflip).

assert (Cong Q A D B) by (conclude lemma_congruencetransitive).

assert (Cong Q A R A) by (conclude lemma_congruencetransitive).

assert (Cong Q A A R) by (forward_using lemma_congruenceflip).

assert (¬ Col D M F).

{

intro.

assert (Col D B F) by (conclude_def Col ).

assert (Col F D B) by (forward_using lemma_collinearorder).

assert (Col F D M) by (forward_using lemma_collinearorder).

assert (neq D F) by (forward_using lemma_betweennotequal).

assert (neq F D) by (conclude lemma_inequalitysymmetric).

assert (Col D B M) by (conclude lemma_collinear4).

contradict.

}

assert (Cong D F R Q) by (conclude lemma_pointreflectionisometry).

assert (Cong F D Q R) by (forward_using lemma_congruenceflip).

assert (BetS F B D) by (conclude axiom_betweennesssymmetry).

assert (Cong B D A R) by (forward_using lemma_congruenceflip).

assert (BetS Q A R) by (conclude lemma_betweennesspreserved).

assert (Midpoint Q A R) by (conclude_def Midpoint ).

assert (Cong E A A C) by (forward_using lemma_doublereverse).

assert (BetS E A C) by (conclude axiom_betweennesssymmetry).

assert (Midpoint E A C) by (conclude_def Midpoint ).

assert (Cong E Q C R) by (conclude lemma_pointreflectionisometry).

assert (Cong Q E R C) by (forward_using lemma_congruenceflip).

assert (neq Q M) by (forward_using lemma_betweennotequal).

assert (Cong E F C D) by (conclude axiom_5_line).

assert (Cong C D E F) by (conclude lemma_congruencesymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_rightreverse.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearright.

Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_linereflectionisometry :

∀ A B C D E F,

Per B A C → Per A B D → BetS C A E → BetS D B F → Cong A C A E → Cong B D B F →

Cong C D E F.

Proof.

intros.

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS B A H ∧ Cong B A H A ∧ Cong B C H C ∧ neq A C)) by (conclude_def Per );destruct Tf as [H];spliter.

let Tf:=fresh in

assert (Tf:∃ G, (BetS A B G ∧ Cong A B G B ∧ Cong A D G D ∧ neq B D)) by (conclude_def Per );destruct Tf as [G];spliter.

assert (neq A B) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ M, (BetS A M B ∧ Cong M A M B)) by (conclude proposition_10);destruct Tf as [M];spliter.

assert (Per D B A) by (conclude lemma_8_2).

assert (neq B A) by (conclude lemma_inequalitysymmetric).

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Out B A M) by (conclude lemma_ray4).

assert (Per D B M) by (conclude lemma_8_3).

assert (nCol D B M) by (conclude lemma_rightangleNC).

assert (¬ eq D M).

{

intro.

assert (Col D B M) by (conclude_def Col ).

contradict.

}

assert (neq M D) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ R, (BetS D M R ∧ Cong M R M D)) by (conclude postulate_extension);destruct Tf as [R];spliter.

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Cong D B B F) by (forward_using lemma_congruenceflip).

assert (Cong D A F A) by (conclude lemma_rightreverse).

assert (Cong F A D A) by (conclude lemma_congruencesymmetric).

assert (Col D B F) by (conclude_def Col ).

assert (Col B D F) by (forward_using lemma_collinearorder).

assert (neq B F) by (forward_using lemma_betweennotequal).

assert (neq F B) by (conclude lemma_inequalitysymmetric).

assert (Per D B A) by (conclude lemma_8_2).

assert (Per F B A) by (conclude lemma_collinearright).

assert (Per F B M) by (conclude lemma_8_3).

assert (nCol F B M) by (conclude lemma_rightangleNC).

assert (nCol D B M) by (conclude lemma_rightangleNC).

assert (¬ eq F M).

{

intro.

assert (Col F B M) by (conclude_def Col ).

contradict.

}

assert (neq M F) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS F M Q ∧ Cong M Q M F)) by (conclude postulate_extension);destruct Tf as [Q];spliter.

assert (Cong M D M R) by (conclude lemma_congruencesymmetric).

assert (Cong D M M R) by (forward_using lemma_congruenceflip).

assert (Midpoint D M R) by (conclude_def Midpoint ).

assert (Cong M F M Q) by (conclude lemma_congruencesymmetric).

assert (Cong F M M Q) by (forward_using lemma_congruenceflip).

assert (Midpoint F M Q) by (conclude_def Midpoint ).

assert (Cong M B M A) by (conclude lemma_congruencesymmetric).

assert (Cong B M M A) by (forward_using lemma_congruenceflip).

assert (BetS B M A) by (conclude axiom_betweennesssymmetry).

assert (Midpoint B M A) by (conclude_def Midpoint ).

assert (¬ Col D M B).

{

intro.

assert (Col D B M) by (forward_using lemma_collinearorder).

assert (Col D B F) by (conclude_def Col ).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (Col B M F) by (conclude lemma_collinear4).

assert (Col F B M) by (forward_using lemma_collinearorder).

contradict.

}

assert (Cong D B R A) by (conclude lemma_pointreflectionisometry).

assert (¬ Col F M B).

{

intro.

assert (Col F B M) by (forward_using lemma_collinearorder).

assert (Col D B F) by (conclude_def Col ).

assert (Col F B D) by (forward_using lemma_collinearorder).

assert (neq B F) by (forward_using lemma_betweennotequal).

assert (neq F B) by (conclude lemma_inequalitysymmetric).

assert (Col B M D) by (conclude lemma_collinear4).

assert (Col D B M) by (forward_using lemma_collinearorder).

contradict.

}

assert (Cong F B Q A) by (conclude lemma_pointreflectionisometry).

assert (Cong B F F B) by (conclude cn_equalityreverse).

assert (Cong B D F B) by (conclude lemma_congruencetransitive).

assert (Cong B D Q A) by (conclude lemma_congruencetransitive).

assert (Cong R A D B) by (conclude lemma_congruencesymmetric).

assert (Cong R A B D) by (forward_using lemma_congruenceflip).

assert (Cong R A Q A) by (conclude lemma_congruencetransitive).

assert (Per C A B) by (conclude lemma_8_2).

assert (Out A B M) by (conclude lemma_ray4).

assert (Per C A M) by (conclude lemma_8_3).

assert (Cong C A A E) by (forward_using lemma_congruenceflip).

assert (Cong C M E M) by (conclude lemma_rightreverse).

assert (nCol C A M) by (conclude lemma_rightangleNC).

assert (¬ eq C M).

{

intro.

assert (Col C A M) by (conclude_def Col ).

contradict.

}

assert (BetS Q M F) by (conclude axiom_betweennesssymmetry).

assert (BetS R M D) by (conclude axiom_betweennesssymmetry).

assert (Cong D B B F) by (forward_using lemma_congruenceflip).

assert (Cong D M F M) by (conclude lemma_rightreverse).

assert (Cong F M D M) by (conclude lemma_congruencesymmetric).

assert (Cong F M M Q) by (forward_using lemma_congruenceflip).

assert (Cong M Q F M) by (conclude lemma_congruencesymmetric).

assert (Cong Q M F M) by (forward_using lemma_congruenceflip).

assert (Cong Q M D M) by (conclude lemma_congruencetransitive).

assert (Cong Q M M R) by (conclude lemma_congruencetransitive).

assert (Cong Q M R M) by (forward_using lemma_congruenceflip).

assert (Cong M F M D) by (forward_using lemma_congruenceflip).

assert (Cong C A A E) by (forward_using lemma_congruenceflip).

assert (Cong C M E M) by (conclude lemma_rightreverse).

assert (Cong E M C M) by (conclude lemma_congruencesymmetric).

assert (Cong M E M C) by (forward_using lemma_congruenceflip).

assert (Midpoint C A E) by (conclude_def Midpoint ).

assert (Midpoint D M R) by (conclude_def Midpoint ).

assert (Midpoint F M Q) by (conclude_def Midpoint ).

assert (Cong M B M A) by (conclude lemma_congruencesymmetric).

assert (Cong B M M A) by (forward_using lemma_congruenceflip).

assert (Midpoint B M A) by (conclude_def Midpoint ).

assert (Cong F B Q A) by (conclude lemma_pointreflectionisometry).

assert (Cong D B R A) by (conclude lemma_pointreflectionisometry).

assert (Cong Q A F B) by (conclude lemma_congruencesymmetric).

assert (Cong B F D B) by (conclude lemma_congruencesymmetric).

assert (Cong F B D B) by (forward_using lemma_congruenceflip).

assert (Cong Q A D B) by (conclude lemma_congruencetransitive).

assert (Cong Q A R A) by (conclude lemma_congruencetransitive).

assert (Cong Q A A R) by (forward_using lemma_congruenceflip).

assert (¬ Col D M F).

{

intro.

assert (Col D B F) by (conclude_def Col ).

assert (Col F D B) by (forward_using lemma_collinearorder).

assert (Col F D M) by (forward_using lemma_collinearorder).

assert (neq D F) by (forward_using lemma_betweennotequal).

assert (neq F D) by (conclude lemma_inequalitysymmetric).

assert (Col D B M) by (conclude lemma_collinear4).

contradict.

}

assert (Cong D F R Q) by (conclude lemma_pointreflectionisometry).

assert (Cong F D Q R) by (forward_using lemma_congruenceflip).

assert (BetS F B D) by (conclude axiom_betweennesssymmetry).

assert (Cong B D A R) by (forward_using lemma_congruenceflip).

assert (BetS Q A R) by (conclude lemma_betweennesspreserved).

assert (Midpoint Q A R) by (conclude_def Midpoint ).

assert (Cong E A A C) by (forward_using lemma_doublereverse).

assert (BetS E A C) by (conclude axiom_betweennesssymmetry).

assert (Midpoint E A C) by (conclude_def Midpoint ).

assert (Cong E Q C R) by (conclude lemma_pointreflectionisometry).

assert (Cong Q E R C) by (forward_using lemma_congruenceflip).

assert (neq Q M) by (forward_using lemma_betweennotequal).

assert (Cong E F C D) by (conclude axiom_5_line).

assert (Cong C D E F) by (conclude lemma_congruencesymmetric).

close.

Qed.

End Euclid.