Metamath Proof Explorer

Theorem rrx2vlinest

Description: The vertical 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 ‘ 𝐸 )
Assertion rrx2vlinest ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } )

Proof

Step Hyp Ref Expression
1 rrx2line.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 rrx2line.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 rrx2line.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 rrx2line.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 fveq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
6 5 necon3i ⊢ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) → 𝑋 ≠ 𝑌 )
7 6 adantl ⊢ ( ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 𝑋 ≠ 𝑌 )
8 1 2 3 4 rrx2line ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )
9 7 8 syl3an3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } )
10 oveq2 ⊢ ( ( 𝑌 ‘ 0 ) = ( 𝑋 ‘ 0 ) → ( 𝑡 · ( 𝑌 ‘ 0 ) ) = ( 𝑡 · ( 𝑋 ‘ 0 ) ) )
11 10 oveq2d ⊢ ( ( 𝑌 ‘ 0 ) = ( 𝑋 ‘ 0 ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
12 11 eqcoms ⊢ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
13 12 adantr ⊢ ( ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
15 14 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
16 15 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) )
17 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℝ )
18 17 recnd ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℂ )
19 18 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 ‘ 0 ) ∈ ℂ )
20 19 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 0 ) ∈ ℂ )
21 20 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑋 ‘ 0 ) ∈ ℂ )
22 recn ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
23 22 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
24 21 23 affineid ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑋 ‘ 0 ) ) ) = ( 𝑋 ‘ 0 ) )
25 16 24 eqtrd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) = ( 𝑋 ‘ 0 ) )
26 25 eqeq2d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ↔ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) )
27 26 anbi1d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ) )
28 27 rexbidva ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ) )
29 simpl ⊢ ( ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) → ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) )
30 29 a1i ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ ℝ ) → ( ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) → ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) )
31 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
32 31 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
33 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
34 33 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
35 34 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
36 32 35 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
37 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
38 37 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
39 38 34 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
40 39 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
41 37 recnd ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℂ )
42 41 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
43 33 recnd ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℂ )
44 43 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 ‘ 1 ) ∈ ℂ )
45 simpr ⊢ ( ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
46 45 necomd ⊢ ( ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) )
47 46 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) )
48 42 44 47 subne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 )
49 48 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 )
50 36 40 49 redivcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ∈ ℝ )
51 50 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ∈ ℝ )
52 simpr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) )
53 43 mullidd ⊢ ( 𝑋 ∈ 𝑃 → ( 1 · ( 𝑋 ‘ 1 ) ) = ( 𝑋 ‘ 1 ) )
54 53 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 1 · ( 𝑋 ‘ 1 ) ) = ( 𝑋 ‘ 1 ) )
55 54 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 1 · ( 𝑋 ‘ 1 ) ) = ( 𝑋 ‘ 1 ) )
56 36 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℂ )
57 41 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
58 43 adantr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℂ )
59 57 58 subcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℂ )
60 59 3adant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℂ )
61 60 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℂ )
62 56 61 49 divcan1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) )
63 55 62 oveq12d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 1 · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) = ( ( 𝑋 ‘ 1 ) + ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
64 44 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℂ )
65 31 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
66 65 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
67 64 66 pncan3d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) + ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( 𝑝 ‘ 1 ) )
68 63 67 eqtr2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) = ( ( 1 · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) )
69 68 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( 𝑝 ‘ 1 ) = ( ( 1 · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) )
70 1cnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 1 ∈ ℂ )
71 50 recnd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ∈ ℂ )
72 42 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
73 70 71 64 72 submuladdmuld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) = ( ( 1 · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) )
74 73 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) = ( ( 1 · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) )
75 69 74 eqtr4d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( 𝑝 ‘ 1 ) = ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) )
76 52 75 jca ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) → ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) ) )
77 oveq2 ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( 1 − 𝑡 ) = ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) )
78 77 oveq1d ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) = ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) )
79 oveq1 ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( 𝑡 · ( 𝑌 ‘ 1 ) ) = ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) )
80 78 79 oveq12d ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) = ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) )
81 80 eqeq2d ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) ) )
82 81 anbi2d ⊢ ( 𝑡 = ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) → ( ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) ) · ( 𝑋 ‘ 1 ) ) + ( ( ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
83 30 51 76 82 rspceb2dv ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) )
84 28 83 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) ) )
85 84 rabbidva ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ ( ( 𝑝 ‘ 0 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 0 ) ) + ( 𝑡 · ( 𝑌 ‘ 0 ) ) ) ∧ ( 𝑝 ‘ 1 ) = ( ( ( 1 − 𝑡 ) · ( 𝑋 ‘ 1 ) ) + ( 𝑡 · ( 𝑌 ‘ 1 ) ) ) ) } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } )
86 9 85 eqtrd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 0 ) = ( 𝑌 ‘ 0 ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 0 ) = ( 𝑋 ‘ 0 ) } )