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	⊢ 𝐼 = { 1 , 2 }
	rrx2line.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	rrx2line.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	rrx2line.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
Assertion	rrx2vlinest	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) } )

Proof

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