proposition: Lemma comp_resp_isopsmetry : forall (X Y Z : CPsMetricSpace) (f : CSetoid_fun X Y) (g : CSetoid_fun Y Z), isopsmetry f -> isopsmetry g -> isopsmetry (compose_CSetoid_fun X Y Z f g).
proof: Proof. intros X Y Z f g. unfold isopsmetry in |- *. intros H0 H1. elim H0. intros H00 H01. elim H1. intros H10 H11. split. apply comp_resp_bij. exact H00. exact H10. unfold equivalent_psmetric in |- *. split. split. apply CPsMetricSpace_is_CPsMetricSpace. unfold equivalent_psmetric in H01. elim H01. intros H010 H011. elim H010. intros H0100 H0101. elim H11. intros H110 H111. elim H110. intros H1100 H1101. apply Build_is_CPsMetricSpace. unfold com in |- *. simpl in |- *. intros x y. elim H1101. intros. generalize ax_d_com. unfold com in |- *. simpl in |- *. intro H2. apply H2. unfold nneg in |- *. intros x y. simpl in |- *. elim H1101. intros. generalize ax_d_nneg. unfold nneg in |- *. simpl in |- *. intro H2. apply H2. elim H1101. intros. generalize ax_d_pos_imp_ap. unfold pos_imp_ap in |- *. simpl in |- *. intros H2 x y H3. set (H5 := csf_strext X Y f) in *. generalize H5. unfold fun_strext in |- *. intro H6. apply H6. auto. unfold tri_ineq in |- *. simpl in |- *. intros x y z. elim H1101. intros. generalize ax_d_tri_ineq. unfold tri_ineq in |- *. simpl in |- *. intro H2. apply H2. split. unfold equivalent_psmetric in H01. elim H01. intros H010 H011. elim H011. intros H0110 H0111. unfold equivalent_psmetric in H11. elim H11. intros H110 H111. elim H111. intros H1110 H1111. elim H0110. simpl in |- *. intros n H0110'. elim H1110. simpl in |- *. intros m H1110'. exists (S m * S n). intros x y. apply leEq_transitive with ((nring n[+][1])[*](f x[-d]f y)). apply H0110'. apply leEq_transitive with ((nring n[+][1])[*](nring m[+][1])[*](g (f x)[-d]g (f y))). astepr ((nring n[+][1])[*]((nring m[+][1])[*](g (f x)[-d]g (f y)))). apply mult_resp_leEq_lft. apply H1110'. apply less_leEq. astepr (nring (R:=IR) (S n)). apply pos_nring_S. apply mult_resp_leEq_rht. apply leEq_transitive with (nring (R:=IR) (S m * S n)). apply eq_imp_leEq. astepl (nring (R:=IR) (S n)[*](nring m[+][1])). astepl (nring (R:=IR) (S n)[*]nring (S m)). astepl (nring (R:=IR) (S m)[*]nring (S n)). astepl (nring (R:=IR) (S m * S n)). apply eq_reflexive. astepr (nring (R:=IR) (S (S m * S n))). apply less_leEq. apply nring_less_succ. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. unfold equivalent_psmetric in H01. elim H01. intros H010 H011. elim H011. intros H0110 H0111. unfold equivalent_psmetric in H11. elim H11. intros H110 H111. elim H111. intros H1110 H1111. elim H0111. simpl in |- *. intros n H0111'. elim H1111. simpl in |- *. intros m H1111'. exists (S m * S n). intros x y. apply leEq_transitive with (nring (R:=IR) (S m)[*](f x[-d]f y)). apply H1111'. apply leEq_transitive with (nring (S m)[*]nring (S n)[*](x[-d]y)). astepr (nring (S m)[*](nring (S n)[*](x[-d]y))). apply mult_resp_leEq_lft. apply H0111'. apply less_leEq. apply pos_nring_S. apply mult_resp_leEq_rht. apply leEq_transitive with (nring (R:=IR) (S m * S n)). apply eq_imp_leEq. astepl (nring (R:=IR) (S m * S n)). apply eq_reflexive. astepr (nring (R:=IR) (S (S m * S n))). apply less_leEq. apply nring_less_succ. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.IR_CPMSpace