Let X, d and A be given.
Assume Hm: metric_on X d.
Assume HA: A ⊆ X.
We will prove metric_on A (metric_restrict X d A).
We will prove function_on (metric_restrict X d A) (setprod A A) R ∧ (∀x y : set, x ∈ A → y ∈ A → apply_fun (metric_restrict X d A) (x,y) = apply_fun (metric_restrict X d A) (y,x)) ∧ (∀x : set, x ∈ A → apply_fun (metric_restrict X d A) (x,x) = 0) ∧ (∀x y : set, x ∈ A → y ∈ A → ¬ (Rlt (apply_fun (metric_restrict X d A) (x,y)) 0) ∧ (apply_fun (metric_restrict X d A) (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ A → y ∈ A → z ∈ A → ¬ (Rlt (add_SNo (apply_fun (metric_restrict X d A) (x,y)) (apply_fun (metric_restrict X d A) (y,z))) (apply_fun (metric_restrict X d A) (x,z)))).
Apply and5I to the current goal.
Let pq be given.
Assume Hpq: pq ∈ setprod A A.
We will prove apply_fun (metric_restrict X d A) pq ∈ R.
We prove the intermediate claim Hsub: setprod A A ⊆ setprod X X.
An exact proof term for the current goal is (setprod_Subq A A X X HA HA).
We prove the intermediate claim HpqXX: pq ∈ setprod X X.
An exact proof term for the current goal is (Hsub pq Hpq).
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
rewrite the current goal using (metric_restrict_def X d A) (from left to right) at position 1.
rewrite the current goal using (apply_fun_graph (setprod A A) (λp : set ⇒ apply_fun d p) pq Hpq) (from left to right).
An exact proof term for the current goal is (Hfun pq HpqXX).
Let x and y be given.
Assume HxA: x ∈ A.
Assume HyA: y ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HA y HyA).
We prove the intermediate claim Hxy: (x,y) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x y HxA HyA).
We prove the intermediate claim Hyx: (y,x) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A y x HyA HxA).
rewrite the current goal using (metric_restrict_apply X d A x y HxA HyA) (from left to right).
rewrite the current goal using (metric_restrict_apply X d A y x HyA HxA) (from left to right).
An exact proof term for the current goal is (metric_on_symmetric X d x y Hm HxX HyX).
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hxx: (x,x) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x x HxA HxA).
rewrite the current goal using (metric_restrict_apply X d A x x HxA HxA) (from left to right).
An exact proof term for the current goal is (metric_on_diag_zero X d x Hm HxX).
Let x and y be given.
Assume HxA: x ∈ A.
Assume HyA: y ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HA y HyA).
We prove the intermediate claim Hxy: (x,y) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x y HxA HyA).
We prove the intermediate claim Happly: apply_fun (metric_restrict X d A) (x,y) = apply_fun d (x,y).
An exact proof term for the current goal is (metric_restrict_apply X d A x y HxA HyA).
Apply andI to the current goal.
Assume Hlt: Rlt (apply_fun (metric_restrict X d A) (x,y)) 0.
We will prove False.
We prove the intermediate claim HltD: Rlt (apply_fun d (x,y)) 0.
rewrite the current goal using Happly (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (metric_on_nonneg X d x y Hm HxX HyX HltD).
Assume H0: apply_fun (metric_restrict X d A) (x,y) = 0.
We prove the intermediate claim H0D: apply_fun d (x,y) = 0.
rewrite the current goal using Happly (from right to left) at position 1.
An exact proof term for the current goal is H0.
An exact proof term for the current goal is (metric_on_zero_eq X d x y Hm HxX HyX H0D).
Let x, y and z be given.
Assume HxA: x ∈ A.
Assume HyA: y ∈ A.
Assume HzA: z ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HA y HyA).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HA z HzA).
We prove the intermediate claim Hxy: (x,y) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x y HxA HyA).
We prove the intermediate claim Hyz: (y,z) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A y z HyA HzA).
We prove the intermediate claim Hxz: (x,z) ∈ setprod A A.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x z HxA HzA).
We prove the intermediate claim HxyAp: apply_fun (metric_restrict X d A) (x,y) = apply_fun d (x,y).
An exact proof term for the current goal is (metric_restrict_apply X d A x y HxA HyA).
We prove the intermediate claim HyzAp: apply_fun (metric_restrict X d A) (y,z) = apply_fun d (y,z).
An exact proof term for the current goal is (metric_restrict_apply X d A y z HyA HzA).
We prove the intermediate claim HxzAp: apply_fun (metric_restrict X d A) (x,z) = apply_fun d (x,z).
An exact proof term for the current goal is (metric_restrict_apply X d A x z HxA HzA).
Assume Hbad: Rlt (add_SNo (apply_fun (metric_restrict X d A) (x,y)) (apply_fun (metric_restrict X d A) (y,z))) (apply_fun (metric_restrict X d A) (x,z)).
We will prove False.
We prove the intermediate claim HbadD: Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (apply_fun d (x,z)).
rewrite the current goal using HxyAp (from right to left).
rewrite the current goal using HyzAp (from right to left).
rewrite the current goal using HxzAp (from right to left).
An exact proof term for the current goal is Hbad.
An exact proof term for the current goal is (metric_on_triangle X d x y z Hm HxX HyX HzX HbadD).
∎