Let J be given.
We will prove metric_on (power_real J) (uniform_metric_power_real J).
We will prove ((((function_on (uniform_metric_power_real J) (setprod (power_real J) (power_real J)) R ∧ (∀x y : set, x ∈ power_real J → y ∈ power_real J → apply_fun (uniform_metric_power_real J) (x,y) = apply_fun (uniform_metric_power_real J) (y,x))) ∧ (∀x : set, x ∈ power_real J → apply_fun (uniform_metric_power_real J) (x,x) = 0)) ∧ (∀x y : set, x ∈ power_real J → y ∈ power_real J → ¬ (Rlt (apply_fun (uniform_metric_power_real J) (x,y)) 0) ∧ (apply_fun (uniform_metric_power_real J) (x,y) = 0 → x = y))) ∧ (∀x y z : set, x ∈ power_real J → y ∈ power_real J → z ∈ power_real J → ¬ (Rlt (add_SNo (apply_fun (uniform_metric_power_real J) (x,y)) (apply_fun (uniform_metric_power_real J) (y,z))) (apply_fun (uniform_metric_power_real J) (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_power_real_function_on J).
Let x and y be given.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
rewrite the current goal using (uniform_metric_power_real_apply J x y Hx Hy) (from left to right).
rewrite the current goal using (uniform_metric_power_real_apply J y x Hy Hx) (from left to right).
An exact proof term for the current goal is (power_real_uniform_metric_value_sym J x y Hx Hy).
Let x be given.
Assume Hx: x ∈ power_real J.
rewrite the current goal using (uniform_metric_power_real_apply J x x Hx Hx) (from left to right).
An exact proof term for the current goal is (power_real_uniform_metric_value_self_zero J x Hx).
Let x and y be given.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
We will prove ¬ (Rlt (apply_fun (uniform_metric_power_real J) (x,y)) 0) ∧ (apply_fun (uniform_metric_power_real J) (x,y) = 0 → x = y).
Apply andI to the current goal.
rewrite the current goal using (uniform_metric_power_real_apply J x y Hx Hy) (from left to right).
An exact proof term for the current goal is (power_real_uniform_metric_value_nonneg J x y Hx Hy).
Assume H0: apply_fun (uniform_metric_power_real J) (x,y) = 0.
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
We prove the intermediate claim HXeq: power_real J = {Empty}.
We prove the intermediate claim HdefPow: power_real J = product_space J (const_space_family J R R_standard_topology).
Use reflexivity.
rewrite the current goal using HdefPow (from left to right).
rewrite the current goal using HJ0 (from left to right).
An exact proof term for the current goal is (product_space_empty_index (const_space_family Empty R R_standard_topology)).
We prove the intermediate claim HxSing: x ∈ {Empty}.
rewrite the current goal using HXeq (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HySing: y ∈ {Empty}.
rewrite the current goal using HXeq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HxE: x = Empty.
An exact proof term for the current goal is (SingE Empty x HxSing).
We prove the intermediate claim HyE: y = Empty.
An exact proof term for the current goal is (SingE Empty y HySing).
rewrite the current goal using HxE (from left to right).
rewrite the current goal using HyE (from left to right).
Use reflexivity.
Assume HJne: ¬ (J = Empty).
We prove the intermediate claim HJne2: J ≠ Empty.
An exact proof term for the current goal is HJne.
We prove the intermediate claim Hval0: power_real_uniform_metric_value J x y = 0.
rewrite the current goal using (uniform_metric_power_real_apply J x y Hx Hy) (from right to left).
An exact proof term for the current goal is H0.
We prove the intermediate claim Hcoord: ∀j : set, j ∈ J → apply_fun x j = apply_fun y j.
Let j be given.
Assume HjJ: j ∈ J.
An exact proof term for the current goal is (power_real_uniform_metric_value_eq0_coord_eq J x y j HJne2 Hx Hy HjJ Hval0).
An exact proof term for the current goal is (power_real_ext J x y Hx Hy Hcoord).
Let x, y and z be given.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
Assume Hz: z ∈ power_real J.
rewrite the current goal using (uniform_metric_power_real_apply J x y Hx Hy) (from left to right).
rewrite the current goal using (uniform_metric_power_real_apply J y z Hy Hz) (from left to right).
rewrite the current goal using (uniform_metric_power_real_apply J x z Hx Hz) (from left to right).
An exact proof term for the current goal is (power_real_uniform_metric_value_triangle J x y z Hx Hy Hz).
∎