Metamath Proof Explorer

Theorem rrx2linest2

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in another "standard form" (usually with ( p1 ) = x and ( p2 ) = y ). (Contributed by AV, 23-Feb-2023)

Ref Expression
Hypotheses rrx2linest2.i ⊢ 𝐼 = { 1 , 2 }
rrx2linest2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
rrx2linest2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
rrx2linest2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
rrx2linest2.a ⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
rrx2linest2.b ⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
rrx2linest2.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
Assertion rrx2linest2 ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )

Proof

Step Hyp Ref Expression
1 rrx2linest2.i ⊢ 𝐼 = { 1 , 2 }
2 rrx2linest2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 rrx2linest2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 rrx2linest2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 rrx2linest2.a ⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
6 rrx2linest2.b ⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
7 rrx2linest2.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
8 eqid ⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
9 1 2 3 4 6 8 7 rrx2linest ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
10 eqcom ⊢ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
11 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
12 11 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
13 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
14 13 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
15 12 14 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
16 15 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℝ )
17 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
18 17 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
19 16 18 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
20 19 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
21 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
22 21 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
23 14 22 remulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
24 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
25 24 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
26 25 12 remulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
27 23 26 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
28 7 27 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐶 ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℝ )
30 29 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
31 22 25 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
32 6 31 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐵 ∈ ℝ )
33 32 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
34 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
35 34 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
36 33 35 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℝ )
37 36 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
38 20 30 37 addrsub ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) ↔ 𝐶 = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) ) )
39 eqcom ⊢ ( 𝐶 = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) ↔ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 )
40 14 12 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
41 5 40 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ ℝ )
42 41 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
43 42 18 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
44 43 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
45 44 37 addcomd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) )
46 12 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
47 46 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
48 14 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
49 48 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
50 47 49 negsubdi2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) )
51 5 50 eqtr4id ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 = - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
52 51 oveq1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
53 16 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
54 18 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
55 53 54 mulneg1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
56 52 55 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
57 56 oveq2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + ( 𝐴 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) )
58 37 20 negsubd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) + - ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) )
59 45 57 58 3eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) )
60 59 eqeq1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ) )
61 39 60 bitr4id ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 = ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) − ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
62 38 61 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
63 10 62 syl5bb ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
64 63 rabbidva ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → { 𝑝 ∈ 𝑃 ∣ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
65 9 64 eqtrd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )