Let x0, y0 and y1 be given.
Assume Hx0R: x0 ∈ R.
Assume Hx0ne: x0 ≠ 0.
Assume Hy0R: y0 ∈ R.
Assume Hy1R: y1 ∈ 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 (x0,y1).
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 = (x0,y1) ∧ 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 (Hx0ne (andEL (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 = (x0,y1) ∧ apply_fun p 1 = (x0,y0).
Set c to be the term add_SNo y0 (minus_SNo y1).
We prove the intermediate claim Hm1R: minus_SNo y1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo y1 Hy1R).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (real_add_SNo y0 Hy0R (minus_SNo y1) Hm1R).
Set mul to be the term mul_const_fun c.
Set cy1 to be the term const_fun R y1.
Set pair to be the term pair_map R cy1 mul.
Set hR to be the term compose_fun R pair add_fun_R.
We prove the intermediate claim Hcy1cont: continuous_map R R_standard_topology R R_standard_topology cy1.
An exact proof term for the current goal is (const_fun_continuous R R_standard_topology R R_standard_topology y1 R_standard_topology_is_topology R_standard_topology_is_topology Hy1R).
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 cy1 mul Hcy1cont 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 constx to be the term const_fun unit_interval x0.
We prove the intermediate claim Hconstxcont: continuous_map unit_interval unit_interval_topology R R_standard_topology constx.
An exact proof term for the current goal is (const_fun_continuous unit_interval unit_interval_topology R R_standard_topology x0 unit_interval_topology_on R_standard_topology_is_topology Hx0R).
Set p0 to be the term pair_map unit_interval constx g.
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 constx g Hconstxcont Hgcont).
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 HxtR: apply_fun constx t ∈ R.
An exact proof term for the current goal is (continuous_map_function_on unit_interval unit_interval_topology R R_standard_topology constx Hconstxcont t HtI).
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 Hp0t: apply_fun p0 t = (apply_fun constx t,apply_fun g t).
An exact proof term for the current goal is (pair_map_apply unit_interval R R constx g t HtI).
rewrite the current goal using Hp0t (from left to right).
We prove the intermediate claim Hcst: apply_fun constx t = x0.
An exact proof term for the current goal is (const_fun_apply unit_interval x0 t HtI).
rewrite the current goal using Hcst (from left to right).
Apply (setminusI EuclidPlane {(0,0)} (x0,apply_fun g t)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x0 (apply_fun g t) Hx0R HgtR).
Assume H0: (x0,apply_fun g t) ∈ {(0,0)}.
We prove the intermediate claim Heq0: (x0,apply_fun g t) = (0,0).
An exact proof term for the current goal is (SingE (0,0) (x0,apply_fun g t) H0).
We prove the intermediate claim Hcoords: x0 = 0 ∧ apply_fun g t = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 x0 (apply_fun g t) 0 0 Heq0).
An exact proof term for the current goal is (Hx0ne (andEL (x0 = 0) (apply_fun g t = 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 = (x0,y1).
rewrite the current goal using (pair_map_apply unit_interval R R constx g 0 H0I) (from left to right).
rewrite the current goal using (const_fun_apply unit_interval x0 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 cy1 0,apply_fun mul 0).
An exact proof term for the current goal is (pair_map_apply R R R cy1 mul 0 H0R).
rewrite the current goal using Hpair0 (from left to right).
rewrite the current goal using (const_fun_apply R y1 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: (y1,mul_SNo 0 c) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R y1 (mul_SNo 0 c) Hy1R Hmul0R).
rewrite the current goal using (add_fun_R_apply (y1,mul_SNo 0 c) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq y1 (mul_SNo 0 c)) (from left to right).
rewrite the current goal using (tuple_2_1_eq y1 (mul_SNo 0 c)) (from left to right).
We prove the intermediate claim Hy1S: SNo y1.
An exact proof term for the current goal is (real_SNo y1 Hy1R).
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 y1 Hy1S) (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 constx g 1 H1I) (from left to right).
rewrite the current goal using (const_fun_apply unit_interval x0 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 cy1 1,apply_fun mul 1).
An exact proof term for the current goal is (pair_map_apply R R R cy1 mul 1 H1R).
rewrite the current goal using Hpair1 (from left to right).
rewrite the current goal using (const_fun_apply R y1 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: (y1,mul_SNo 1 c) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R y1 (mul_SNo 1 c) Hy1R Hmul1R).
rewrite the current goal using (add_fun_R_apply (y1,mul_SNo 1 c) HpairRR) (from left to right).
rewrite the current goal using (tuple_2_0_eq y1 (mul_SNo 1 c)) (from left to right).
rewrite the current goal using (tuple_2_1_eq y1 (mul_SNo 1 c)) (from left to right).
We prove the intermediate claim Hy0S: SNo y0.
An exact proof term for the current goal is (real_SNo y0 Hy0R).
We prove the intermediate claim Hy1S: SNo y1.
An exact proof term for the current goal is (real_SNo y1 Hy1R).
We prove the intermediate claim Hm1S: SNo (minus_SNo y1).
An exact proof term for the current goal is (real_SNo (minus_SNo y1) 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 y0 (minus_SNo y1).
Use reflexivity.
rewrite the current goal using Hcdef (from left to right) at position 1.
rewrite the current goal using (add_SNo_com y0 (minus_SNo y1) Hy0S Hm1S) (from left to right).
rewrite the current goal using (add_SNo_assoc y1 (minus_SNo y1) y0 Hy1S Hm1S Hy0S) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv y1 Hy1S) (from left to right).
rewrite the current goal using (add_SNo_0L y0 Hy0S) (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.
∎