Metamath Proof Explorer

Theorem elntg2

Description: The line definition in the Tarski structure for the Euclidean geometry. In contrast to elntg , the betweenness can be strengthened by excluding 1 resp. 0 from the related intervals (because of x =/= y ). (Contributed by AV, 14-Feb-2023)

Ref Expression
Hypotheses elntg2.1 ${⊢}{P}={\mathrm{Base}}_{{𝔼}_{𝒢}\left({N}\right)}$
elntg2.2 ${⊢}{I}=\left(1\dots {N}\right)$
Assertion elntg2 ${⊢}{N}\in ℕ\to {Line}_{𝒢}\left({𝔼}_{𝒢}\left({N}\right)\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{p}\in {P}|\left(\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right\}\right)$

Proof

Step Hyp Ref Expression
1 elntg2.1 ${⊢}{P}={\mathrm{Base}}_{{𝔼}_{𝒢}\left({N}\right)}$
2 elntg2.2 ${⊢}{I}=\left(1\dots {N}\right)$
3 eqid ${⊢}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right)=\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right)$
4 1 3 elntg ${⊢}{N}\in ℕ\to {Line}_{𝒢}\left({𝔼}_{𝒢}\left({N}\right)\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{p}\in {P}|\left({p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)\right)\right\}\right)$
5 simpl1 ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {N}\in ℕ$
6 simpl2 ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {x}\in {P}$
7 eldifi ${⊢}{y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in {P}$
8 7 3ad2ant3 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {y}\in {P}$
9 8 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {y}\in {P}$
10 simpr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {p}\in {P}$
11 5 1 3 6 9 10 ebtwntg ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({p}\mathrm{Btwn}⟨{x},{y}⟩↔{p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\right)$
12 eengbas ${⊢}{N}\in ℕ\to 𝔼\left({N}\right)={\mathrm{Base}}_{{𝔼}_{𝒢}\left({N}\right)}$
13 12 1 syl6reqr ${⊢}{N}\in ℕ\to {P}=𝔼\left({N}\right)$
14 13 3ad2ant1 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {P}=𝔼\left({N}\right)$
15 14 eleq2d ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to \left({p}\in {P}↔{p}\in 𝔼\left({N}\right)\right)$
16 15 biimpa ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {p}\in 𝔼\left({N}\right)$
17 13 eleq2d ${⊢}{N}\in ℕ\to \left({x}\in {P}↔{x}\in 𝔼\left({N}\right)\right)$
18 17 biimpa ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\right)\to {x}\in 𝔼\left({N}\right)$
19 18 3adant3 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {x}\in 𝔼\left({N}\right)$
20 19 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {x}\in 𝔼\left({N}\right)$
21 13 eleq2d ${⊢}{N}\in ℕ\to \left({y}\in {P}↔{y}\in 𝔼\left({N}\right)\right)$
22 21 biimpcd ${⊢}{y}\in {P}\to \left({N}\in ℕ\to {y}\in 𝔼\left({N}\right)\right)$
23 22 7 syl11 ${⊢}{N}\in ℕ\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in 𝔼\left({N}\right)\right)$
24 23 a1d ${⊢}{N}\in ℕ\to \left({x}\in {P}\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in 𝔼\left({N}\right)\right)\right)$
25 24 3imp ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {y}\in 𝔼\left({N}\right)$
26 25 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {y}\in 𝔼\left({N}\right)$
27 brbtwn ${⊢}\left({p}\in 𝔼\left({N}\right)\wedge {x}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)\to \left({p}\mathrm{Btwn}⟨{x},{y}⟩↔\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\right)$
28 16 20 26 27 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({p}\mathrm{Btwn}⟨{x},{y}⟩↔\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\right)$
29 2 raleqi ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)$
30 29 rexbii ${⊢}\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)↔\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)$
31 28 30 syl6bbr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({p}\mathrm{Btwn}⟨{x},{y}⟩↔\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\right)$
32 11 31 bitr3d ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)↔\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\right)$
33 5 1 3 10 9 6 ebtwntg ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({x}\mathrm{Btwn}⟨{p},{y}⟩↔{x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\right)$
34 brbtwn ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{p},{y}⟩↔\exists {l}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
35 20 16 26 34 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({x}\mathrm{Btwn}⟨{p},{y}⟩↔\exists {l}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
36 33 35 bitr3d ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)↔\exists {l}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
37 0xr ${⊢}0\in {ℝ}^{*}$
38 1xr ${⊢}1\in {ℝ}^{*}$
39 0le1 ${⊢}0\le 1$
40 snunico ${⊢}\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge 0\le 1\right)\to \left[0,1\right)\cup \left\{1\right\}=\left[0,1\right]$
41 37 38 39 40 mp3an ${⊢}\left[0,1\right)\cup \left\{1\right\}=\left[0,1\right]$
42 41 eqcomi ${⊢}\left[0,1\right]=\left[0,1\right)\cup \left\{1\right\}$
43 42 a1i ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left[0,1\right]=\left[0,1\right)\cup \left\{1\right\}$
44 43 rexeqdv ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {l}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\exists {l}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
45 rexun ${⊢}\exists {l}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
46 eldifsn ${⊢}{y}\in \left({P}\setminus \left\{{x}\right\}\right)↔\left({y}\in {P}\wedge {y}\ne {x}\right)$
47 elee ${⊢}{N}\in ℕ\to \left({x}\in 𝔼\left({N}\right)↔{x}:\left(1\dots {N}\right)⟶ℝ\right)$
48 ffn ${⊢}{x}:\left(1\dots {N}\right)⟶ℝ\to {x}Fn\left(1\dots {N}\right)$
49 47 48 syl6bi ${⊢}{N}\in ℕ\to \left({x}\in 𝔼\left({N}\right)\to {x}Fn\left(1\dots {N}\right)\right)$
50 17 49 sylbid ${⊢}{N}\in ℕ\to \left({x}\in {P}\to {x}Fn\left(1\dots {N}\right)\right)$
51 50 a1i ${⊢}{y}\in {P}\to \left({N}\in ℕ\to \left({x}\in {P}\to {x}Fn\left(1\dots {N}\right)\right)\right)$
52 51 3imp ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to {x}Fn\left(1\dots {N}\right)$
53 elee ${⊢}{N}\in ℕ\to \left({y}\in 𝔼\left({N}\right)↔{y}:\left(1\dots {N}\right)⟶ℝ\right)$
54 ffn ${⊢}{y}:\left(1\dots {N}\right)⟶ℝ\to {y}Fn\left(1\dots {N}\right)$
55 53 54 syl6bi ${⊢}{N}\in ℕ\to \left({y}\in 𝔼\left({N}\right)\to {y}Fn\left(1\dots {N}\right)\right)$
56 21 55 sylbid ${⊢}{N}\in ℕ\to \left({y}\in {P}\to {y}Fn\left(1\dots {N}\right)\right)$
57 56 a1i ${⊢}{x}\in {P}\to \left({N}\in ℕ\to \left({y}\in {P}\to {y}Fn\left(1\dots {N}\right)\right)\right)$
58 57 3imp31 ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to {y}Fn\left(1\dots {N}\right)$
59 eqfnfv ${⊢}\left({x}Fn\left(1\dots {N}\right)\wedge {y}Fn\left(1\dots {N}\right)\right)\to \left({x}={y}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
60 52 58 59 syl2anc ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to \left({x}={y}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
61 60 biimprd ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\to {x}={y}\right)$
62 eqcom ${⊢}{y}={x}↔{x}={y}$
63 61 62 syl6ibr ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\to {y}={x}\right)$
64 63 necon3ad ${⊢}\left({y}\in {P}\wedge {N}\in ℕ\wedge {x}\in {P}\right)\to \left({y}\ne {x}\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
65 64 3exp ${⊢}{y}\in {P}\to \left({N}\in ℕ\to \left({x}\in {P}\to \left({y}\ne {x}\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)\right)\right)$
66 65 com24 ${⊢}{y}\in {P}\to \left({y}\ne {x}\to \left({x}\in {P}\to \left({N}\in ℕ\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)\right)\right)$
67 66 imp ${⊢}\left({y}\in {P}\wedge {y}\ne {x}\right)\to \left({x}\in {P}\to \left({N}\in ℕ\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)\right)$
68 46 67 sylbi ${⊢}{y}\in \left({P}\setminus \left\{{x}\right\}\right)\to \left({x}\in {P}\to \left({N}\in ℕ\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)\right)$
69 68 3imp31 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)$
70 69 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)$
71 13 eleq2d ${⊢}{N}\in ℕ\to \left({p}\in {P}↔{p}\in 𝔼\left({N}\right)\right)$
72 elee ${⊢}{N}\in ℕ\to \left({p}\in 𝔼\left({N}\right)↔{p}:\left(1\dots {N}\right)⟶ℝ\right)$
73 72 biimpd ${⊢}{N}\in ℕ\to \left({p}\in 𝔼\left({N}\right)\to {p}:\left(1\dots {N}\right)⟶ℝ\right)$
74 71 73 sylbid ${⊢}{N}\in ℕ\to \left({p}\in {P}\to {p}:\left(1\dots {N}\right)⟶ℝ\right)$
75 74 3ad2ant1 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to \left({p}\in {P}\to {p}:\left(1\dots {N}\right)⟶ℝ\right)$
76 75 imp ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {p}:\left(1\dots {N}\right)⟶ℝ$
77 76 ffvelrnda ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {p}\left({i}\right)\in ℝ$
78 77 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {p}\left({i}\right)\in ℂ$
79 78 mul02d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0\cdot {p}\left({i}\right)=0$
80 22 53 mpbidi ${⊢}{y}\in {P}\to \left({N}\in ℕ\to {y}:\left(1\dots {N}\right)⟶ℝ\right)$
81 80 7 syl11 ${⊢}{N}\in ℕ\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}:\left(1\dots {N}\right)⟶ℝ\right)$
82 81 a1d ${⊢}{N}\in ℕ\to \left({x}\in {P}\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}:\left(1\dots {N}\right)⟶ℝ\right)\right)$
83 82 3imp ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {y}:\left(1\dots {N}\right)⟶ℝ$
84 83 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {y}:\left(1\dots {N}\right)⟶ℝ$
85 84 ffvelrnda ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {y}\left({i}\right)\in ℝ$
86 85 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {y}\left({i}\right)\in ℂ$
87 86 mulid2d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1{y}\left({i}\right)={y}\left({i}\right)$
88 79 87 oveq12d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0\cdot {p}\left({i}\right)+1{y}\left({i}\right)=0+{y}\left({i}\right)$
89 86 addid2d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0+{y}\left({i}\right)={y}\left({i}\right)$
90 88 89 eqtrd ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0\cdot {p}\left({i}\right)+1{y}\left({i}\right)={y}\left({i}\right)$
91 90 eqeq2d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)↔{x}\left({i}\right)={y}\left({i}\right)\right)$
92 91 ralbidva ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
93 70 92 mtbird ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)$
94 1re ${⊢}1\in ℝ$
95 oveq2 ${⊢}{l}=1\to 1-{l}=1-1$
96 95 oveq1d ${⊢}{l}=1\to \left(1-{l}\right){p}\left({i}\right)=\left(1-1\right){p}\left({i}\right)$
97 1m1e0 ${⊢}1-1=0$
98 97 oveq1i ${⊢}\left(1-1\right){p}\left({i}\right)=0\cdot {p}\left({i}\right)$
99 96 98 syl6eq ${⊢}{l}=1\to \left(1-{l}\right){p}\left({i}\right)=0\cdot {p}\left({i}\right)$
100 oveq1 ${⊢}{l}=1\to {l}{y}\left({i}\right)=1{y}\left({i}\right)$
101 99 100 oveq12d ${⊢}{l}=1\to \left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)$
102 101 eqeq2d ${⊢}{l}=1\to \left({x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)\right)$
103 102 ralbidv ${⊢}{l}=1\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)\right)$
104 103 rexsng ${⊢}1\in ℝ\to \left(\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)\right)$
105 94 104 ax-mp ${⊢}\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=0\cdot {p}\left({i}\right)+1{y}\left({i}\right)$
106 93 105 sylnibr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)$
107 2 raleqi ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)$
108 107 rexbii ${⊢}\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)$
109 biorf ${⊢}¬\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\to \left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\left(\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)\right)$
110 108 109 syl5bb ${⊢}¬\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\to \left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\left(\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)\right)$
111 106 110 syl ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\left(\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)\right)$
112 orcom ${⊢}\left(\exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)↔\left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
113 111 112 syl6rbb ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\left(\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {l}\in \left\{1\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)↔\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
114 45 113 syl5bb ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {l}\in \left(\left[0,1\right)\cup \left\{1\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)↔\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
115 36 44 114 3bitrd ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)↔\exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\right)$
116 5 1 3 6 10 9 ebtwntg ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({y}\mathrm{Btwn}⟨{x},{p}⟩↔{y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)\right)$
117 brbtwn ${⊢}\left({y}\in 𝔼\left({N}\right)\wedge {x}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\to \left({y}\mathrm{Btwn}⟨{x},{p}⟩↔\exists {m}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
118 26 20 16 117 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({y}\mathrm{Btwn}⟨{x},{p}⟩↔\exists {m}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
119 116 118 bitr3d ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)↔\exists {m}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
120 snunioc ${⊢}\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge 0\le 1\right)\to \left\{0\right\}\cup \left(0,1\right]=\left[0,1\right]$
121 37 38 39 120 mp3an ${⊢}\left\{0\right\}\cup \left(0,1\right]=\left[0,1\right]$
122 121 eqcomi ${⊢}\left[0,1\right]=\left\{0\right\}\cup \left(0,1\right]$
123 122 a1i ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left[0,1\right]=\left\{0\right\}\cup \left(0,1\right]$
124 123 rexeqdv ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {m}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\exists {m}\in \left(\left\{0\right\}\cup \left(0,1\right]\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
125 eqcom ${⊢}{x}\left({i}\right)={y}\left({i}\right)↔{y}\left({i}\right)={x}\left({i}\right)$
126 125 ralbii ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)={x}\left({i}\right)$
127 70 126 sylnib ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)={x}\left({i}\right)$
128 17 biimpd ${⊢}{N}\in ℕ\to \left({x}\in {P}\to {x}\in 𝔼\left({N}\right)\right)$
129 128 47 sylibd ${⊢}{N}\in ℕ\to \left({x}\in {P}\to {x}:\left(1\dots {N}\right)⟶ℝ\right)$
130 129 imp ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\right)\to {x}:\left(1\dots {N}\right)⟶ℝ$
131 130 3adant3 ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {x}:\left(1\dots {N}\right)⟶ℝ$
132 131 adantr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {x}:\left(1\dots {N}\right)⟶ℝ$
133 132 ffvelrnda ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)\in ℝ$
134 133 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)\in ℂ$
135 134 mulid2d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1{x}\left({i}\right)={x}\left({i}\right)$
136 135 79 oveq12d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1{x}\left({i}\right)+0\cdot {p}\left({i}\right)={x}\left({i}\right)+0$
137 134 addid1d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)+0={x}\left({i}\right)$
138 136 137 eqtrd ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1{x}\left({i}\right)+0\cdot {p}\left({i}\right)={x}\left({i}\right)$
139 138 eqeq2d ${⊢}\left(\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)↔{y}\left({i}\right)={x}\left({i}\right)\right)$
140 139 ralbidva ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)={x}\left({i}\right)\right)$
141 127 140 mtbird ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)$
142 0re ${⊢}0\in ℝ$
143 oveq2 ${⊢}{m}=0\to 1-{m}=1-0$
144 143 oveq1d ${⊢}{m}=0\to \left(1-{m}\right){x}\left({i}\right)=\left(1-0\right){x}\left({i}\right)$
145 1m0e1 ${⊢}1-0=1$
146 145 oveq1i ${⊢}\left(1-0\right){x}\left({i}\right)=1{x}\left({i}\right)$
147 144 146 syl6eq ${⊢}{m}=0\to \left(1-{m}\right){x}\left({i}\right)=1{x}\left({i}\right)$
148 oveq1 ${⊢}{m}=0\to {m}{p}\left({i}\right)=0\cdot {p}\left({i}\right)$
149 147 148 oveq12d ${⊢}{m}=0\to \left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)$
150 149 eqeq2d ${⊢}{m}=0\to \left({y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)\right)$
151 150 ralbidv ${⊢}{m}=0\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)\right)$
152 151 rexsng ${⊢}0\in ℝ\to \left(\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)\right)$
153 142 152 ax-mp ${⊢}\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=1{x}\left({i}\right)+0\cdot {p}\left({i}\right)$
154 141 153 sylnibr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to ¬\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)$
155 2 raleqi ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)$
156 155 rexbii ${⊢}\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)$
157 biorf ${⊢}¬\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\to \left(\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\left(\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right)$
158 156 157 syl5bb ${⊢}¬\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\to \left(\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\left(\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right)$
159 154 158 syl ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\left(\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right)$
160 rexun ${⊢}\exists {m}\in \left(\left\{0\right\}\cup \left(0,1\right]\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\left(\exists {m}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
161 159 160 syl6rbbr ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {m}\in \left(\left\{0\right\}\cup \left(0,1\right]\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)↔\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
162 119 124 161 3bitrd ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left({y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)↔\exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)$
163 32 115 162 3orbi123d ${⊢}\left(\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to \left(\left({p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)\right)↔\left(\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right)$
164 163 rabbidva ${⊢}\left({N}\in ℕ\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to \left\{{p}\in {P}|\left({p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)\right)\right\}=\left\{{p}\in {P}|\left(\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right\}$
165 164 mpoeq3dva ${⊢}{N}\in ℕ\to \left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{p}\in {P}|\left({p}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {x}\in \left({p}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){y}\right)\vee {y}\in \left({x}\mathrm{Itv}\left({𝔼}_{𝒢}\left({N}\right)\right){p}\right)\right)\right\}\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{p}\in {P}|\left(\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right\}\right)$
166 4 165 eqtrd ${⊢}{N}\in ℕ\to {Line}_{𝒢}\left({𝔼}_{𝒢}\left({N}\right)\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\left\{{p}\in {P}|\left(\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{k}\right){x}\left({i}\right)+{k}{y}\left({i}\right)\vee \exists {l}\in \left[0,1\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{l}\right){p}\left({i}\right)+{l}{y}\left({i}\right)\vee \exists {m}\in \left(0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{m}\right){x}\left({i}\right)+{m}{p}\left({i}\right)\right)\right\}\right)$