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 = ( Base ` ( EEG ` N ) )
elntg2.2 
|- I = ( 1 ... N )
Assertion elntg2 
|- ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | ( E. k e. ( 0 [,] 1 ) A. i e. I ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. I ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. I ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) } ) )

Proof

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