Let x0, x1 and y0 be given.
Assume Hy0R: y0 ∈ R.
Assume Hy0ne: y0 ≠ 0.
Assume Hx0R: x0 ∈ R.
Assume Hx1R: x1 ∈ R.
Set X to be the term EuclidPlane ∖ {(0,0)}.
Set Tx to be the term subspace_topology EuclidPlane R2_standard_topology X.
We will prove (x0,y0) ∈ path_component_of X Tx (x1,y0).
We will prove (x0,y0) ∈ {y ∈ X|∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = (x1,y0) ∧ apply_fun p 1 = y}.
Apply SepI to the current goal.
Apply (setminusI EuclidPlane {(0,0)} (x0,y0)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x0 y0 Hx0R Hy0R).
Assume H0: (x0,y0) ∈ {(0,0)}.
We prove the intermediate claim Heq: (x0,y0) = (0,0).
An exact proof term for the current goal is (SingE (0,0) (x0,y0) H0).
We prove the intermediate claim Hcoords: x0 = 0 ∧ y0 = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 x0 y0 0 0 Heq).
An exact proof term for the current goal is (Hy0ne (andER (x0 = 0) (y0 = 0) Hcoords)).
We will prove ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = (x1,y0) ∧ apply_fun p 1 = (x0,y0).
Set c to be the term add_SNo x0 (minus_SNo x1).
We prove the intermediate claim Hm1R: minus_SNo x1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo x1 Hx1R).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (real_add_SNo x0 Hx0R (minus_SNo x1) Hm1R).
Set mul to be the term mul_const_fun c.
Set cx1 to be the term const_fun R x1.
Set pair to be the term pair_map R cx1 mul.
Set hR to be the term compose_fun R pair add_fun_R.
We prove the intermediate claim Hcx1cont: continuous_map R R_standard_topology R R_standard_topology cx1.
An exact proof term for the current goal is (const_fun_continuous R R_standard_topology R R_standard_topology x1 R_standard_topology_is_topology R_standard_topology_is_topology Hx1R).
We prove the intermediate claim Hmulcont: continuous_map R R_standard_topology R R_standard_topology mul.
An exact proof term for the current goal is (mul_const_fun_continuous c HcR).
We prove the intermediate claim Hpaircont: continuous_map R R_standard_topology (setprod R R) (product_topology R R_standard_topology R R_standard_topology) pair.
An exact proof term for the current goal is (maps_into_products_axiom R R_standard_topology R R_standard_topology R R_standard_topology cx1 mul Hcx1cont Hmulcont).
We prove the intermediate claim Haddcont: continuous_map (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology add_fun_R.
An exact proof term for the current goal is add_fun_R_continuous.
We prove the intermediate claim HhRcont: continuous_map R R_standard_topology R R_standard_topology hR.
An exact proof term for the current goal is (composition_continuous R R_standard_topology (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology pair add_fun_R Hpaircont Haddcont).
Set j to be the term {(t,t)|t ∈ unit_interval}.
We prove the intermediate claim Hjcont: continuous_map unit_interval unit_interval_topology R R_standard_topology j.
An exact proof term for the current goal is unit_interval_inclusion_continuous.
Set g to be the term compose_fun unit_interval j hR.
We prove the intermediate claim Hgcont: continuous_map unit_interval unit_interval_topology R R_standard_topology g.
An exact proof term for the current goal is (composition_continuous unit_interval unit_interval_topology R R_standard_topology R R_standard_topology j hR Hjcont HhRcont).
Set consty to be the term const_fun unit_interval y0.
We prove the intermediate claim Hconstycont: continuous_map unit_interval unit_interval_topology R R_standard_topology consty.
An exact proof term for the current goal is (const_fun_continuous unit_interval unit_interval_topology R R_standard_topology y0 unit_interval_topology_on R_standard_topology_is_topology Hy0R).
Set p0 to be the term pair_map unit_interval g consty.
We prove the intermediate claim Hp0contPlane: continuous_map unit_interval unit_interval_topology EuclidPlane R2_standard_topology p0.
We prove the intermediate claim Heq: EuclidPlane = setprod R R.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (maps_into_products_axiom unit_interval unit_interval_topology R R_standard_topology R R_standard_topology g consty Hgcont Hconstycont).
We prove the intermediate claim HimgX: ∀t : set, t ∈ unit_interval → apply_fun p0 t ∈ X.
Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove apply_fun p0 t ∈ X.
We prove the intermediate claim HgtR: apply_fun g t ∈ R.
An exact proof term for the current goal is (continuous_map_function_on unit_interval unit_interval_topology R R_standard_topology g Hgcont t HtI).
We prove the intermediate claim HytR: apply_fun consty t ∈ R.
An exact proof term for the current goal is (continuous_map_function_on unit_interval unit_interval_topology R R_standard_topology consty Hconstycont t HtI).
We prove the intermediate claim Hp0t: apply_fun p0 t = (apply_fun g t,apply_fun consty t).
An exact proof term for the current goal is (pair_map_apply unit_interval R R g consty t HtI).
rewrite the current goal using Hp0t (from left to right).
We prove the intermediate claim Hcst: apply_fun consty t = y0.
An exact proof term for the current goal is (const_fun_apply unit_interval y0 t HtI).
rewrite the current goal using Hcst (from left to right).
Apply (setminusI EuclidPlane {(0,0)} (apply_fun g t,y0)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun g t) y0 HgtR Hy0R).
Assume H0: (apply_fun g t,y0) ∈ {(0,0)}.
We prove the intermediate claim Heq0: (apply_fun g t,y0) = (0,0).
An exact proof term for the current goal is (SingE (0,0) (apply_fun g t,y0) H0).
We prove the intermediate claim Hcoords: apply_fun g t = 0 ∧ y0 = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 (apply_fun g t) y0 0 0 Heq0).
An exact proof term for the current goal is (Hy0ne (andER (apply_fun g t = 0) (y0 = 0) Hcoords)).
We prove the intermediate claim HXsub: X ⊆ EuclidPlane.
An exact proof term for the current goal is (setminus_Subq EuclidPlane {(0,0)}).
We prove the intermediate claim Hp0cont: continuous_map unit_interval unit_interval_topology X Tx p0.
An exact proof term for the current goal is (continuous_map_range_restrict unit_interval unit_interval_topology EuclidPlane R2_standard_topology p0 X Hp0contPlane HXsub HimgX).
We prove the intermediate claim Hp0fun: function_on p0 unit_interval X.
An exact proof term for the current goal is (continuous_map_function_on unit_interval unit_interval_topology X Tx p0 Hp0cont).
We prove the intermediate claim H0I: 0 ∈ unit_interval.
An exact proof term for the current goal is zero_in_unit_interval.
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is one_in_unit_interval.
We prove the intermediate claim Hp0_0: apply_fun p0 0 = (x1,y0).
rewrite the current goal using (pair_map_apply unit_interval R R g consty 0 H0I) (from left to right).
rewrite the current goal using (const_fun_apply unit_interval y0 0 H0I) (from left to right).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
rewrite the current goal using (compose_fun_apply unit_interval j hR 0 H0I) (from left to right).
rewrite the current goal using (identity_function_apply unit_interval 0 H0I) (from left to right).
rewrite the current goal using (compose_fun_apply R pair add_fun_R 0 H0R) (from left to right).
We prove the intermediate claim Hpair0: apply_fun pair 0 = (apply_fun cx1 0,apply_fun mul 0).
An exact proof term for the current goal is (pair_map_apply R R R cx1 mul 0 H0R).
rewrite the current goal using Hpair0 (from left to right).
rewrite the current goal using (const_fun_apply R x1 0 H0R) (from left to right).
rewrite the current goal using (mul_const_fun_apply c 0 HcR H0R) (from left to right).
We prove the intermediate claim Hmul0R: mul_SNo 0 c ∈ R.
An exact proof term for the current goal is (real_mul_SNo 0 H0R c HcR).
We prove the intermediate claim HpairRR: (x1,mul_SNo 0 c) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x1 (mul_SNo 0 c) Hx1R Hmul0R).
rewrite the current goal using (add_fun_R_apply (x1,mul_SNo 0 c) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq x1 (mul_SNo 0 c)) (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (mul_SNo 0 c)) (from left to right).
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1R).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
rewrite the current goal using (mul_SNo_zeroL c HcS) (from left to right).
rewrite the current goal using (add_SNo_0R x1 Hx1S) (from left to right).
Use reflexivity.
We prove the intermediate claim Hp0_1: apply_fun p0 1 = (x0,y0).
rewrite the current goal using (pair_map_apply unit_interval R R g consty 1 H1I) (from left to right).
rewrite the current goal using (const_fun_apply unit_interval y0 1 H1I) (from left to right).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
rewrite the current goal using (compose_fun_apply unit_interval j hR 1 H1I) (from left to right).
rewrite the current goal using (identity_function_apply unit_interval 1 H1I) (from left to right).
rewrite the current goal using (compose_fun_apply R pair add_fun_R 1 H1R) (from left to right).
We prove the intermediate claim Hpair1: apply_fun pair 1 = (apply_fun cx1 1,apply_fun mul 1).
An exact proof term for the current goal is (pair_map_apply R R R cx1 mul 1 H1R).
rewrite the current goal using Hpair1 (from left to right).
rewrite the current goal using (const_fun_apply R x1 1 H1R) (from left to right).
rewrite the current goal using (mul_const_fun_apply c 1 HcR H1R) (from left to right).
We prove the intermediate claim Hmul1R: mul_SNo 1 c ∈ R.
An exact proof term for the current goal is (real_mul_SNo 1 H1R c HcR).
We prove the intermediate claim HpairRR: (x1,mul_SNo 1 c) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x1 (mul_SNo 1 c) Hx1R Hmul1R).
rewrite the current goal using (add_fun_R_apply (x1,mul_SNo 1 c) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq x1 (mul_SNo 1 c)) (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (mul_SNo 1 c)) (from left to right).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0R).
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1R).
We prove the intermediate claim Hm1S: SNo (minus_SNo x1).
An exact proof term for the current goal is (real_SNo (minus_SNo x1) Hm1R).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
rewrite the current goal using (mul_SNo_oneL c HcS) (from left to right).
We prove the intermediate claim Hcdef: c = add_SNo x0 (minus_SNo x1).
Use reflexivity.
rewrite the current goal using Hcdef (from left to right) at position 1.
rewrite the current goal using (add_SNo_com x0 (minus_SNo x1) Hx0S Hm1S) (from left to right).
rewrite the current goal using (add_SNo_assoc x1 (minus_SNo x1) x0 Hx1S Hm1S Hx0S) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv x1 Hx1S) (from left to right).
rewrite the current goal using (add_SNo_0L x0 Hx0S) (from left to right).
Use reflexivity.
We use p0 to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hp0fun.
An exact proof term for the current goal is Hp0cont.
An exact proof term for the current goal is Hp0_0.
An exact proof term for the current goal is Hp0_1.
∎