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 ⊢ 𝐼 = ( 0 ..^ 2 )
rrx2line.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
rrx2line.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
rrx2line.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
rrx2linest.a ⊢ 𝐴 = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
rrx2linest.b ⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
rrx2linest.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
Assertion rrx2linest ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( ( 𝐵 · ( 𝑝 ‘ 0 ) ) + 𝐶 ) } )

Proof

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