Theorem rrxlinesc

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension, expressed by their coordinates. (Contributed by AV, 13-Feb-2023)

	Ref	Expression
Hypotheses	rrxlinesc.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrxlinesc.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrxlinesc.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
Assertion	rrxlinesc	⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		rrxlinesc.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
2		rrxlinesc.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		rrxlinesc.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
4		eqid	⊢ ( ·𝑠 ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐸 )
5		eqid	⊢ ( +g ‘ 𝐸 ) = ( +g ‘ 𝐸 )
6	1 2 3 4 5	rrxlines	⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑥 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑦 ) ) } ) )
7		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8		simpll1	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝐼 ∈ Fin )
9		1red	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℝ )
10		simpr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
11	9 10	resubcld	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
12		id	⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
13	12 1 7	rrxbasefi	⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) )
14	2 13	eqtr4id	⊢ ( 𝐼 ∈ Fin → 𝑃 = ( Base ‘ 𝐸 ) )
15	14	eleq2d	⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ 𝑃 ↔ 𝑥 ∈ ( Base ‘ 𝐸 ) ) )
16	15	biimpa	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
17	16	3adant3	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
18	17	ad2antrr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
19		eldifi	⊢ ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ 𝑃 )
20	14	eleq2d	⊢ ( 𝐼 ∈ Fin → ( 𝑦 ∈ 𝑃 ↔ 𝑦 ∈ ( Base ‘ 𝐸 ) ) )
21	19 20	imbitrid	⊢ ( 𝐼 ∈ Fin → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ ( Base ‘ 𝐸 ) ) )
22	21	a1d	⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ 𝑃 → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) )
23	22	3imp	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑦 ∈ ( Base ‘ 𝐸 ) )
24	23	ad2antrr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑦 ∈ ( Base ‘ 𝐸 ) )
25	14	3ad2ant1	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑃 = ( Base ‘ 𝐸 ) )
26	25	eleq2d	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( Base ‘ 𝐸 ) ) )
27	26	biimpa	⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
28	27	adantr	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑝 ∈ ( Base ‘ 𝐸 ) )
29	1 7 4 8 11 18 24 28 5 10	rrxplusgvscavalb	⊢ ( ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑥 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑦 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
30	29	rexbidva	⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑥 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑦 ) ) ↔ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
31	30	rabbidva	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑥 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑦 ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } )
32	31	mpoeq3dva	⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) ( ·𝑠 ‘ 𝐸 ) 𝑥 ) ( +g ‘ 𝐸 ) ( 𝑡 ( ·𝑠 ‘ 𝐸 ) 𝑦 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )
33	6 32	eqtrd	⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) } ) )