Library Algebra.AffineSpace.AffineSpace_sub

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for affine subspaces.

Description

Support for affine subspace

Let K : Ring, V : ModuleSpace K and E : AffineSpace V. Let PE : E Prop, O : E and PV : V Prop.
Let O : E.
Lemmas about predicate compatible_as have "cas" in their names, usually as prefix "cas_", sometimes as suffix "_cas".
Let gen : E Prop.

Additional support for affine map

Let K : Ring, V1 V2 : ModuleSpace K. Let E1 : AffineSpace V1 and E2 : AffineSpace V2. Let f : E1 E2 and PE1 : E1 Prop.

Additional support for affine subspace

Let K : Ring and HK : invertible (2 : K). Let V : ModuleSpace K and E : AffineSpace V. Let PE : E Prop and HPE : compatible_as PE. Let O : E and HO : PE O.
Let K : Ring and HK : invertible (2 : K). Let V1 V2 : ModuleSpace K. Let E1 : AffineSpace V1 and E2 : AffineSpace V2. Let PE1 : E1 Prop and PE2 : E2 Prop. Let HPE1 : compatible_as PE1 and HPE2 : compatible_as PE2. Let O1 : E1, HO1 : PE1 O1, O2 : E2 and HO2 : PE2 O2. Let f : E1 E2 and Hf : funS PE1 PE2 f.

Additional definition for commutative rings of scalars

This is only stated for the ring of real numbers R_Ring.
Let V1 V2 : ModuleSpace R_Ring. Let E1 : AffineSpace V1 and E2 : AffineSpace V2.
  • Am E1 E2 is the affine subspace of affine maps from E1 to E2

Bibliography

[GostiauxT4] Bernard Gostiaux, Cours de mathématiques spéciales - 4. Géométrie affine et métrique Mathématiques, Presses Universitaires de France, Paris, 1995, https://www.puf.com/cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique.

Used logic axioms

Usage

This module may be used through the import of Algebra.AffineSpace.AffineSpace, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Sub_struct.
From Algebra Require Import Monoid Group Ring ModuleSpace.
From Algebra Require Import AffineSpace_def AffineSpace_FF.
From Algebra Require Import AffineSpace_baryc AffineSpace_aff_map.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Local Open Scope AffineSpace_scope.

Section Compatible_AffineSpace_Def.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Definition vectP (PE : E Prop) (O : E) : V Prop :=
  preimage (transl O) PE.
Definition translP (PV : V Prop) (O : E) : E Prop :=
  preimage (vect O) PV.
Definition vect_closed_gen (PE : E Prop) (PV : V Prop) : Prop :=
   O A, PE O PE A translP PV O A.
Definition transl_closed_gen (PE : E Prop) (PV : V Prop) : Prop :=
   O u, PE O PV u vectP PE O u.
Definition vect_closed PE O := vect_closed_gen PE (vectP PE O).
Definition transl_closed PE O := transl_closed_gen PE (vectP PE O).

