Theorem rrx2line

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023) (Proof shortened by AV, 13-Feb-2023)

	Ref	Expression
Hypotheses	rrx2line.i	⊢ 𝐼 = { 1 , 2 }
	rrx2line.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrx2line.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrx2line.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
Assertion	rrx2line	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	⊢ 𝐼 = { 1 , 2 }
2		rrx2line.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		rrx2line.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		rrx2line.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		prfi	⊢ { 1 , 2 } ∈ Fin
6	1 5	eqeltri	⊢ 𝐼 ∈ Fin
7	2 3 4	rrxlinec	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )
8	6 7	mpan	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } )
9	1	a1i	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝐼 = { 1 , 2 } )
10	9	raleqdv	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ { 1 , 2 } ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
11		1ex	⊢ 1 ∈ V
12		2ex	⊢ 2 ∈ V
13		fveq2	⊢ ( 𝑖 = 1 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 1 ) )
14		fveq2	⊢ ( 𝑖 = 1 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 1 ) )
15	14	oveq2d	⊢ ( 𝑖 = 1 → ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) )
16		fveq2	⊢ ( 𝑖 = 1 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 1 ) )
17	16	oveq2d	⊢ ( 𝑖 = 1 → ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑌 ‘ 1 ) ) )
18	15 17	oveq12d	⊢ ( 𝑖 = 1 → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) )
19	13 18	eqeq12d	⊢ ( 𝑖 = 1 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) )
20		fveq2	⊢ ( 𝑖 = 2 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 2 ) )
21		fveq2	⊢ ( 𝑖 = 2 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 2 ) )
22	21	oveq2d	⊢ ( 𝑖 = 2 → ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) )
23		fveq2	⊢ ( 𝑖 = 2 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 2 ) )
24	23	oveq2d	⊢ ( 𝑖 = 2 → ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑌 ‘ 2 ) ) )
25	22 24	oveq12d	⊢ ( 𝑖 = 2 → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) )
26	20 25	eqeq12d	⊢ ( 𝑖 = 2 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) )
27	11 12 19 26	ralpr	⊢ ( ∀ 𝑖 ∈ { 1 , 2 } ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) )
28	10 27	bitrdi	⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ) )
29	28	rexbidva	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ) )
30	29	rabbidva	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑌 ‘ 𝑖 ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )
31	8 30	eqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )