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 ⊒ 𝑃 = ( Base β€˜ ( EEG β€˜ 𝑁 ) )
elntg2.2 ⊒ 𝐼 = ( 1 ... 𝑁 )
Assertion elntg2 ( 𝑁 ∈ β„• β†’ ( LineG β€˜ ( EEG β€˜ 𝑁 ) ) = ( π‘₯ ∈ 𝑃 , 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) } ) )

Proof

Step Hyp Ref Expression
1 elntg2.1 ⊒ 𝑃 = ( Base β€˜ ( EEG β€˜ 𝑁 ) )
2 elntg2.2 ⊒ 𝐼 = ( 1 ... 𝑁 )
3 eqid ⊒ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) = ( Itv β€˜ ( EEG β€˜ 𝑁 ) )
4 1 3 elntg ⊒ ( 𝑁 ∈ β„• β†’ ( LineG β€˜ ( EEG β€˜ 𝑁 ) ) = ( π‘₯ ∈ 𝑃 , 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ) } ) )
5 simpl1 ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑁 ∈ β„• )
6 simpl2 ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ π‘₯ ∈ 𝑃 )
7 eldifi ⊒ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ 𝑦 ∈ 𝑃 )
8 7 3ad2ant3 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ 𝑦 ∈ 𝑃 )
9 8 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑦 ∈ 𝑃 )
10 simpr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑝 ∈ 𝑃 )
11 5 1 3 6 9 10 ebtwntg ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑝 Btwn ⟨ π‘₯ , 𝑦 ⟩ ↔ 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ) )
12 eengbas ⊒ ( 𝑁 ∈ β„• β†’ ( 𝔼 β€˜ 𝑁 ) = ( Base β€˜ ( EEG β€˜ 𝑁 ) ) )
13 1 12 eqtr4id ⊒ ( 𝑁 ∈ β„• β†’ 𝑃 = ( 𝔼 β€˜ 𝑁 ) )
14 13 3ad2ant1 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ 𝑃 = ( 𝔼 β€˜ 𝑁 ) )
15 14 eleq2d ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ) )
16 15 biimpa ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) )
17 13 eleq2d ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 ↔ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ) )
18 17 biimpa ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) )
19 18 3adant3 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) )
20 19 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) )
21 13 eleq2d ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ 𝑃 ↔ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) )
22 21 biimpcd ⊒ ( 𝑦 ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) )
23 22 7 syl11 ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) )
24 23 a1d ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) ) )
25 24 3imp ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) )
26 25 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) )
27 brbtwn ⊒ ( ( 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ∧ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) β†’ ( 𝑝 Btwn ⟨ π‘₯ , 𝑦 ⟩ ↔ βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
28 16 20 26 27 syl3anc ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑝 Btwn ⟨ π‘₯ , 𝑦 ⟩ ↔ βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
29 2 raleqi ⊒ ( βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
30 29 rexbii ⊒ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
31 28 30 bitr4di ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑝 Btwn ⟨ π‘₯ , 𝑦 ⟩ ↔ βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
32 11 31 bitr3d ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ↔ βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
33 5 1 3 10 9 6 ebtwntg ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( π‘₯ Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ) )
34 brbtwn ⊒ ( ( π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ) β†’ ( π‘₯ Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ βˆƒ 𝑙 ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
35 20 16 26 34 syl3anc ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( π‘₯ Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ βˆƒ 𝑙 ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
36 33 35 bitr3d ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ↔ βˆƒ 𝑙 ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
37 0xr ⊒ 0 ∈ ℝ*
38 1xr ⊒ 1 ∈ ℝ*
39 0le1 ⊒ 0 ≀ 1
40 snunico ⊒ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≀ 1 ) β†’ ( ( 0 [,) 1 ) βˆͺ { 1 } ) = ( 0 [,] 1 ) )
41 37 38 39 40 mp3an ⊒ ( ( 0 [,) 1 ) βˆͺ { 1 } ) = ( 0 [,] 1 )
42 41 eqcomi ⊒ ( 0 [,] 1 ) = ( ( 0 [,) 1 ) βˆͺ { 1 } )
43 42 a1i ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 0 [,] 1 ) = ( ( 0 [,) 1 ) βˆͺ { 1 } ) )
44 43 rexeqdv ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ 𝑙 ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆƒ 𝑙 ∈ ( ( 0 [,) 1 ) βˆͺ { 1 } ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
45 rexun ⊒ ( βˆƒ 𝑙 ∈ ( ( 0 [,) 1 ) βˆͺ { 1 } ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
46 eldifsn ⊒ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↔ ( 𝑦 ∈ 𝑃 ∧ 𝑦 β‰  π‘₯ ) )
47 elee ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ↔ π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ ) )
48 ffn ⊒ ( π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ β†’ π‘₯ Fn ( 1 ... 𝑁 ) )
49 47 48 syl6bi ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) β†’ π‘₯ Fn ( 1 ... 𝑁 ) ) )
50 17 49 sylbid ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ π‘₯ Fn ( 1 ... 𝑁 ) ) )
51 50 a1i ⊒ ( 𝑦 ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ π‘₯ Fn ( 1 ... 𝑁 ) ) ) )
52 51 3imp ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ π‘₯ Fn ( 1 ... 𝑁 ) )
53 elee ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ↔ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
54 ffn ⊒ ( 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ β†’ 𝑦 Fn ( 1 ... 𝑁 ) )
55 53 54 syl6bi ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) β†’ 𝑦 Fn ( 1 ... 𝑁 ) ) )
56 21 55 sylbid ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ 𝑃 β†’ 𝑦 Fn ( 1 ... 𝑁 ) ) )
57 56 a1i ⊒ ( π‘₯ ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ 𝑃 β†’ 𝑦 Fn ( 1 ... 𝑁 ) ) ) )
58 57 3imp31 ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ 𝑦 Fn ( 1 ... 𝑁 ) )
59 eqfnfv ⊒ ( ( π‘₯ Fn ( 1 ... 𝑁 ) ∧ 𝑦 Fn ( 1 ... 𝑁 ) ) β†’ ( π‘₯ = 𝑦 ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) )
60 52 58 59 syl2anc ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ ( π‘₯ = 𝑦 ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) )
61 60 biimprd ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) β†’ π‘₯ = 𝑦 ) )
62 eqcom ⊒ ( 𝑦 = π‘₯ ↔ π‘₯ = 𝑦 )
63 61 62 imbitrrdi ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) β†’ 𝑦 = π‘₯ ) )
64 63 necon3ad ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ ( 𝑦 β‰  π‘₯ β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) )
65 64 3exp ⊒ ( 𝑦 ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑦 β‰  π‘₯ β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) ) ) )
66 65 com24 ⊒ ( 𝑦 ∈ 𝑃 β†’ ( 𝑦 β‰  π‘₯ β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) ) ) )
67 66 imp ⊒ ( ( 𝑦 ∈ 𝑃 ∧ 𝑦 β‰  π‘₯ ) β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) ) )
68 46 67 sylbi ⊒ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) ) )
69 68 3imp31 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) )
70 69 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) )
71 13 eleq2d ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ) )
72 elee ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ↔ 𝑝 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
73 72 biimpd ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) β†’ 𝑝 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
74 71 73 sylbid ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑝 ∈ 𝑃 β†’ 𝑝 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
75 74 3ad2ant1 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ ( 𝑝 ∈ 𝑃 β†’ 𝑝 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
76 75 imp ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑝 : ( 1 ... 𝑁 ) ⟢ ℝ )
77 76 ffvelcdmda ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝑝 β€˜ 𝑖 ) ∈ ℝ )
78 77 recnd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝑝 β€˜ 𝑖 ) ∈ β„‚ )
79 78 mul02d ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) = 0 )
80 22 53 mpbidi ⊒ ( 𝑦 ∈ 𝑃 β†’ ( 𝑁 ∈ β„• β†’ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
81 80 7 syl11 ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ ) )
82 81 a1d ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ ( 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) β†’ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ ) ) )
83 82 3imp ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ )
84 83 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ 𝑦 : ( 1 ... 𝑁 ) ⟢ ℝ )
85 84 ffvelcdmda ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝑦 β€˜ 𝑖 ) ∈ ℝ )
86 85 recnd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝑦 β€˜ 𝑖 ) ∈ β„‚ )
87 86 mullidd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) = ( 𝑦 β€˜ 𝑖 ) )
88 79 87 oveq12d ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) = ( 0 + ( 𝑦 β€˜ 𝑖 ) ) )
89 86 addlidd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 0 + ( 𝑦 β€˜ 𝑖 ) ) = ( 𝑦 β€˜ 𝑖 ) )
90 88 89 eqtrd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) = ( 𝑦 β€˜ 𝑖 ) )
91 90 eqeq2d ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) )
92 91 ralbidva ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ) )
93 70 92 mtbird ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
94 1re ⊒ 1 ∈ ℝ
95 oveq2 ⊒ ( 𝑙 = 1 β†’ ( 1 βˆ’ 𝑙 ) = ( 1 βˆ’ 1 ) )
96 95 oveq1d ⊒ ( 𝑙 = 1 β†’ ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) = ( ( 1 βˆ’ 1 ) Β· ( 𝑝 β€˜ 𝑖 ) ) )
97 1m1e0 ⊒ ( 1 βˆ’ 1 ) = 0
98 97 oveq1i ⊒ ( ( 1 βˆ’ 1 ) Β· ( 𝑝 β€˜ 𝑖 ) ) = ( 0 Β· ( 𝑝 β€˜ 𝑖 ) )
99 96 98 eqtrdi ⊒ ( 𝑙 = 1 β†’ ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) = ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) )
100 oveq1 ⊒ ( 𝑙 = 1 β†’ ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) = ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) )
101 99 100 oveq12d ⊒ ( 𝑙 = 1 β†’ ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
102 101 eqeq2d ⊒ ( 𝑙 = 1 β†’ ( ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
103 102 ralbidv ⊒ ( 𝑙 = 1 β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
104 103 rexsng ⊒ ( 1 ∈ ℝ β†’ ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
105 94 104 ax-mp ⊒ ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 1 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
106 93 105 sylnibr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
107 2 raleqi ⊒ ( βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
108 107 rexbii ⊒ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) )
109 biorf ⊒ ( Β¬ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) β†’ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) ) )
110 108 109 bitrid ⊒ ( Β¬ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) β†’ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) ) )
111 106 110 syl ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) ) )
112 orcom ⊒ ( ( βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) ↔ ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
113 111 112 bitr2di ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( ( βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ { 1 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) ↔ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
114 45 113 bitrid ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ 𝑙 ∈ ( ( 0 [,) 1 ) βˆͺ { 1 } ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ↔ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
115 36 44 114 3bitrd ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ↔ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ) )
116 5 1 3 6 10 9 ebtwntg ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑦 Btwn ⟨ π‘₯ , 𝑝 ⟩ ↔ 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ) )
117 brbtwn ⊒ ( ( 𝑦 ∈ ( 𝔼 β€˜ 𝑁 ) ∧ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 β€˜ 𝑁 ) ) β†’ ( 𝑦 Btwn ⟨ π‘₯ , 𝑝 ⟩ ↔ βˆƒ π‘š ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
118 26 20 16 117 syl3anc ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑦 Btwn ⟨ π‘₯ , 𝑝 ⟩ ↔ βˆƒ π‘š ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
119 116 118 bitr3d ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ↔ βˆƒ π‘š ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
120 snunioc ⊒ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≀ 1 ) β†’ ( { 0 } βˆͺ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) )
121 37 38 39 120 mp3an ⊒ ( { 0 } βˆͺ ( 0 (,] 1 ) ) = ( 0 [,] 1 )
122 121 eqcomi ⊒ ( 0 [,] 1 ) = ( { 0 } βˆͺ ( 0 (,] 1 ) )
123 122 a1i ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 0 [,] 1 ) = ( { 0 } βˆͺ ( 0 (,] 1 ) ) )
124 123 rexeqdv ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ π‘š ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆƒ π‘š ∈ ( { 0 } βˆͺ ( 0 (,] 1 ) ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
125 rexun ⊒ ( βˆƒ π‘š ∈ ( { 0 } βˆͺ ( 0 (,] 1 ) ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
126 eqcom ⊒ ( ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ↔ ( 𝑦 β€˜ 𝑖 ) = ( π‘₯ β€˜ 𝑖 ) )
127 126 ralbii ⊒ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( π‘₯ β€˜ 𝑖 ) = ( 𝑦 β€˜ 𝑖 ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( π‘₯ β€˜ 𝑖 ) )
128 70 127 sylnib ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( π‘₯ β€˜ 𝑖 ) )
129 17 biimpd ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ π‘₯ ∈ ( 𝔼 β€˜ 𝑁 ) ) )
130 129 47 sylibd ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 β†’ π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ ) )
131 130 imp ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ) β†’ π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ )
132 131 3adant3 ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ )
133 132 adantr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ π‘₯ : ( 1 ... 𝑁 ) ⟢ ℝ )
134 133 ffvelcdmda ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( π‘₯ β€˜ 𝑖 ) ∈ ℝ )
135 134 recnd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( π‘₯ β€˜ 𝑖 ) ∈ β„‚ )
136 135 mullidd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) = ( π‘₯ β€˜ 𝑖 ) )
137 136 79 oveq12d ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) = ( ( π‘₯ β€˜ 𝑖 ) + 0 ) )
138 135 addridd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( π‘₯ β€˜ 𝑖 ) + 0 ) = ( π‘₯ β€˜ 𝑖 ) )
139 137 138 eqtrd ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) = ( π‘₯ β€˜ 𝑖 ) )
140 139 eqeq2d ⊒ ( ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( 𝑦 β€˜ 𝑖 ) = ( π‘₯ β€˜ 𝑖 ) ) )
141 140 ralbidva ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( π‘₯ β€˜ 𝑖 ) ) )
142 128 141 mtbird ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
143 0re ⊒ 0 ∈ ℝ
144 oveq2 ⊒ ( π‘š = 0 β†’ ( 1 βˆ’ π‘š ) = ( 1 βˆ’ 0 ) )
145 144 oveq1d ⊒ ( π‘š = 0 β†’ ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) = ( ( 1 βˆ’ 0 ) Β· ( π‘₯ β€˜ 𝑖 ) ) )
146 1m0e1 ⊒ ( 1 βˆ’ 0 ) = 1
147 146 oveq1i ⊒ ( ( 1 βˆ’ 0 ) Β· ( π‘₯ β€˜ 𝑖 ) ) = ( 1 Β· ( π‘₯ β€˜ 𝑖 ) )
148 145 147 eqtrdi ⊒ ( π‘š = 0 β†’ ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) = ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) )
149 oveq1 ⊒ ( π‘š = 0 β†’ ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) = ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) )
150 148 149 oveq12d ⊒ ( π‘š = 0 β†’ ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
151 150 eqeq2d ⊒ ( π‘š = 0 β†’ ( ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
152 151 ralbidv ⊒ ( π‘š = 0 β†’ ( βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
153 152 rexsng ⊒ ( 0 ∈ ℝ β†’ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
154 143 153 ax-mp ⊒ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( 1 Β· ( π‘₯ β€˜ 𝑖 ) ) + ( 0 Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
155 142 154 sylnibr ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ Β¬ βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
156 2 raleqi ⊒ ( βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
157 156 rexbii ⊒ ( βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) )
158 biorf ⊒ ( Β¬ βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) β†’ ( βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) ) )
159 157 158 bitrid ⊒ ( Β¬ βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) β†’ ( βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) ) )
160 155 159 syl ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ ( βˆƒ π‘š ∈ { 0 } βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) ) )
161 125 160 bitr4id ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( βˆƒ π‘š ∈ ( { 0 } βˆͺ ( 0 (,] 1 ) ) βˆ€ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ↔ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
162 119 124 161 3bitrd ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ↔ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) )
163 32 115 162 3orbi123d ⊒ ( ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) ∧ 𝑝 ∈ 𝑃 ) β†’ ( ( 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ) ↔ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) ) )
164 163 rabbidva ⊒ ( ( 𝑁 ∈ β„• ∧ π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ) β†’ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ) } = { 𝑝 ∈ 𝑃 ∣ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) } )
165 164 mpoeq3dva ⊒ ( 𝑁 ∈ β„• β†’ ( π‘₯ ∈ 𝑃 , 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ π‘₯ ∈ ( 𝑝 ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( π‘₯ ( Itv β€˜ ( EEG β€˜ 𝑁 ) ) 𝑝 ) ) } ) = ( π‘₯ ∈ 𝑃 , 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) } ) )
166 4 165 eqtrd ⊒ ( 𝑁 ∈ β„• β†’ ( LineG β€˜ ( EEG β€˜ 𝑁 ) ) = ( π‘₯ ∈ 𝑃 , 𝑦 ∈ ( 𝑃 βˆ– { π‘₯ } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( βˆƒ π‘˜ ∈ ( 0 [,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑝 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘˜ ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘˜ Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ 𝑙 ∈ ( 0 [,) 1 ) βˆ€ 𝑖 ∈ 𝐼 ( π‘₯ β€˜ 𝑖 ) = ( ( ( 1 βˆ’ 𝑙 ) Β· ( 𝑝 β€˜ 𝑖 ) ) + ( 𝑙 Β· ( 𝑦 β€˜ 𝑖 ) ) ) ∨ βˆƒ π‘š ∈ ( 0 (,] 1 ) βˆ€ 𝑖 ∈ 𝐼 ( 𝑦 β€˜ 𝑖 ) = ( ( ( 1 βˆ’ π‘š ) Β· ( π‘₯ β€˜ 𝑖 ) ) + ( π‘š Β· ( 𝑝 β€˜ 𝑖 ) ) ) ) } ) )