proposition: Lemma inv_isopsmetry : forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y) (H : isopsmetry f), isopsmetry (Inv f (isopsmetry_imp_bij X Y f H)).
proof: Proof. intros X Y f H. unfold isopsmetry in |- *. split. apply Inv_bij. unfold isopsmetry in H. unfold equivalent_psmetric in H. elim H. intros. elim b. intros. elim a0. intros. elim b0. intros. unfold equivalent_psmetric in |- *. split. split. apply CPsMetricSpace_is_CPsMetricSpace. apply Build_is_CPsMetricSpace. unfold com in |- *. intros x y. unfold Inv in |- *. simpl in |- *. apply ax_d_com. exact a1. unfold nneg in |- *. intros x y. unfold Inv in |- *. simpl in |- *. apply ax_d_nneg. exact a1. unfold pos_imp_ap in |- *. intros x y. unfold Inv in |- *. simpl in |- *. intro H7. set (H6 := inv_strext) in *. set (H5 := H6 X Y f (isopsmetry_imp_bij X Y f (a, ((a1, b1), (a2, b2))))) in *. generalize H5. unfold fun_strext in |- *. intros H4. apply H4. set (H8 := ax_d_pos_imp_ap) in *. set (H9 := H8 X (cms_d (c:=X)) a1) in *. generalize H9. unfold pos_imp_ap in |- *. intro H10. apply H10. apply H7. unfold tri_ineq in |- *. unfold Inv in |- *. simpl in |- *. set (H3 := ax_d_tri_ineq) in *. set (H4 := H3 X (cms_d (c:=X)) a1) in *. generalize H4. unfold tri_ineq in |- *. intro H5. intros x y z. apply H5. split. elim b2. simpl in |- *. intros m P. exists m. intros y0 y1. elim a. intros. unfold surjective in b3. elim (b3 y0). intros x0 b4. elim (b3 y1). intros x1 b5. astepl (f x0[-d]y1). astepl (f x0[-d]f x1). apply leEq_transitive with (nring (S m)[*](x0[-d]x1)). simpl in |- *. apply P. simpl in |- *. apply eq_imp_leEq. apply mult_wdr. set (H4 := csbf_wd) in *. set (H5 := H4 X X IR (cms_d (c:=X))) in *. generalize H5. unfold bin_fun_wd in |- *. intro H6. apply H6. cut (invfun f (isopsmetry_imp_bij X Y f ((a3, b3), (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) (f x0)[=] invfun f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) y0). intros. astepr (invfun f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) (f x0)). apply eq_symmetric. apply inv2. set (H10 := csf_wd) in *. set (H7 := H10 Y X (Inv f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))))) in *. generalize H7. unfold fun_wd in |- *. unfold Inv in |- *. simpl in |- *. intro H8. apply H8. exact b4. cut (invfun f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) (f x1)[=] invfun f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) y1). intros. astepr (invfun f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))) (f x1)). apply eq_symmetric. apply inv2. set (H10 := csf_wd) in *. set (H7 := H10 Y X (Inv f (isopsmetry_imp_bij X Y f (pair (a3, b3) (pair (a1, b1) (pair a2 (existT (fun n : nat => forall x y : X, f x[-d]f y[<=](nring n[+][1])[*](x[-d]y)) m P))))))) in *. generalize H7. unfold fun_wd in |- *. unfold Inv in |- *. simpl in |- *. intro H8. apply H8. exact b5. elim a2. simpl in |- *. intros m P. exists m. intros y0 y1. elim a. intros. unfold surjective in b3. elim (b3 y0). intros x0 b4. elim (b3 y1). intros x1 b5. astepr ((nring m[+][1])[*](f x0[-d]f x1)). apply leEq_transitive with (x0[-d]x1). 2: apply P. apply eq_imp_leEq. set (H4 := csbf_wd) in *. set (H5 := H4 X X IR (cms_d (c:=X))) in *. generalize H5. unfold bin_fun_wd in |- *. intro H6. apply H6. cut (invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) y0[=] invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) (f x0)). intros. astepl (invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) (f x0)). apply inv2. set (H10 := csf_wd) in *. set (H7 := H10 Y X (Inv f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))))) in *. generalize H7. unfold fun_wd in |- *. unfold Inv in |- *. simpl in |- *. intro H8. apply H8. apply eq_symmetric. exact b4. cut (invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) y1[=] invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) (f x1)). intros. astepl (invfun f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))) (f x1)). apply inv2. set (H10 := csf_wd) in *. set (H7 := H10 Y X (Inv f (isopsmetry_imp_bij X Y f (pair (pair a3 b3) (pair (pair a1 b1) (pair (existT (fun n : nat => forall x y : X, x[-d]y[<=](nring n[+][1])[*](f x[-d]f y)) m P) b2)))))) in *. generalize H7. unfold fun_wd in |- *. unfold Inv in |- *. simpl in |- *. intro H8. apply H8. apply eq_symmetric. exact b5. Qed.
imports: CoRN.metrics.IR_CPMSpace