[GostiauxT4] Def. 1.23, p. 9. compatible_as is actually baryc_closed.
Definition compatible_as (PE : E Prop) : Prop :=
   n L (A : 'E^n),
    invertible (sum L) inclF A PE PE (barycenter L A).

Definition span_as (gen : E Prop) : E Prop :=
  span compatible_as gen.

Inductive baryc_closure (gen : E Prop) : E Prop :=
  | Barycenter_closure :
     n L (B : 'E^n),
      invertible (sum L) inclF B gen
      baryc_closure gen (barycenter L B).

End Compatible_AffineSpace_Def.

Section Compatible_AffineSpace_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Lemma vectP_correct :
   {PE : E Prop} {O}, PE O PE = image (transl O) (vectP PE O).
Proof. intros; rewrite image_of_preimage transl_l_fullset inter_full_r //. Qed.

Lemma vectP_eq : {PE : E Prop} {O}, vectP PE O = image (vect O) PE.
Proof.
intros; apply preimage_eq; [apply transl_correct_r | apply transl_correct_l].
Qed.

Lemma vectP_inj :
   {PE QE : E Prop} O, vectP PE O = vectP QE O PE = QE.
Proof. move=>>; eapply preimage_inj, transl_correct_l. Qed.

Lemma vectP_full :
   {PE : E Prop} O, full PE full (vectP PE O).
Proof. intros; apply preimage_full_equiv; easy. Qed.

Lemma vectP_fullset : (O : E), vectP fullset O = fullset.
Proof. easy. Qed.

Lemma vectP_inter :
   {PE1 PE2 : E Prop} {O},
    vectP (inter PE1 PE2) O = inter (vectP PE1 O) (vectP PE2 O).
Proof. easy. Qed.

Lemma vectP_inter_any :
   {Idx : Type} {PE : Idx E Prop} {O},
    vectP (inter_any PE) O = inter_any (fun idxvectP (PE idx) O).
Proof. easy. Qed.

Lemma vectP_zero_closed_equiv :
   {PE : E Prop} {O}, zero_closed (vectP PE O) PE O.
Proof. intros PE O; rewrite -{2}(transl_zero O); easy. Qed.

Lemma translP_correct :
   {PV : V Prop} (O : E), PV = image (vect O) (translP PV O).
Proof. intros; rewrite image_of_preimage vect_l_fullset inter_full_r //. Qed.

Lemma translP_eq :
   {PV : V Prop} {O : E}, translP PV O = image (transl O) PV.
Proof.
intros; apply preimage_eq; [apply transl_correct_l | apply transl_correct_r].
Qed.

Lemma translP_inj :
   {PV QV : V Prop} (O : E), translP PV O = translP QV O PV = QV.
Proof. move=>>; eapply preimage_inj, transl_correct_r. Qed.

Lemma translP_full :
   {PV : V Prop} (O : E), full PV full (translP PV O).
Proof. intros; apply preimage_full_equiv; easy. Qed.

Lemma translP_fullset : (O : E), translP fullset O = fullset.
Proof. easy. Qed.

Lemma translP_inter :
   {PV1 PV2 : V Prop} {O : E},
    translP (inter PV1 PV2) O = inter (translP PV1 O) (translP PV2 O).
Proof. easy. Qed.

Lemma translP_inter_any :
   {Idx : Type} {PV : Idx V Prop} {O : E},
    translP (inter_any PV) O = inter_any (fun idxtranslP (PV idx) O).
Proof. easy. Qed.

Lemma translP_zero_closed_equiv :
   {PV : V Prop} (O : E), zero_closed PV translP PV O O.
Proof. intros; unfold translP, preimage; rewrite vect_zero; easy. Qed.

Lemma vectP_translP :
   (PV : V Prop) (O : E), vectP (translP PV O) O = PV.
Proof. intros; apply preimage_can, transl_correct_r. Qed.

Lemma translP_vectP :
   {PE : E Prop} O, translP (vectP PE O) O = PE.
Proof. intros; apply preimage_can, transl_correct_l. Qed.

Lemma vect_transl_closed_gen_equiv :
   {PE : E Prop} {PV},
    vect_closed_gen PE PV transl_closed_gen PE PV.
Proof.
intros; split; intros HPE A; unfold vectP, translP, preimage.
intros u HA; rewrite -{1}(transl_correct_r A u) (HPE A); easy.
intros B HA; rewrite -{1}(transl_correct_l A B) (HPE A); easy.
Qed.

Lemma vect_transl_closed_equiv :
   {PE : E Prop} {O}, vect_closed PE O transl_closed PE O.
Proof. intros; apply vect_transl_closed_gen_equiv. Qed.

Lemma transl_plus_closed :
   {PE : E Prop} {O}, transl_closed PE O plus_closed (vectP PE O).
Proof.
move=>> HPE u v; unfold vectP, preimage; rewrite -transl_assoc; apply HPE; easy.
Qed.

Lemma vect_plus_closed :
   {PE : E Prop} {O}, vect_closed PE O plus_closed (vectP PE O).
Proof. move=>> /vect_transl_closed_equiv; apply transl_plus_closed. Qed.

Lemma cms_transl :
   {PE : E Prop} {O}, PE O
    compatible_ms (vectP PE O) transl_closed PE O.
Proof.
unfold vectP; intros PE O HO HPE A u; unfold vectP, preimage.
rewrite -(transl_correct_l O A) transl_assoc iff_sym_equiv.
apply (cms_plus_equiv HPE).
Qed.

Lemma cms_vect :
   {PE : E Prop} {O}, PE O
    compatible_ms (vectP PE O) vect_closed PE O.
Proof.
unfold vect_closed.
move=>>; rewrite vect_transl_closed_gen_equiv; apply cms_transl.
Qed.

Lemma vectP_orig_indep :
   {PE : E Prop} {O} (O' : E), PE O
    compatible_ms (vectP PE O') vectP PE O = vectP PE O'.
Proof.
intros; apply subset_ext; intros u.
apply iff_sym, cms_transl; try easy.
apply vectP_zero_closed_equiv, cms_zero; easy.
Qed.

Lemma translP_orig_indep :
   {PV : V Prop} {O} (O' : E), translP PV O O'
    compatible_ms PV translP PV O = translP PV O'.
Proof.
intros PV O O' HO' HPV; apply subset_ext; intros A.
rewrite -{2}(vectP_translP PV O); apply cms_vect; try easy.
apply translP_zero_closed_equiv, cms_zero; easy.
rewrite vectP_translP; easy.
Qed.

Lemma vect_closed_orig_indep :
   {PE : E Prop} O O',
    PE O compatible_ms (vectP PE O')
    vect_closed PE O vect_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.

Lemma transl_closed_orig_indep :
   {PE : E Prop} O O',
    PE O compatible_ms (vectP PE O')
    transl_closed PE O transl_closed PE O'.
Proof.
move=>> HO HPV HPE; move=>>; rewrite -(vectP_orig_indep _ HO); auto.
Qed.

Lemma transl_closed_gen_sms_uniq :
   {PE : E Prop} {PV} {O : E},
    PE O compatible_ms PV transl_closed_gen PE PV PV = vectP PE O.
Proof.
move=>> HO HPV HPE; apply subset_ext_equiv; split; intro;
    [apply HPE | apply (HPE _ _ HO)]; easy.
Qed.

Lemma vect_closed_gen_sms_uniq :
   {PE : E Prop} {PV} {O : E},
    PE O compatible_ms PV vect_closed_gen PE PV PV = vectP PE O.
Proof.
move=>>; rewrite vect_transl_closed_gen_equiv; apply transl_closed_gen_sms_uniq.
Qed.

Lemma cas_empty :
   {PE : E Prop}, nonzero_struct K empty PE compatible_as PE.
Proof.
intros PE HK HPE n L A HL HA; destruct n.
contradict HL; apply sum_nil_noninvertible; easy.
contradict HA; rewrite not_all_ex_not_equiv; ord0.
intros HA0; apply (HPE _ HA0).
Qed.

Lemma cas_emptyset :
   {PE : E Prop}, nonzero_struct K compatible_as (@emptyset E).
Proof. intros; apply cas_empty; easy. Qed.

Lemma cas_singleton : (O : E), compatible_as (singleton O).
Proof. move=>> HL /extF ->; apply baryc_constF; easy. Qed.

Lemma cas_unit :
   {PE : E Prop},
    nonzero_struct K is_unit_type E compatible_as PE.
Proof.
intros PE HK [O HE].
destruct (empty_dec PE) as [HPE | HPE].
apply cas_empty; easy.
rewrite (unit_subset_is_singleton PE HE HPE).
apply cas_singleton.
Qed.

Lemma cas_full : {PE : E Prop}, full PE compatible_as PE.
Proof. easy. Qed.

Lemma cas_fullset : compatible_as (@fullset E).
Proof. easy. Qed.

Lemma cms_cas :
   {PE : E Prop} {O},
    PE O nonzero_struct K invertible (2 : K)
    compatible_ms (vectP PE O) compatible_as PE.
Proof.
move=>> HO HK1 HK2 HPE n L A HL HA.
destruct n. contradict HL; apply sum_nil_noninvertible; easy.
generalize (cms_vect HO HPE (A ord0)); intros HPE'.
unfold translP, vectP, preimage in HPE'.
apply HPE', (cms_scal_rev HPE (sum L) _ HL); try easy.
rewrite baryc_correct_orig; try easy.
apply cms_lc; try easy.
unfold vectP, preimage; intro; rewrite vectF_correct -HPE'; easy.
Qed.

Lemma cas_scal :
   {PE : E Prop} {O},
    PE O compatible_as PE scal_closed (vectP PE O).
Proof.
intros PE O HO HPE a u Hu; unfold vectP, preimage in ×.
assert (H0 : invertible (sum (coupleF (1 - a) a))).
  rewrite sum_coupleF -plus_assoc plus_opp_l plus_zero_r.
  apply invertible_one.
assert (H : O +++ scal a u =
    barycenter (coupleF (1 - a) a) (coupleF O (O +++ u))).
  apply baryc_coupleF_equiv; try easy.
  rewrite -{2}(transl_zero O) 2!vect_transl.
  rewrite 2!scal_minus_distr_l scal_zero_r scal_minus_distr_r scal_one.
  rewrite minus_zero_l plus_opp_l; easy.
unfold vectP; rewrite H; apply HPE; try easy.
intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
    [rewrite coupleF_0 | rewrite coupleF_1]; easy.
Qed.

Lemma cas_scal_rev :
   {PE : E Prop} {O},
    PE O compatible_as PE scal_rev_closed (vectP PE O).
Proof. intros; apply scal_scal_rev_closed, cas_scal; easy. Qed.

Lemma cas_plus :
   {PE : E Prop} {O},
    PE O invertible (2 : K)
    compatible_as PE plus_closed (vectP PE O).
Proof.
intros PE O HO HK HPE; unfold vectP, preimage.
unfold two in HK; rewrite -(sum_2 ones) in HK.
intros u v Hu Hv; pose (A := coupleF (O +++ u) (O +++ v)).
rewrite (transl_l_eq _ _ (sum (vectF O A))).
rewrite -lc_ones_l -baryc_correct_orig; try easy.
apply (cas_scal_rev HO HPE (inv (@sum _ 2 ones)));
    try now apply inv_invertible. unfold vectP, preimage.
rewritescal_assoc, mult_inv_l, scal_one, transl_correct_l; try easy.
apply HPE; try easy; unfold A;
    intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi;
    [rewrite coupleF_0 | rewrite coupleF_1]; easy.
unfold A; rewrite vectF_coupleF sum_2 coupleF_0 coupleF_1 !transl_correct_r //.
Qed.

Lemma cas_cms :
   {PE : E Prop} {O},
    PE O invertible (2 : K)
    compatible_as PE compatible_ms (vectP PE O).
Proof.
intros; apply plus_scal_closed_cms.
unfold vectP, preimage; 0; rewrite transl_zero; easy.
apply cas_plus; easy.
apply cas_scal; easy.
Qed.

Lemma cas_cms_equiv :
   {PE : E Prop} {O},
    PE O nonzero_struct K invertible (2 : K)
    compatible_as PE compatible_ms (vectP PE O).
Proof. intros; split; [apply cas_cms | apply cms_cas]; easy. Qed.

Lemma cas_sms_orig_indep :
   {PE : E Prop} {O O'},
    PE O PE O' invertible (2 : K)
    compatible_as PE vectP PE O = vectP PE O'.
Proof. intros; apply vectP_orig_indep; try apply cas_cms; easy. Qed.

Lemma cas_vect :
   {PE : E Prop} {O},
    PE O invertible (2 : K)
    compatible_as PE vect_closed PE O.
Proof. intros; apply cms_vect, cas_cms; easy. Qed.

Lemma cas_transl :
   {PE : E Prop} {O},
    PE O invertible (2 : K)
    compatible_as PE transl_closed PE O.
Proof.
intros; apply vect_transl_closed_gen_equiv, cas_vect; easy.
Qed.

Lemma cas_inter :
   {PE1 PE2 : E Prop},
    compatible_as PE1 compatible_as PE2 compatible_as (inter PE1 PE2).
Proof.
move=>> HPE1 HPE2; move=>> HL HA; split; [apply HPE1 | apply HPE2];
    try easy; intro; apply HA.
Qed.

Lemma cas_inter_any :
   {Idx : Type} {PE : Idx E Prop},
    ( idx, compatible_as (PE idx))
    compatible_as (inter_any PE).
Proof.
move=>> HPE; move=>> HL HA idx; apply HPE; try easy; intro; apply HA.
Qed.

Lemma span_as_cas : (gen : E Prop), compatible_as (span_as gen).
Proof. apply span_compatible; move=>>; apply cas_inter_any. Qed.

Lemma span_as_incl : (gen : E Prop), incl gen (span_as gen).
Proof. apply span_incl. Qed.

Lemma span_as_lub :
   gen {PE : E Prop},
    compatible_as PE incl gen PE incl (span_as gen) PE.
Proof. apply span_lub. Qed.

Lemma span_as_full :
   {PE : E Prop}, compatible_as PE span_as PE = PE.
Proof. apply span_full. Qed.

Lemma baryc_closure_ex :
   (gen : E Prop) A,
    ( n L (B : 'E^n),
      invertible (sum L) inclF B gen A = barycenter L B)
    baryc_closure gen A.
Proof.
move=>> [n [L [B [HL [HB HA]]]]]; rewrite HA; apply Barycenter_closure; easy.
Qed.

Lemma baryc_closure_ex_rev :
   (gen : E Prop) A,
    baryc_closure gen A
     n L (B : 'E^n),
      sum L = 1 ( i, L i 0) inclF B gen A = barycenter L B.
Proof.
intros gen A HA; induction HA as [n L B HL HB].
destruct (baryc_normalized_n0_ex L B HL)
    as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]].
n1, L1, A1; repeat split; try easy.
apply (inclF_monot_l _ B); easy.
Qed.

Lemma bc_len_EX :
   (gen : E Prop) A,
    { n | baryc_closure gen A
       L (B : 'E^n),
        sum L = 1 ( i, L i 0)
        inclF B gen A = barycenter L B }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (baryc_closure_ex_rev _ _ HA) as [n [L [B HLB]]].
n; intros _; L, B; easy.
0; intros HA'; easy.
Qed.

Definition bc_len (gen : E Prop) A := proj1_sig (bc_len_EX gen A).

Lemma bc_EX :
   (gen : E Prop) A,
    { LB : 'K^(bc_len gen A) × 'E^(bc_len gen A) |
      baryc_closure gen A
      sum LB.1 = 1 ( i, LB.1 i 0)
      inclF LB.2 gen A = barycenter LB.1 LB.2 }.
Proof.
intros gen A; apply ex_EX.
destruct (classic_dec (baryc_closure gen A)) as [HA | HA].
destruct (proj2_sig (bc_len_EX gen A)) as [L [B HLB]]; try easy.
(L, B); intros _; easy.
destruct (inhabited_as E) as [O].
((fun _ ⇒ 0), (fun _O)); intros HA'; easy.
Qed.

Definition bc_coef (gen : E Prop) A := fst (proj1_sig (bc_EX gen A)).
Definition bc_point (gen : E Prop) A := snd (proj1_sig (bc_EX gen A)).

Lemma bc_nLB_correct :
   (gen : E Prop) A,
    baryc_closure gen A
    sum (bc_coef gen A) = 1
    ( i, bc_coef gen A i 0)
    inclF (bc_point gen A) gen
    A = barycenter (bc_coef gen A) (bc_point gen A).
Proof. intros gen A HA; destruct (proj2_sig (bc_EX gen A)); easy. Qed.

Lemma baryc_closure_exs :
   {gen : E Prop} {n} (A : 'E^n),
    inclF A (baryc_closure gen)
     (b : 'nat^n) L (B : i, 'E^(b i)),
      ( i, sum (L i) = 1) ( i j, L i j 0)
      ( i, inclF (B i) gen) A = fun ibarycenter (L i) (B i).
Proof.
intros gen n A HA; destruct n.
destruct (inhabited_as E) as [O]; 0, (fun _ ⇒ 0), (fun _ _O).
repeat split; try apply extF; intros [i Hi]; easy.
(fun ibc_len gen (A i)), (fun ibc_coef gen (A i)),
    (fun ibc_point gen (A i)).
repeat split; try apply extF; intro; apply bc_nLB_correct; easy.
Qed.

Lemma cas_equiv :
   (PE : E Prop), compatible_as PE PE = baryc_closure PE.
Proof.
intros PE; split; intros HPE.
apply subset_ext_equiv; split; intros A HA; try induction HA; auto.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A)); try easy.
apply Barycenter_closure; try easy.
apply sum_singleF_invertible.
1,2: apply invertible_one.
move=>> HL HB; rewrite HPE; apply Barycenter_closure; easy.
Qed.

Lemma baryc_closure_incl :
   (gen : E Prop), incl gen (baryc_closure gen).
Proof.
intros gen A HA.
rewrite -(baryc_singleF 1 A (singleF 1) (singleF A));
    try apply invertible_one; try easy.
apply Barycenter_closure; try easy.
rewrite sum_1 singleF_0; apply invertible_one.
Qed.

End Compatible_AffineSpace_Facts.

Section Compatible_AffineSpace_Affine_Mapping_Facts1.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 Prop}.
Context {PE2 : E2 Prop}.

Context {f : E1 E2}.
Hypothesis Hf : aff_map f.

Lemma cas_image : compatible_as PE1 compatible_as (image f PE1).
Proof.
intro; move=>> HL /inclF_image_equiv [A [HA1 HA2]].
rewrite HA2 -Hf; try easy; apply Im; auto.
Qed.

Lemma cas_preimage : compatible_as PE2 compatible_as (preimage f PE2).
Proof. intro; move=>> Hl HA; unfold preimage; rewrite Hf; auto. Qed.

End Compatible_AffineSpace_Affine_Mapping_Facts1.

Section Compatible_AffineSpace_Affine_Mapping_Def.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 Prop.

Variable f : E1 E2.

Definition am_sub : Prop :=
   n L (A1 : 'E1^n),
    inclF A1 PE1
    invertible (sum L) f (barycenter L A1) = barycenter L (mapF f A1).

End Compatible_AffineSpace_Affine_Mapping_Def.

Section Compatible_AffineSpace_Affine_Mapping_Facts2a.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 Prop}.
Hypothesis HPE1 : compatible_as PE1.
Context {PE2 : E2 Prop}.
Hypothesis HPE2 : compatible_as PE2.

Context {f : E1 E2}.
Hypothesis Hf : aff_map f.

Lemma RgS_gen_cas : compatible_as (RgS_gen PE1 PE2 f).
Proof. apply cas_inter, cas_image; easy. Qed.

Lemma RgS_cas : compatible_as (RgS PE1 f).
Proof. apply cas_image; easy. Qed.

End Compatible_AffineSpace_Affine_Mapping_Facts2a.

Section Compatible_AffineSpace_Affine_Mapping_Facts2b.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.

Context {f : E1 E2}.
Hypothesis Hf : aff_map f.

Lemma Rg_cas : compatible_as (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cas cas_fullset Hf). Qed.

End Compatible_AffineSpace_Affine_Mapping_Facts2b.

Section Compatible_AffineSpace_Affine_Mapping_Facts4a.

Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Variable PE1 : E1 Prop.

Lemma am_sub_id : am_sub PE1 ssrfun.id.
Proof. easy. Qed.

Context {f : E1 E2}.

Lemma am_is_sub : aff_map f am_sub PE1 f.
Proof. intros Hf n L A1 _; apply Hf. Qed.

End Compatible_AffineSpace_Affine_Mapping_Facts4a.

Section Compatible_AffineSpace_Affine_Mapping_Facts4b.

Context {K : Ring}.
Context {V1 V2 V3 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {E3 : AffineSpace V3}.
Context {PE1 : E1 Prop}.
Variable PE2 : E2 Prop.

Context {f : E1 E2}.
Hypothesis Hf : funS PE1 PE2 f.
Variable g : E2 E3.

Lemma am_comp_sub : am_sub PE1 f am_sub PE2 g am_sub PE1 (g \o f).
Proof.
intros Hfa Hga n L A1 HA1 HL; unfold ssrfun.comp; rewrite Hfa// Hga//.
apply (inclF_monot_r (RgS PE1 f)); [easy |].
apply mapF_inclF; easy.
Qed.

End Compatible_AffineSpace_Affine_Mapping_Facts4b.

Section Sub_AffineSpace_Def.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_as PE.
Context {O : E}.
Hypothesis HO : PE O.

Definition sub_point_of_as : sub PE := mk_sub HO.

Let PV := vectP PE O.
Let HPV : compatible_ms PV := cas_cms HO HK HPE.

Lemma sub_vect_aux : {A B}, PE A PE B PV (A --> B).
Proof. move=>>; apply cas_vect; easy. Qed.

Lemma sub_vectF_aux :
   {n} {A} {B : 'E^n}, PE A inclF B PE inclF (vectF A B) PV.
Proof. intros; intro; apply sub_vect_aux; easy. Qed.

Definition sub_vect (A B : sub PE) : sub_ModuleSpace HPV :=
  mk_sub (sub_vect_aux (in_sub A) (in_sub B)).

Lemma sub_vect_chasles :
   A B C, sub_vect B A + sub_vect A C = sub_vect B C.
Proof. intros; apply val_inj, vect_chasles. Qed.

Lemma sub_vect_l_bij_ex : A u, ! B, sub_vect A B = u.
Proof.
intros [A HA] [u Hu]; unfold PV in Hu.
assert (Hu' : vectP PE A u) by now rewrite -(cas_transl HO).
(mk_sub_ PE (A +++ u) Hu'); split.
apply val_inj, transl_correct_r.
move⇒ [B HB1] /(f_equal val) /= HB2.
apply val_inj; simpl; rewrite -HB2; apply transl_correct_l.
Qed.

Definition sub_AffineSpace_mixin :=
  AffineSpace.Mixin _ _ _ sub_point_of_as _ sub_vect_chasles sub_vect_l_bij_ex.

Canonical Structure sub_AffineSpace :=
  AffineSpace.Pack _ _ sub_AffineSpace_mixin (sub PE).

Lemma sub_transl_aux : {A u}, PE A PV u PE (A +++ u).
Proof. move=>>; apply cas_transl; easy. Qed.

Lemma sub_translF_aux :
   {n} {A} {u : 'V^n}, PE A inclF u PV inclF (translF A u) PE.
Proof. intros; intro; apply sub_transl_aux; easy. Qed.

Definition sub_transl
    (A : sub_AffineSpace) (u : sub_ModuleSpace HPV) : sub_AffineSpace :=
  mk_sub (sub_transl_aux (in_sub A) (in_sub u)).

Lemma val_vect : f_vect_compat_gen val val.
Proof. easy. Qed.

Lemma val_vectF : f_vectF_compat_gen val val.
Proof. easy. Qed.

Lemma val_transl : f_transl_compat_gen val val.
Proof.
intros A u; pose (B := A +++ u).
assert (HB : u = A --> B) by now unfold B; rewrite transl_correct_r.
rewrite HB val_vect 2!transl_correct_l; easy.
Qed.

Lemma val_translF : f_translF_compat_gen val val.
Proof. move=>>; apply extF; intro; apply val_transl. Qed.

Lemma val_baryc :
   {n} L (A : 'sub_AffineSpace^n),
    invertible (sum L) val (barycenter L A) = barycenter L (mapF val A).
Proof.
intros n L A HL; apply baryc_correct_equiv; [easy |].
unfold aff_comb; rewrite -val_vectF -val_lc baryc_correct; easy.
Qed.

Lemma val_am : aff_map val.
Proof. intro; apply val_baryc. Qed.

Lemma mk_sub_vect :
   {A B : E} (HA : PE A) (HB : PE B),
    mk_sub HA --> mk_sub HB = mk_sub (sub_vect_aux HA HB).
Proof. easy. Qed.

Lemma mk_sub_vectF :
   {n} {O} {A : 'E^n} (HO : PE O) (HA : inclF A PE),
    vectF (mk_sub HO) (fun imk_sub (HA i)) =
      fun imk_sub (sub_vect_aux HO (HA i)).
Proof. easy. Qed.

Lemma mk_sub_transl :
   {A u} (HA : PE A) (Hu : PV u),
    mk_sub HA +++ mk_sub Hu = mk_sub (sub_transl_aux HA Hu).
Proof. intros; apply val_inj, val_transl. Qed.

Lemma mk_sub_translF :
   {n} {A} {u : 'V^n} (HA : PE A) (Hu : inclF u PV),
    translF (mk_sub HA) (fun imk_sub (Hu i)) =
      fun imk_sub (sub_transl_aux HA (Hu i)).
Proof. intros; apply extF; intro; apply mk_sub_transl. Qed.

Lemma mk_sub_baryc :
   {n} {L} {A : 'E^n} (HL : invertible (sum L)) (HA : inclF A PE),
    barycenter L (fun imk_sub (HA i)) = mk_sub (HPE _ _ _ HL HA).
Proof. intros; apply val_inj, val_baryc; easy. Qed.

Lemma sub_vect_eq :
   (A B : sub_AffineSpace),
    A --> B = mk_sub (sub_vect_aux (in_sub A) (in_sub B)).
Proof. easy. Qed.

Lemma sub_vectF_eq :
   {n} O (A : 'sub_AffineSpace^n),
    vectF O A = fun imk_sub (sub_vect_aux (in_sub O) (in_sub (A i))).
Proof. easy. Qed.

Lemma sub_transl_eq :
   (A : sub_AffineSpace) (u : sub_ModuleSpace HPV),
    A +++ u = mk_sub (sub_transl_aux (in_sub A) (in_sub u)).
Proof. intros; apply val_inj, val_transl. Qed.

Lemma sub_translF_eq :
   {n} (A : sub_AffineSpace) (u : '(sub_ModuleSpace HPV)^n),
    translF A u = fun imk_sub (sub_transl_aux (in_sub A) (in_sub (u i))).
Proof. intros; apply extF; intro; apply sub_transl_eq. Qed.

Lemma sub_baryc_eq :
   {n} {L} {A : 'sub_AffineSpace^n} (HL : invertible (sum L)),
    barycenter L A = mk_sub (HPE _ _ _ HL (fun iin_sub (A i))).
Proof. intros; apply val_inj, val_baryc; easy. Qed.

End Sub_AffineSpace_Def.

Section Sub_AffineSpace_Facts1.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEa PEb : E Prop}.
Hypothesis HPE : incl PEa PEb.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Let PEa' : PEb_as Prop := preimage val PEa.

Lemma RgS_val_as_eq : RgS PEa' val = PEa.
Proof. apply RgS_val_eq; easy. Qed.

Lemma preimage_val_cas : compatible_as PEa compatible_as PEa'.
Proof. intros; apply cas_preimage; [apply val_am | easy]. Qed.

Lemma preimage_val_cas_rev : compatible_as PEa' compatible_as PEa.
Proof.
intros; rewrite -RgS_val_as_eq; apply RgS_cas; [easy | apply val_am].
Qed.

Lemma preimage_val_cas_equiv : compatible_as PEa' compatible_as PEa.
Proof. split; [apply preimage_val_cas_rev | apply preimage_val_cas]. Qed.

End Sub_AffineSpace_Facts1.

Section Sub_AffineSpace_Facts2.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PEb : E Prop}.
Hypothesis HPEb : compatible_as PEb.
Context {O : E}.
Hypothesis HO : PEb O.
Let PEb_as := sub_AffineSpace HK HPEb HO.
Context {PEa : PEb_as Prop}.
Let PEa' := RgS PEa val.

Lemma preimage_val_as_eq : preimage val PEa' = PEa.
Proof. apply preimage_val_eq. Qed.

Lemma RgS_val_cas : compatible_as PEa compatible_as PEa'.
Proof. intros; apply RgS_cas; [easy | apply val_am]. Qed.

Lemma RgS_val_cas_rev : compatible_as PEa' compatible_as PEa.
Proof.
intros; rewrite -preimage_val_as_eq; apply cas_preimage; [apply val_am | easy].
Qed.

Lemma RgS_val_cas_equiv : compatible_as PEa' compatible_as PEa.
Proof. split; [apply RgS_val_cas_rev | apply RgS_val_cas]. Qed.

End Sub_AffineSpace_Facts2.

Section Sub_AffineSpace_Affine_Mapping_Facts1.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 Prop}.
Context {PE2 : E2 Prop}.
Context {HPE1 : compatible_as PE1}.
Context {HPE2 : compatible_as PE2}.
Context {O1 : E1}.
Context {O2 : E2}.
Context {HO1 : PE1 O1}.
Context {HO2 : PE2 O2}.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.

Context {f : E1 E2}.
Context {fS : PE1_as PE2_as}.
Hypothesis HfS : x, val (fS x) = f (val x).

Lemma sub_as_am : aff_map f aff_map fS.
Proof.
intros Hf n; intros; apply val_inj; rewrite HfS !val_baryc// Hf//.
f_equal; apply extF; intro; rewrite !mapF_correct; easy.
Qed.

End Sub_AffineSpace_Affine_Mapping_Facts1.

Section Sub_AffineSpace_Affine_Mapping_Facts2.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {PE1 : E1 Prop}.
Context {PE2 : E2 Prop}.
Hypothesis HPE1 : compatible_as PE1.
Hypothesis HPE2 : compatible_as PE2.
Context {O1 : E1}.
Context {O2 : E2}.
Hypothesis HO1 : PE1 O1.
Hypothesis HO2 : PE2 O2.
Let PE1_as := sub_AffineSpace HK HPE1 HO1.
Let PE2_as := sub_AffineSpace HK HPE2 HO2.

Context {f : E1 E2}.
Hypothesis Hf : funS PE1 PE2 f.

Definition fct_sub_as : PE1_as PE2_as := fct_sub Hf.

Lemma fct_sub_as_inj : injS PE1 f injective fct_sub_as.
Proof. apply fct_sub_inj. Qed.

Lemma fct_sub_as_inj_rev : injective fct_sub_as injS PE1 f.
Proof. apply fct_sub_inj_rev. Qed.

Lemma fct_sub_as_inj_equiv : injective fct_sub_as injS PE1 f.
Proof. apply fct_sub_inj_equiv. Qed.

Lemma fct_sub_as_surj : surjS PE1 PE2 f surjective fct_sub_as.
Proof. apply fct_sub_surj. Qed.

Lemma fct_sub_as_surj_rev : surjective fct_sub_as surjS PE1 PE2 f.
Proof. apply fct_sub_surj_rev. Qed.

Lemma fct_sub_as_surj_equiv : surjective fct_sub_as surjS PE1 PE2 f.
Proof. apply fct_sub_surj_equiv. Qed.

Lemma fct_sub_as_bij : bijS PE1 PE2 f bijective fct_sub_as.
Proof. apply fct_sub_bij, inhabited_as. Qed.

Lemma fct_sub_as_bij_rev : bijective fct_sub_as bijS PE1 PE2 f.
Proof. apply fct_sub_bij_rev, inhabited_as. Qed.

Lemma fct_sub_as_bij_equiv : bijective fct_sub_as bijS PE1 PE2 f.
Proof. apply fct_sub_bij_equiv, inhabited_as. Qed.

Lemma fct_sub_as_am : aff_map f aff_map fct_sub_as.
Proof. apply sub_as_am, fct_sub_correct. Qed.

Lemma fct_sub_as_f_inv_am :
   (Hfb : bijS PE1 PE2 f),
    aff_map f aff_map (f_inv (fct_sub_as_bij Hfb)).
Proof. intros; apply am_bij_compat, fct_sub_as_am; easy. Qed.

End Sub_AffineSpace_Affine_Mapping_Facts2.

Section Sub_AffineSpace_Affine_Mapping_Facts3.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E Prop}.
Context {PF : F Prop}.
Hypothesis HPE : compatible_as PE.
Hypothesis HPF : compatible_as PF.

Context {f : E F}.
Hypothesis Hf : aff_map f.

Variable O : E.
Hypothesis HO : PE O.

Let lf := fct_lm f O.
Let PV := vectP PE O.
Let PW := vectP PF (f O).

Lemma funS_aff_lin_equiv : funS PE PF f funS PV PW lf.
Proof.
rewrite !funS_equiv; split.
intros Hf1 v Hv; unfold PW, vectP, preimage, lf;
    rewrite transl_correct_l; auto.
intros Hlf A HA;
    rewrite -(transl_correct_l (f O) (f A)) -(transl_correct_l O A).
apply Hlf; unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
Qed.

Lemma injS_aff_lin_equiv : injS PE f injS PV lf.
Proof.
split.
intros Hf1 u1 u2 Hu1 Hu2 Hu; apply (transl_l_inj O), Hf1; auto.
apply (vect_l_inj (f O)); auto.
intros Hlf1 A1 A2 HA1 HA2 HA; apply (vect_l_inj O), Hlf1.
1,2: unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite !transl_correct_l HA; easy.
Qed.

Lemma injS_aff_lin_equiv_alt : injS PE f incl (KerS PV lf) zero_sub_struct.
Proof.
rewrite injS_aff_lin_equiv -KerS_zero_equiv.
rewrite -lmS_injS_equiv; [easy |..].
1,3: apply cas_cms; easy.
1,2: apply am_lm_equiv; easy.
Qed.

Lemma surjS_gen_aff_lin_equiv : surjS PE PF f surjS PV PW lf.
Proof.
split.
intros Hf1 w Hw; destruct (Hf1 (f O +++ w)) as [A [HA1 HA2]]; try easy.
(O --> A); split.
unfold PV, vectP, preimage; rewrite transl_correct_l; easy.
unfold lf, fct_lm; rewrite transl_correct_l HA2 transl_correct_r; easy.
intros Hlf B HB; destruct (Hlf (f O --> B)) as [v [Hv1 Hv2]].
unfold PW, vectP, preimage; rewrite transl_correct_l; easy.
(O +++ v); split; try apply (vect_l_inj (f O)); easy.
Qed.

Lemma surjS_gen_aff_lin_equiv_alt : surjS PE PF f incl PW (RgS PV lf).
Proof.
rewrite surjS_gen_aff_lin_equiv -RgS_gen_full_equiv; apply surjS_RgS_gen_equiv.
Qed.

Lemma bijS_gen_aff_lin_equiv : bijS PE PF f bijS PV PW lf.
Proof.
rewrite !bijS_equiv; [| apply inhabited_ms | easy].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv surjS_gen_aff_lin_equiv; easy.
Qed.

Lemma bijS_gen_aff_lin_equiv_alt :
  bijS PE PF f
  funS PV PW lf incl (KerS PV lf) zero_sub_struct incl PW (RgS PV lf).
Proof.
rewrite bijS_equiv; [| apply inhabited_as].
rewrite funS_aff_lin_equiv injS_aff_lin_equiv_alt surjS_gen_aff_lin_equiv_alt//.
Qed.

End Sub_AffineSpace_Affine_Mapping_Facts3.

Section Sub_AffineSpace_Affine_Mapping_Facts4.

Context {K : Ring}.
Hypothesis HK : invertible (2 : K).
Context {V W : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_as PE.

Context {f : E F}.
Hypothesis Hf : aff_map f.

Variable O : E.
Hypothesis HO : PE O.

Let lf := fct_lm f O.
Let PV := vectP PE O.

Lemma surjS_aff_lin_equiv : surjS PE fullset f surjS PV fullset lf.
Proof. rewrite (surjS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.

Lemma surjS_aff_lin_equiv_alt :
  surjS PE fullset f incl fullset (RgS PV lf).
Proof. rewrite (surjS_gen_aff_lin_equiv_alt O) vectP_fullset; easy. Qed.

Lemma bijS_aff_lin_equiv : bijS PE fullset f bijS PV fullset lf.
Proof. rewrite (bijS_gen_aff_lin_equiv O) vectP_fullset; easy. Qed.

Lemma bijS_aff_lin_equiv_alt :
  bijS PE fullset f
  incl (KerS PV lf) zero_sub_struct incl fullset (RgS PV lf).
Proof.
rewrite (bijS_gen_aff_lin_equiv_alt HK HPE Hf O)// vectP_fullset; easy.
Qed.

End Sub_AffineSpace_Affine_Mapping_Facts4.

Section Compatible_AffineSpace_R_Facts.

Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {PE : E Prop}.
Context {O : E}.
Hypothesis HO : PE O.

Lemma cas_cms_equiv_R : compatible_as PE compatible_ms (vectP PE O).
Proof.
apply cas_cms_equiv; [easy | apply nonzero_struct_R | apply invertible_2].
Qed.

Variable gen : E Prop.

Lemma cas_baryc_closure_R : compatible_as (baryc_closure gen).
Proof.
intros n L A HL HA; destruct (baryc_normalized_n0_ex _ A HL)
    as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]]; rewrite HA1b.
destruct (baryc_closure_exs _ (inclF_monot_l _ _ _ HA1a HA))
    as [b [M [B [HM1 [HM2 [HB HA']]]]]].
assert (HL1' : L1 = fun i1sum (scal (L1 i1) (M i1))).
  apply extF; intro; rewrite -scal_sum_distr_l HM1 scal_one_r; easy.
rewrite (baryc_eq_r (fun i1barycenter (scal (L1 i1) (M i1)) (B i1))).
2: { rewrite HA'; apply extF; intro; apply baryc_homogeneous.
  apply invertible_equiv_R; easy.
  rewrite HM1; apply invertible_one. }
rewrite {1}HL1' -baryc_assoc.
apply Barycenter_closure.
1,4: rewrite sum_assoc -HL1' HL1a; apply invertible_one.
apply concatnF_inclF_equiv; easy.
intros i; rewrite -(extF_rev _ _ HL1' i).
apply invertible_equiv_R; easy.
Qed.

Lemma baryc_closure_idem_R :
  baryc_closure (baryc_closure gen) = baryc_closure gen.
Proof. apply eq_sym, cas_equiv, cas_baryc_closure_R. Qed.

[GostiauxT4] Th 1.26, p. 10.
Lemma span_as_eq_R : span_as gen = baryc_closure gen.
Proof.
apply subset_ext_equiv; split.
apply (span_as_lub gen).
apply cas_baryc_closure_R.
apply baryc_closure_incl.
intros A HA; induction HA; apply span_as_cas; try easy.
apply inclF_monot_r with gen; try easy.
apply span_as_incl.
Qed.

End Compatible_AffineSpace_R_Facts.

Section Sub_AffineSpace_Affine_Mapping_R_Facts.

Context {V W : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Context {F : AffineSpace W}.

Lemma cas_am : compatible_as (@aff_map _ _ _ E F).
Proof.
intros n2 L2 f2 HL2 Hf2 n1 L1 A1 HL1; generalize HL1 HL2.
move⇒ /invertible_equiv_R HL1' /invertible_equiv_R HL2'.
rewrite fct_baryc_eq; try easy.
assert (Hf2a :
  f2^~ (barycenter L1 A1) = fun i2barycenter L1 (mapF (f2 i2) A1))
    by now apply extF; intros i2; apply (Hf2 i2).
rewrite Hf2a.
pose (f := barycenter L2 f2).
generalize (baryc_correct f2 HL2); fold f; intros Hf.
pose (B1 := mapF f A1); fold B1.
pose (B2 := fun i2barycenter L1 (mapF (f2 i2) A1)); fold B2.
assert (HB2 : i2, aff_comb L1 (mapF (f2 i2) A1) (B2 i2))
    by now intros; apply baryc_correct_equiv.
pose (B := barycenter L2 B2).
generalize (baryc_correct B2 HL2); fold B; intros HB.
apply baryc_correct_equiv; try easy; unfold aff_comb in ×.
pose (M i1 i2 := f2 i2 (A1 i1) --> B2 i2).
assert (HM : lin_comb L1 (mapF (lin_comb L2 (vectF f f2)) A1) +
    lin_comb L1 (mapF (lin_comb L2) M) = 0).
  rewrite Hf mapF_zero_f lc_zero_r plus_zero_l.
  rewrite -lc_flipT_r lc2_r_sym flipT_invol; unfold M.
  apply lc_zero_compat_r, extF; intros i2.
  rewrite fct_lc_r_eq fct_zero_eq opp_zero_equiv -lc_opp_r -(HB2 i2).
  apply lc_eq_r, extF; intro; rewrite vectF_correct vect_sym; easy.
apply (scal_zero_reg_r_R (sum L2)); try easy.
rewrite -(plus_zero_r (scal _ _)) -{1}HM -lc_plus_r; unfold M.
rewrite (lc_eq_r _ (_ + _) (lin_comb L2 (fun i2 i1B1 i1 --> B2 i2))).
2: { apply extF; intro.
    rewrite fct_plus_eq !mapF_correct !fct_lc_r_eq -lc_plus_r; f_equal.
    rewrite vectF_chasles; easy. }
rewrite -lc_scal_r -lc_constF_r -!lc_plus_r.
apply lc_zero_compat_r, extF; intros i1.
rewrite fct_lc_r_eq fct_zero_eq -HB; f_equal; apply extF; intros i2.
rewrite !fct_plus_eq constF_correct !vectF_correct; apply vect_chasles.
Qed.

Definition Am := sub_AffineSpace invertible_2 cas_am fct_point_of_as_am.

End Sub_AffineSpace_Affine_Mapping_R_Facts.