Theorem rrx2linesl

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2, expressed by the slope S between the two points ("point-slope form"), sometimes also written as ( ( p2 ) - ( X2 ) ) = ( S x. ( ( p1 ) - ( X1 ) ) ) . (Contributed by AV, 22-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	⊢ 𝐼 = { 1 , 2 }
2		rrx2line.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		rrx2line.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		rrx2line.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		rrx2linesl.s	⊢ 𝑆 = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) )
6		fveq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
7	6	necon3i	⊢ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) → 𝑋 ≠ 𝑌 )
8	1 2 3 4	rrx2line	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )
9	7 8	syl3an3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )
10		reex	⊢ ℝ ∈ V
11		prex	⊢ { 1 , 2 } ∈ V
12	1 11	eqeltri	⊢ 𝐼 ∈ V
13	10 12	elmap	⊢ ( 𝑝 ∈ ( ℝ ↑m 𝐼 ) ↔ 𝑝 : 𝐼 ⟶ ℝ )
14		id	⊢ ( 𝑝 : 𝐼 ⟶ ℝ → 𝑝 : 𝐼 ⟶ ℝ )
15		1ex	⊢ 1 ∈ V
16	15	prid1	⊢ 1 ∈ { 1 , 2 }
17	16 1	eleqtrri	⊢ 1 ∈ 𝐼
18	17	a1i	⊢ ( 𝑝 : 𝐼 ⟶ ℝ → 1 ∈ 𝐼 )
19	14 18	ffvelcdmd	⊢ ( 𝑝 : 𝐼 ⟶ ℝ → ( 𝑝 ‘ 1 ) ∈ ℝ )
20	13 19	sylbi	⊢ ( 𝑝 ∈ ( ℝ ↑m 𝐼 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
21	20 3	eleq2s	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
22	21	adantl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
23	10 12	elmap	⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ ℝ )
24		id	⊢ ( 𝑋 : 𝐼 ⟶ ℝ → 𝑋 : 𝐼 ⟶ ℝ )
25	17	a1i	⊢ ( 𝑋 : 𝐼 ⟶ ℝ → 1 ∈ 𝐼 )
26	24 25	ffvelcdmd	⊢ ( 𝑋 : 𝐼 ⟶ ℝ → ( 𝑋 ‘ 1 ) ∈ ℝ )
27	23 26	sylbi	⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
28	27 3	eleq2s	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
29	28	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
30	29	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
31	10 12	elmap	⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) ↔ 𝑌 : 𝐼 ⟶ ℝ )
32		id	⊢ ( 𝑌 : 𝐼 ⟶ ℝ → 𝑌 : 𝐼 ⟶ ℝ )
33	17	a1i	⊢ ( 𝑌 : 𝐼 ⟶ ℝ → 1 ∈ 𝐼 )
34	32 33	ffvelcdmd	⊢ ( 𝑌 : 𝐼 ⟶ ℝ → ( 𝑌 ‘ 1 ) ∈ ℝ )
35	31 34	sylbi	⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
36	35 3	eleq2s	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
37	36	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
38	37	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
39		simpl3	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
40		2ex	⊢ 2 ∈ V
41	40	prid2	⊢ 2 ∈ { 1 , 2 }
42	41 1	eleqtrri	⊢ 2 ∈ 𝐼
43	42	a1i	⊢ ( 𝑝 : 𝐼 ⟶ ℝ → 2 ∈ 𝐼 )
44	14 43	ffvelcdmd	⊢ ( 𝑝 : 𝐼 ⟶ ℝ → ( 𝑝 ‘ 2 ) ∈ ℝ )
45	13 44	sylbi	⊢ ( 𝑝 ∈ ( ℝ ↑m 𝐼 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
46	45 3	eleq2s	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
47	46	adantl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
48	42	a1i	⊢ ( 𝑋 : 𝐼 ⟶ ℝ → 2 ∈ 𝐼 )
49	24 48	ffvelcdmd	⊢ ( 𝑋 : 𝐼 ⟶ ℝ → ( 𝑋 ‘ 2 ) ∈ ℝ )
50	23 49	sylbi	⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
51	50 3	eleq2s	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
52	51	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
53	52	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
54	3	eleq2i	⊢ ( 𝑌 ∈ 𝑃 ↔ 𝑌 ∈ ( ℝ ↑m 𝐼 ) )
55	54 31	bitri	⊢ ( 𝑌 ∈ 𝑃 ↔ 𝑌 : 𝐼 ⟶ ℝ )
56	42	a1i	⊢ ( 𝑌 : 𝐼 ⟶ ℝ → 2 ∈ 𝐼 )
57	32 56	ffvelcdmd	⊢ ( 𝑌 : 𝐼 ⟶ ℝ → ( 𝑌 ‘ 2 ) ∈ ℝ )
58	55 57	sylbi	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
59	58	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
60	59	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
61	22 30 38 39 47 53 60 5	affinecomb1	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) ) )
62	61	rabbidva	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 2 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) } )
63	9 62	eqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 2 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) } )