Theorem rrxline

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023)

	Ref	Expression
Hypotheses	rrxlines.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrxlines.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrxlines.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	rrxlines.m	⊢ · = ( ·𝑠 ‘ 𝐸 )
	rrxlines.a	⊢ + = ( +g ‘ 𝐸 )
Assertion	rrxline	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rrxlines.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
2		rrxlines.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		rrxlines.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
4		rrxlines.m	⊢ · = ( ·𝑠 ‘ 𝐸 )
5		rrxlines.a	⊢ + = ( +g ‘ 𝐸 )
6	1 2 3 4 5	rrxlines	⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
7	6	oveqd	⊢ ( 𝐼 ∈ Fin → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) )
8	7	adantr	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) )
9		eqidd	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )
10		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
11	10	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 1 − 𝑡 ) · 𝑥 ) = ( ( 1 − 𝑡 ) · 𝑋 ) )
12		simpr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
13	12	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑡 · 𝑦 ) = ( 𝑡 · 𝑌 ) )
14	11 13	oveq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) )
15	14	eqeq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) ) )
16	15	rexbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) ) )
17	16	rabbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
18	17	adantl	⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
19		sneq	⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
20	19	difeq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑃 ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑋 } ) )
21	20	adantl	⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑥 = 𝑋 ) → ( 𝑃 ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑋 } ) )
22		simpr1	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ 𝑃 )
23		id	⊢ ( 𝑋 ≠ 𝑌 → 𝑋 ≠ 𝑌 )
24	23	necomd	⊢ ( 𝑋 ≠ 𝑌 → 𝑌 ≠ 𝑋 )
25	24	anim2i	⊢ ( ( 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝑃 ∧ 𝑌 ≠ 𝑋 ) )
26	25	3adant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝑃 ∧ 𝑌 ≠ 𝑋 ) )
27		eldifsn	⊢ ( 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ 𝑃 ∧ 𝑌 ≠ 𝑋 ) )
28	26 27	sylibr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
29	28	adantl	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
30	2	ovexi	⊢ 𝑃 ∈ V
31	30	rabex	⊢ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } ∈ V
32	31	a1i	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } ∈ V )
33	9 18 21 22 29 32	ovmpodx	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )
34	8 33	eqtrd	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑋 ) + ( 𝑡 · 𝑌 ) ) } )