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 ‘ 𝑁 ) ) )