Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝑝 : 𝐼 ⟶ ℝ → ( 𝑝 ‘ 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 ffvelrnd ⊢ ( 𝑋 : 𝐼 ⟶ ℝ → ( 𝑋 ‘ 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 ffvelrnd ⊢ ( 𝑌 : 𝐼 ⟶ ℝ → ( 𝑌 ‘ 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 ffvelrnd ⊢ ( 𝑝 : 𝐼 ⟶ ℝ → ( 𝑝 ‘ 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 ffvelrnd ⊢ ( 𝑋 : 𝐼 ⟶ ℝ → ( 𝑋 ‘ 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 ffvelrnd ⊢ ( 𝑌 : 𝐼 ⟶ ℝ → ( 𝑌 ‘ 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 ) ) } )