We will prove metric_on_total EuclidPlane EuclidPlane_metric.
We will prove metric_on EuclidPlane EuclidPlane_metric ∧ total_function_on EuclidPlane_metric (setprod EuclidPlane EuclidPlane) R.
Apply andI to the current goal.
An exact proof term for the current goal is EuclidPlane_metric_is_metric_on.
We will prove total_function_on EuclidPlane_metric (setprod EuclidPlane EuclidPlane) R.
We will prove function_on EuclidPlane_metric (setprod EuclidPlane EuclidPlane) R ∧ ∀pq : set, pq ∈ (setprod EuclidPlane EuclidPlane) → ∃y : set, y ∈ R ∧ (pq,y) ∈ EuclidPlane_metric.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_on_function_on EuclidPlane EuclidPlane_metric EuclidPlane_metric_is_metric_on).
Let pq be given.
Assume Hpq: pq ∈ (setprod EuclidPlane EuclidPlane).
We will prove ∃y : set, y ∈ R ∧ (pq,y) ∈ EuclidPlane_metric.
We use (distance_R2 (pq 0) (pq 1)) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hp: (pq 0) ∈ EuclidPlane.
An exact proof term for the current goal is (ap0_Sigma EuclidPlane (λ_ : set ⇒ EuclidPlane) pq Hpq).
We prove the intermediate claim Hq: (pq 1) ∈ EuclidPlane.
An exact proof term for the current goal is (ap1_Sigma EuclidPlane (λ_ : set ⇒ EuclidPlane) pq Hpq).
An exact proof term for the current goal is (distance_R2_in_R (pq 0) (pq 1) Hp Hq).
An exact proof term for the current goal is (ReplI (setprod EuclidPlane EuclidPlane) (λpq0 : set ⇒ (pq0,distance_R2 (pq0 0) (pq0 1))) pq Hpq).
∎