Metamath Proof Explorer

Theorem rrx2linest

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in "standard form". (Contributed by AV, 2-Feb-2023)

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

Proof

Step Hyp Ref Expression
1 rrx2line.i ⊢ 𝐼 = { 1 , 2 }
2 rrx2line.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 rrx2line.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 rrx2line.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 rrx2linest.a ⊢ 𝐴 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
6 rrx2linest.b ⊢ 𝐵 = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
7 rrx2linest.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
8 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → 𝑋 ∈ 𝑃 )
9 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → 𝑌 ∈ 𝑃 )
10 simpr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
11 simpr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
12 11 anim1i ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
13 1 raleqi ⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
14 1ex ⊢ 1 ∈ V
15 2ex ⊢ 2 ∈ V
16 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 1 ) )
17 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 1 ) )
18 16 17 eqeq12d ⊢ ( 𝑖 = 1 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
19 fveq2 ⊢ ( 𝑖 = 2 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 2 ) )
20 fveq2 ⊢ ( 𝑖 = 2 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 2 ) )
21 19 20 eqeq12d ⊢ ( 𝑖 = 2 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
22 14 15 18 21 ralpr ⊢ ( ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
23 13 22 bitri ⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
24 12 23 sylibr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
25 elmapfn ⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 Fn 𝐼 )
26 25 3 eleq2s ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 Fn 𝐼 )
27 elmapfn ⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → 𝑌 Fn 𝐼 )
28 27 3 eleq2s ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 Fn 𝐼 )
29 26 28 anim12i ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) )
30 29 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) )
31 eqfnfv ⊢ ( ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) )
32 30 31 syl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) )
33 24 32 mpbird ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → 𝑋 = 𝑌 )
34 33 ex ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) → 𝑋 = 𝑌 ) )
35 34 necon3d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
36 35 ex ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( 𝑋 ≠ 𝑌 → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
37 36 com23 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≠ 𝑌 → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
38 37 3impia ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
39 38 imp ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) )
40 1 2 3 4 rrx2vlinest ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } )
41 8 9 10 39 40 syl112anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } )
42 ancom ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) )
43 simplr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
44 simpr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
45 simpll ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
46 5 oveq1i ⊢ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) )
47 46 a1i ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) )
48 oveq2 ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) )
49 48 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) )
50 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
51 50 recnd ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℂ )
52 51 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
53 52 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
54 53 subidd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) = 0 )
55 49 54 eqtrd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 0 )
56 55 oveq1d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( 0 · ( 𝑝 ‘ 2 ) ) )
57 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
58 57 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℂ )
59 58 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑝 ‘ 2 ) ∈ ℂ )
60 59 mul02d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 0 · ( 𝑝 ‘ 2 ) ) = 0 )
61 47 56 60 3eqtrd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝐴 · ( 𝑝 ‘ 2 ) ) = 0 )
62 6 oveq1i ⊢ ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) )
63 62 a1i ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) )
64 oveq1 ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
65 64 oveq2d ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
66 7 65 syl5eq ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
67 66 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
68 63 67 oveq12d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
69 61 68 eqeq12d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
70 43 44 45 69 syl21anc ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ↔ 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
71 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
72 71 recnd ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℂ )
73 72 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
74 52 73 mulcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) )
75 74 oveq2d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ) )
76 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
77 76 recnd ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℂ )
78 77 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
79 78 73 52 subdird ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ) )
80 75 79 eqtr4d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) )
81 80 ad2antlr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) )
82 81 oveq2d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) )
83 82 eqeq2d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) ) )
84 eqcom ⊢ ( 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) = 0 )
85 84 a1i ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) = 0 ) )
86 73 ad2antlr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
87 78 ad2antlr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
88 86 87 subcld ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
89 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
90 89 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
91 90 adantl ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
92 88 91 mulcld ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
93 87 86 subcld ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℂ )
94 52 ad2antlr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
95 93 94 mulcld ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ∈ ℂ )
96 addeq0 ⊢ ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) ∈ ℂ ∧ ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ∈ ℂ ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) = 0 ↔ ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) )
97 92 95 96 syl2anc ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) = 0 ↔ ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) )
98 93 94 mulneg1d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) = - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) )
99 87 86 negsubdi2d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
100 99 oveq1d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) )
101 98 100 eqtr3d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) )
102 101 eqeq2d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ↔ ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) )
103 necom ⊢ ( ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ↔ ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) )
104 39 42 103 3imtr3i ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) )
105 104 adantr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) )
106 86 87 105 subne0d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 )
107 91 94 88 106 mulcand ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ↔ ( 𝑝 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
108 102 107 bitrd ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = - ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ↔ ( 𝑝 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
109 85 97 108 3bitrd ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
110 83 109 bitrd ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑌 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
111 simpl ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
112 111 eqcomd ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑌 ‘ 1 ) = ( 𝑋 ‘ 1 ) )
113 112 adantr ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) = ( 𝑋 ‘ 1 ) )
114 113 eqeq2d ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) = ( 𝑌 ‘ 1 ) ↔ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) ) )
115 70 110 114 3bitrrd ⊢ ( ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) )
116 115 rabbidva ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
117 42 116 sylbi ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
118 41 117 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
119 1 2 3 4 rrx2line ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )
120 119 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } )
121 df-ne ⊢ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ↔ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
122 89 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
123 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
124 123 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
125 124 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
126 50 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
127 126 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
128 simpr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
129 57 ad2antlr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
130 76 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
131 130 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
132 71 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
133 132 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
134 122 125 127 128 129 131 133 affinecomb2 ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
135 5 eqcomi ⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 𝐴
136 135 oveq1i ⊢ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( 𝐴 · ( 𝑝 ‘ 2 ) )
137 6 eqcomi ⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 𝐵
138 137 oveq1i ⊢ ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · ( 𝑝 ‘ 1 ) )
139 7 eqcomi ⊢ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = 𝐶
140 138 139 oveq12i ⊢ ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 )
141 136 140 eqeq12i ⊢ ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) )
142 134 141 bitrdi ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) )
143 142 expcom ⊢ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) → ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) ) )
144 121 143 sylbir ⊢ ( ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) ) )
145 144 expd ⊢ ( ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑝 ∈ 𝑃 → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) ) ) )
146 145 impcom ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑝 ∈ 𝑃 → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) ) )
147 146 imp ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) ) )
148 147 rabbidva ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ∧ ( 𝑝 ‘ 2 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 2 ) ) + ( 𝑡 · ( 𝑌 ‘ 2 ) ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
149 120 148 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )
150 118 149 pm2.61dan ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 2 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 1 ) ) + 𝐶 ) } )