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 ( ( p1 ) - ( X1 ) ) = ( S x. ( ( p0 ) - ( X0 ) ) ) . (Contributed by AV, 22-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	⊢ 𝐼 = ( 0 ..^ 2 )
2		rrx2line.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		rrx2line.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		rrx2line.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		rrx2linesl.s	⊢ 𝑆 = ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) )
6		fveq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) )
7	6	necon3i	⊢ ( ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) → 𝑋 ≠ 𝑌 )
8	1 2 3 4	rrx2line	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )
9	7 8	syl3an3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )
10	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
11	10	adantl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 0 ) ∈ ℝ )
12	1 3	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℝ )
13	12	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
14	13	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
15	1 3	rrx2pxel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 0 ) ∈ ℝ )
16	15	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
17	16	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
18		simpl3	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) )
19	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
20	19	adantl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
21	1 3	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
22	21	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
23	22	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
24	1 3	rrx2pyel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
25	24	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
26	25	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
27	11 14 17 18 20 23 26 5	affinecomb1	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ) + ( 𝑋 ‘ 1 ) ) ) )
28	27	rabbidva	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ) + ( 𝑋 ‘ 1 ) ) } )
29	9 28	eqtrd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( ( 𝑆 · ( ( 𝑝 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ) + ( 𝑋 ‘ 1 ) ) } )