# Library HighSchoolGeometry.composee_translation_rotation

Require Export composee_reflexions.
Set Implicit Arguments.
Unset Strict Implicit.

Theorem composee_translation_rotation :
(I A B : PO) (a : R),
image_angle a image_angle 0
J : PO,
( M M1 M2 : PO,
M1 = translation A B M M2 = rotation I a M1 M2 = rotation J a M).
intros I A B a H50; try assumption.
elim (classic (A = B)); intros H2.
I; intros.
generalize (translation_vecteur (I:=A) (J:=B) (A:=M) (A':=M1)); intros.
cut (M1 = M); intros.
rewrite H3 in H0; auto.
symmetry in |- ×.
apply vecteur_nul_conf.
rewrite <- H1; auto.
rewrite <- H2; Ringvec.
elim existence_representant_vecteur with (A := I) (B := milieu A B) (C := A);
intros D H3; try clear existence_representant_vecteur;
try exact H3.
cut (vec A B = mult_PP 2 (mult_PP (/ 2) (vec A B))); intros.
cut (I D); intros.
elim existence_rotation_Ia with (I := I) (M := D) (a := pisurdeux);
intros C H7.
cut (I C); auto; intros.
cut (orthogonal (vec I C) (vec I D)); intros.
elim existence_representant_vecteur with (A := C) (B := I) (C := D);
intros E H10; try clear existence_representant_vecteur;
try exact H10.
generalize (egalite_vecteur (A:=C) (B:=E) (C:=I) (D:=D)).
intros H33.
elim existence_representant_vecteur with (A := D) (B := A) (C := B);
intros F H11; try clear existence_representant_vecteur;
try exact H11.
cut (D E); intros.
cut (paralleles (droite I C) (droite D E)); intros.
elim existence_rotation_Ia with (I := I) (M := C) (a := / 2 × a);
intros G H18.
cut (I G); intros.
generalize (rotation_def (I:=I) (A:=C) (B:=G) (a:=/ 2 × a)); intros.
generalize
(position_relative_droites_coplanaires (A:=D) (B:=E) (C:=I) (D:=G));
intros.
elim H12; intros; auto with geo.
elim def_concours2 with (A := D) (B := E) (C := I) (D := G);
[ intros J H27; try clear def_concours2; try exact H27
| auto
| auto
| auto ].
elim H27; intros H28 H29; try clear H27; try exact H29.
cut (J I); intros.
J; intros.
generalize (translation_vecteur (I:=A) (J:=B) (A:=M) (A':=M1)); intros.
elim existence_reflexion_AB with (A := D) (B := E) (M := M);
[ intros M' H23; try clear existence_reflexion_AB | auto ].
elim existence_reflexion_AB with (A := I) (B := C) (M := M');
[ intros N H24; try clear existence_reflexion_AB | auto ].
generalize
(composee_reflexions_axes_paralleles (A:=D) (B:=E) (C:=I) (D:=C) (E:=F)
(M:=M) (M':=N) (M1:=M')); intros.
cut (N = translation D F M); intros.
cut (M1 = N); intros.
elim existence_reflexion_AB with (A := I) (B := C) (M := M1);
[ intros N' H31; try clear existence_reflexion_AB | auto ].
elim existence_reflexion_AB with (A := I) (B := G) (M := N');
[ intros N1 H32; try clear existence_reflexion_AB | auto ].
generalize (reflexion_symetrie (A:=I) (B:=C) (M:=M') (M':=N)); intros.
rewrite H21 in H31.
cut (N' = M'); intros.
generalize
(composee_reflexions_axes_secants (A:=I) (B:=C) (C:=G) (M:=N) (M':=N1)
(M1:=N') (a:=/ 2 × a)); intros.
rewrite H16.
rewrite H21.
replace a with (/ 2 × a + / 2 × a); auto.
rewrite <- H26; auto.
elim H9; intros.
cut (D J E J); intros.
elim H34;
[ intros H35; try clear H34 | intros H35; try clear H34; try exact H35 ].
mesure J D J I.
cut (double_AV (cons_AV (vec J D) (vec J I)) = image_angle a); intros.
generalize (axe_reflexion_droite (A:=D) (B:=E) (C:=J) (M:=M) (M':=M'));
intros.
generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1));
intros.
generalize
(composee_reflexions_axes_secants (A:=J) (B:=D) (C:=I) (M:=M) (M':=N1)
(M1:=M') (a:=x)); intros.
rewrite H39; auto.
apply deux_mes_angle_rotation.
unfold double_AV in H36.
rewrite H34; rewrite H36.
replace (/ 2 × a + / 2 × a) with a; auto with real.
apply (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1)); auto.
rewrite H32; rewrite H25; auto.
rewrite
(angles_et_paralleles (A:=J) (B:=D) (C:=J) (D:=I) (E:=I) (F:=C) (G:=I)
(I:=G)).
unfold double_AV in |- *; rewrite <- H30.
replace (/ 2 × a + / 2 × a) with a; auto with real.
auto.
red in |- *; intros.
rewrite H36 in H28.
absurd (alignes D E I); auto.
auto.
auto.
generalize (alignes_paralleles (A:=D) (B:=E) (C:=J)); intros.
apply paralleles_trans with (C := D) (D := E); auto with geo.
apply paralleles_trans with (C := D) (D := J); auto with geo.
generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros.
apply paralleles_trans with (C := I) (D := J); auto with geo.
mesure J E J I.
cut
(plus (cons_AV (vec J E) (vec J I)) (cons_AV (vec J E) (vec J I)) =
image_angle a); intros.
generalize (axe_reflexion_droite (A:=E) (B:=D) (C:=J) (M:=M) (M':=M'));
intros.
generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1));
intros.
generalize
(composee_reflexions_axes_secants (A:=J) (B:=E) (C:=I) (M:=M) (M':=N1)
(M1:=M') (a:=x)); intros.
rewrite H39; auto.
apply deux_mes_angle_rotation.
unfold double_AV in H36.
rewrite H34; rewrite H36.
replace (/ 2 × a + / 2 × a) with a; auto with real.
apply (axe_reflexion_droite (A:=E) (B:=D) (C:=J) (M:=M) (M':=M'));
auto with geo.
apply (axe_reflexion_droite (A:=D) (B:=E) (C:=E) (M:=M) (M':=M'));
auto with geo.
apply (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M') (M':=N1));
auto with geo.
rewrite H32; rewrite H25; auto.
replace (plus (cons_AV (vec J E) (vec J I)) (cons_AV (vec J E) (vec J I)))
with (double_AV (cons_AV (vec J E) (vec J I))); auto.
rewrite
(angles_et_paralleles (A:=J) (B:=E) (C:=J) (D:=I) (E:=I) (F:=C) (G:=I)
(I:=G)).
unfold double_AV in |- ×.
rewrite <- H30.
replace (/ 2 × a + / 2 × a) with a; auto with real.
auto.
auto.
auto.
auto.
generalize (alignes_paralleles (A:=E) (B:=D) (C:=J)); intros.
apply paralleles_trans with (C := D) (D := E); auto with geo.
apply paralleles_trans with (C := E) (D := D); auto with geo.
apply paralleles_trans with (C := E) (D := J); auto with geo.
generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros.
apply paralleles_trans with (C := I) (D := J); auto with geo.
apply not_and_or.
red in |- *; intros.
elim H34; intros.
apply H5.
rewrite H36; rewrite H35; auto.
auto.
auto.
elim H9; intros; auto with real.
auto with real.
rewrite H22; auto.
rewrite H20.
apply rec_translation_vecteur.
rewrite <- H17; auto.
apply H19; auto.
replace (vec D E) with (vec I C).
apply ortho_sym; auto with geo.
apply egalite_vecteur; auto with geo.
apply rec_translation_vecteur.
apply egalite_vecteur; auto with geo.
replace (vec D I) with (mult_PP (-1) (vec I D)).
rewrite <- H10; Ringvec.
Ringvec.
apply rec_translation_vecteur.
replace (vec D I) with (mult_PP (-1) (vec I D)).
replace (vec I F) with (add_PP (vec I D) (vec D F)).
rewrite H11; rewrite H3; auto.
rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto.
Ringvec.
Ringvec.
Ringvec.
red in |- *; intros.
rewrite H14 in H28.
absurd (alignes D E I); auto.
apply orthogonal_non_alignes; auto.
replace (vec D E) with (vec I C); auto with geo.
absurd (paralleles (droite D E) (droite I G)); auto with geo.
generalize (angle_non_paralleles (A:=I) (B:=C) (C:=I) (D:=G)); intros.
apply non_paralleles_trans with (A := I) (B := C); auto with geo.
red in |- *; intros.
apply H14; auto with geo.
elim H9; auto; intros.
unfold double_AV in |- *; rewrite <- H17.
replace (/ 2 × a + / 2 × a) with a; auto with real.
apply image_distinct_centre with (2 := H18); auto with geo.
apply (colineaires_paralleles (k:=1) (A:=I) (B:=C) (C:=D) (D:=E)); auto.
replace (vec D E) with (vec I C); auto with geo.
Ringvec.
red in |- *; intros; apply H1.
symmetry in |- ×.
apply vecteur_nul_conf; auto.
rewrite H33; auto.
rewrite H5; Ringvec.
elim (rotation_def (I:=I) (A:=D) (B:=C) (a:=pisurdeux)); auto with geo;
intros.
apply image_distinct_centre with (2 := H7); auto.
red in |- *; intros; apply H2.
apply vecteur_nul_conf; auto.
rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto.
replace (vec A (milieu A B)) with (mult_PP (-1) (vec (milieu A B) A)).
rewrite <- H3; rewrite H0; auto.
Ringvec.
Ringvec.
cut (2 0); intros; auto with real.
Fieldvec 2.
Qed.

Theorem composee_rotation_translation :
(I A B : PO) (a : R),
image_angle a image_angle 0
ex
(fun J : PO
M M1 M2 : PO,
M1 = rotation I a M M2 = translation A B M1 M2 = rotation J a M).
intros I A B a H50; try assumption.
elim (classic (A = B)); intros H2.
I; intros.
generalize (translation_vecteur (I:=A) (J:=B) (A:=M1) (A':=M2)); intros.
cut (M1 = M2); intros.
rewrite H3 in H; auto.
apply vecteur_nul_conf.
rewrite <- H1; auto.
rewrite <- H2; Ringvec.
elim existence_representant_vecteur with (A := I) (B := milieu A B) (C := B);
intros D H3; try clear existence_representant_vecteur;
try exact H3.
cut (vec A B = mult_PP 2 (mult_PP (/ 2) (vec A B))); intros.
cut (I D); intros.
elim existence_rotation_Ia with (I := I) (M := D) (a := pisurdeux);
intros C H7.
cut (I C); auto with geo; intros.
cut (orthogonal (vec I C) (vec I D)); intros.
elim existence_representant_vecteur with (A := C) (B := I) (C := D);
intros E H10; try clear existence_representant_vecteur;
try exact H10.
generalize (egalite_vecteur (A:=C) (B:=E) (C:=I) (D:=D)).
intros H33.
elim existence_representant_vecteur with (A := I) (B := A) (C := B);
intros F H11; try clear existence_representant_vecteur;
try exact H11.
cut (D E); intros.
cut (paralleles (droite I C) (droite D E)); intros.
elim existence_rotation_Ia with (I := I) (M := C) (a := - (/ 2 × a));
intros G H18.
cut (I G); intros.
generalize (rotation_def (I:=I) (A:=C) (B:=G) (a:=- (/ 2 × a))); intros.
generalize
(position_relative_droites_coplanaires (A:=D) (B:=E) (C:=I) (D:=G));
intros.
elim H12; intros; auto with geo.
elim def_concours2 with (A := D) (B := E) (C := I) (D := G);
[ intros J H28; try clear def_concours2; try exact H28
| auto
| auto
| auto ].
elim H28; intros.
clear H28.
cut (J I); intros.
J; intros.
generalize (translation_vecteur (I:=A) (J:=B) (A:=M1) (A':=M2)); intros.
elim existence_reflexion_AB with (A := I) (B := G) (M := M);
[ intros N' H25; try clear existence_reflexion_AB | auto ].
elim existence_reflexion_AB with (A := I) (B := C) (M := N');
[ intros N1 H26; try clear existence_reflexion_AB | auto ].
elim existence_reflexion_AB with (A := I) (B := C) (M := M1);
[ intros M' H27; try clear existence_reflexion_AB | auto ].
elim existence_reflexion_AB with (A := D) (B := E) (M := M');
[ intros N H29; try clear existence_reflexion_AB | auto ].
generalize
(composee_reflexions_axes_paralleles (A:=I) (B:=C) (C:=D) (D:=E) (E:=F)
(M:=M1) (M':=N) (M1:=M')); intros.
cut (N = translation I F M1); intros.
cut (M1 = N1); intros.
cut (M2 = N); intros.
generalize (reflexion_symetrie (A:=I) (B:=C) (M:=N') (M':=N1)); intros.
rewrite H23 in H27.
cut (N' = M'); intros.
generalize
(composee_reflexions_axes_secants (A:=I) (B:=G) (C:=C) (M:=M) (M':=M1)
(M1:=N') (a:=/ 2 × a)); intros.
elim H9; auto; intros.
rewrite H24.
cut (D J E J); intros.
elim H35; intros.
mesure J I J D.
cut
(plus (cons_AV (vec J I) (vec J D)) (cons_AV (vec J I) (vec J D)) =
image_angle a); intros.
generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M) (M':=N'));
intros.
generalize (axe_reflexion_droite (A:=D) (B:=E) (C:=J) (M:=N') (M':=N));
intros.
generalize
(composee_reflexions_axes_secants (A:=J) (B:=I) (C:=D) (M:=M) (M':=N)
(M1:=N') (a:=x)); intros.
rewrite H41; auto.
apply deux_mes_angle_rotation.
rewrite H37; rewrite H38; auto.
rewrite H40; auto.
rewrite H30; rewrite H29; auto.
replace (plus (cons_AV (vec J I) (vec J D)) (cons_AV (vec J I) (vec J D)))
with (double_AV (cons_AV (vec J I) (vec J D))); auto.
rewrite
(angles_et_paralleles (A:=J) (B:=I) (C:=J) (D:=D) (E:=I) (F:=G) (G:=I)
(I:=C)); auto.
unfold double_AV in |- ×.
rewrite <- (mes_oppx (A:=I) (B:=C) (C:=I) (D:=G) (x:=- (/ 2 × a))); auto.
replace (- - (/ 2 × a)) with (/ 2 × a); auto.
replace (/ 2 × a + / 2 × a) with a; auto with real.
ring.
generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros.
apply paralleles_trans with (C := I) (D := J); auto with geo.
generalize (alignes_paralleles (A:=D) (B:=E) (C:=J)); intros.
apply paralleles_trans with (C := D) (D := E); auto.
apply paralleles_trans with (C := D) (D := J); auto with geo.
mesure J I J E.
cut
(plus (cons_AV (vec J I) (vec J E)) (cons_AV (vec J I) (vec J E)) =
image_angle a); intros.
generalize (axe_reflexion_droite (A:=I) (B:=G) (C:=J) (M:=M) (M':=N'));
intros.
generalize (axe_reflexion_droite (A:=E) (B:=D) (C:=J) (M:=N') (M':=N));
intros.
generalize
(composee_reflexions_axes_secants (A:=J) (B:=I) (C:=E) (M:=M) (M':=N)
(M1:=N') (a:=x)); intros.
rewrite H41; auto.
apply deux_mes_angle_rotation.
rewrite H37; rewrite H38; auto.
rewrite H40; auto with geo.
apply (axe_reflexion_droite (A:=D) (B:=E) (C:=E) (M:=N') (M':=N));
auto with geo.
rewrite H29; rewrite H30; auto.
replace (plus (cons_AV (vec J I) (vec J E)) (cons_AV (vec J I) (vec J E)))
with (double_AV (cons_AV (vec J I) (vec J E))); auto.
rewrite
(angles_et_paralleles (A:=J) (B:=I) (C:=J) (D:=E) (E:=I) (F:=G) (G:=I)
(I:=C)); auto.
unfold double_AV in |- ×.
rewrite <- (mes_oppx (A:=I) (B:=C) (C:=I) (D:=G) (x:=- (/ 2 × a))); auto.
replace (- - (/ 2 × a)) with (/ 2 × a); auto.
replace (/ 2 × a + / 2 × a) with a; auto with real.
ring.
generalize (alignes_paralleles (A:=I) (B:=G) (C:=J)); intros.
apply paralleles_trans with (C := I) (D := J); auto with geo.
generalize (alignes_paralleles (A:=E) (B:=D) (C:=J)); intros.
apply paralleles_trans with (C := D) (D := E); auto.
apply paralleles_trans with (C := E) (D := D); auto with geo.
apply paralleles_trans with (C := E) (D := J); auto with geo.
apply not_and_or.
red in |- *; intros.
elim H35; intros.
apply H5.
rewrite H36; rewrite H37; auto.
rewrite H28; auto.
rewrite H21; auto.
apply rec_translation_vecteur.
rewrite H11; auto.
apply rec_translation_vecteur; auto with geo.
apply rec_translation_vecteur; auto with geo.
replace (vec D F) with (add_PP (vec I F) (mult_PP (-1) (vec I D))).
rewrite H11; rewrite H3; auto.
rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto.
rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=milieu A B)); auto.
Ringvec.
Ringvec.
generalize
(composee_reflexions_axes_secants (A:=I) (B:=G) (C:=C) (M:=M) (M':=N1)
(M1:=N') (a:=/ 2 × a)); intros.
rewrite H17; rewrite H23; auto.
replace (/ 2 × a + / 2 × a) with a; auto with real.
rewrite <- (mes_oppx (A:=I) (B:=C) (C:=I) (D:=G) (x:=- (/ 2 × a))); auto.
replace (- - (/ 2 × a)) with (/ 2 × a); auto.
ring.
elim H9; auto.
apply H21; auto.
apply rec_translation_vecteur; auto with geo.
apply rec_translation_vecteur; auto with geo.
replace (vec D F) with (add_PP (vec I F) (mult_PP (-1) (vec I D))).
rewrite H11; rewrite H3; auto.
rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto.
rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=milieu A B)); auto.
Ringvec.
Ringvec.
red in |- *; intros.
rewrite H16 in H14.
absurd (alignes D E I); auto.
apply orthogonal_non_alignes; auto with geo.
replace (vec D E) with (vec I C); auto with geo.
absurd (paralleles (droite D E) (droite I G)); auto.
generalize (angle_non_paralleles (A:=I) (B:=G) (C:=I) (D:=C)); intros H31.
apply non_paralleles_trans with (A := I) (B := C); auto with geo.
red in |- *; intros.
apply H31; auto.
elim H9; auto; intros.
unfold double_AV in |- ×.
rewrite <- (mes_oppx (A:=I) (B:=C) (C:=I) (D:=G) (x:=- (/ 2 × a))); auto.
replace (- - (/ 2 × a)) with (/ 2 × a); auto with geo.
replace (/ 2 × a + / 2 × a) with a; auto with real.
ring.
apply image_distinct_centre with (2 := H18); auto.
apply (colineaires_paralleles (k:=1) (A:=I) (B:=C) (C:=D) (D:=E)); auto.
replace (vec D E) with (vec I C); auto with geo.
Ringvec.
red in |- *; intros; apply H1.
symmetry in |- ×.
apply vecteur_nul_conf; auto.
rewrite H33; auto.
rewrite H5; Ringvec.
elim (rotation_def (I:=I) (A:=D) (B:=C) (a:=pisurdeux)); auto with geo;
intros.
apply image_distinct_centre with (2 := H7); auto with geo.
red in |- *; intros; apply H2.
apply vecteur_nul_conf; auto.
replace (vec A B) with (mult_PP 2 (vec (milieu A B) B)).
rewrite <- H3.
rewrite H0.
Ringvec.
rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=milieu A B)); auto.
rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=milieu A B)); auto.
cut (2 0); intros; auto with real.
Fieldvec 2.
Qed.