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	eqtrid	⊢ ( ( 𝑋 ‘ 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 ) ) + 𝐶 ) } )