Metamath Proof Explorer

Theorem eenglngeehlnm

Description: The line definition in the Tarski structure for the Euclidean geometry (see elntg ) corresponds to the definition of lines passing through two different points in a left module (see rrxlines ). (Contributed by AV, 16-Feb-2023)

Ref Expression
Assertion eenglngeehlnm ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( LineM ‘ ( 𝔼hil ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eengbas ⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
2 1 eqcomd ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( 𝔼 ‘ 𝑁 ) )
3 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
4 3 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ℝ ↑m ( 1 ... 𝑛 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
5 df-ee ⊢ 𝔼 = ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )
6 ovex ⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∈ V
7 4 5 6 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
8 2 7 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
9 2 ancli ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℕ ∧ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( 𝔼 ‘ 𝑁 ) ) )
10 9 8 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 ∈ ℕ ∧ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( 𝔼 ‘ 𝑁 ) ) ∧ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
11 difeq1 ⊢ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) = ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
12 11 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( 𝔼 ‘ 𝑁 ) ) ∧ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) = ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
13 10 12 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) = ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
14 8 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) → ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
15 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) ∧ 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
16 8 eleq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ↔ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
17 16 biimpcd ⊢ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) → ( 𝑁 ∈ ℕ → 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
18 17 adantr ⊢ ( ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) → ( 𝑁 ∈ ℕ → 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
19 18 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) ∧ 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
21 8 difeq1d ⊢ ( 𝑁 ∈ ℕ → ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) = ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
22 21 eleq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ↔ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) )
23 22 biimpd ⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) → 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) )
24 23 adantld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) → 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) )
25 24 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) → 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
26 25 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) ∧ 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) )
27 14 eleq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) → ( 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ↔ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
28 27 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) ∧ 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
29 eenglngeehlnmlem1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
30 eenglngeehlnmlem2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
31 29 30 impbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
32 15 20 26 28 31 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) ∧ 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) → ( ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
33 14 32 rabeqbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ) ) → { 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∣ ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) } = { 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } )
34 8 13 33 mpoeq123dva ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∣ ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) } ) = ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) , 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )
35 eqid ⊢ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( Base ‘ ( EEG ‘ 𝑁 ) )
36 eqid ⊢ ( 1 ... 𝑁 ) = ( 1 ... 𝑁 )
37 35 36 elntg2 ⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ ( EEG ‘ 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∣ ( ∃ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑧 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑧 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑣 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑣 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑣 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑤 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑤 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑤 · ( 𝑝 ‘ 𝑖 ) ) ) ) } ) )
38 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
39 eqid ⊢ ( 𝔼hil ‘ 𝑁 ) = ( 𝔼hil ‘ 𝑁 )
40 39 ehlval ⊢ ( 𝑁 ∈ ℕ0 → ( 𝔼hil ‘ 𝑁 ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
41 38 40 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝔼hil ‘ 𝑁 ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
42 41 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( LineM ‘ ( 𝔼hil ‘ 𝑁 ) ) = ( LineM ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) )
43 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
44 eqid ⊢ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) )
45 eqid ⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) )
46 eqid ⊢ ( LineM ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( LineM ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
47 44 45 46 rrxlinesc ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( LineM ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) , 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )
48 43 47 syl ⊢ ( 𝑁 ∈ ℕ → ( LineM ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) , 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )
49 42 48 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( LineM ‘ ( 𝔼hil ‘ 𝑁 ) ) = ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) , 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )
50 34 37 49 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( LineM ‘ ( 𝔼hil ‘ 𝑁 ) ) )