We will prove metric_on real_sequences uniform_metric_Romega.
We will prove ((((function_on uniform_metric_Romega (setprod real_sequences real_sequences) R ∧ (∀x y : set, x ∈ real_sequences → y ∈ real_sequences → apply_fun uniform_metric_Romega (x,y) = apply_fun uniform_metric_Romega (y,x))) ∧ (∀x : set, x ∈ real_sequences → apply_fun uniform_metric_Romega (x,x) = 0)) ∧ (∀x y : set, x ∈ real_sequences → y ∈ real_sequences → ¬ (Rlt (apply_fun uniform_metric_Romega (x,y)) 0) ∧ (apply_fun uniform_metric_Romega (x,y) = 0 → x = y))) ∧ (∀x y z : set, x ∈ real_sequences → y ∈ real_sequences → z ∈ real_sequences → ¬ (Rlt (add_SNo (apply_fun uniform_metric_Romega (x,y)) (apply_fun uniform_metric_Romega (y,z))) (apply_fun uniform_metric_Romega (x,z))))).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is uniform_metric_Romega_function_on.
Let x and y be given.
Assume Hx: x ∈ real_sequences.
Assume Hy: y ∈ real_sequences.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x y Hx Hy).
We prove the intermediate claim Hyxprod: (y,x) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences y x Hy Hx).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (y,x) Hyxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq y x) (from left to right).
rewrite the current goal using (tuple_2_1_eq y x) (from left to right).
An exact proof term for the current goal is (Romega_uniform_metric_value_sym x y Hx Hy).
Let x be given.
Assume Hx: x ∈ real_sequences.
We prove the intermediate claim Hxxprod: (x,x) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x x Hx Hx).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,x) Hxxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
An exact proof term for the current goal is (Romega_uniform_metric_value_self_zero x Hx).
Let x and y be given.
Assume Hx: x ∈ real_sequences.
Assume Hy: y ∈ real_sequences.
We will prove ¬ (Rlt (apply_fun uniform_metric_Romega (x,y)) 0) ∧ (apply_fun uniform_metric_Romega (x,y) = 0 → x = y).
Apply andI to the current goal.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x y Hx Hy).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
An exact proof term for the current goal is (Romega_uniform_metric_value_nonneg x y Hx Hy).
Assume H0: apply_fun uniform_metric_Romega (x,y) = 0.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x y Hx Hy).
We prove the intermediate claim Happ: apply_fun uniform_metric_Romega (x,y) = Romega_uniform_metric_value x y.
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim Hval0: Romega_uniform_metric_value x y = 0.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is H0.
We prove the intermediate claim Hcoord: ∀n : set, n ∈ ω → apply_fun x n = apply_fun y n.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (Romega_uniform_metric_value_eq0_coord_eq x y Hx Hy Hval0 n HnO).
An exact proof term for the current goal is (real_sequences_ext x y Hx Hy Hcoord).
Let x, y and z be given.
Assume Hx: x ∈ real_sequences.
Assume Hy: y ∈ real_sequences.
Assume Hz: z ∈ real_sequences.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x y Hx Hy).
We prove the intermediate claim Hyzprod: (y,z) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences y z Hy Hz).
We prove the intermediate claim Hxzprod: (x,z) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences x z Hx Hz).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (y,z) Hyzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (x,z) Hxzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
An exact proof term for the current goal is (Romega_uniform_metric_value_triangle x y z Hx Hy Hz).
∎