Theorem line2

Description: Example for a line G passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023)

	Ref	Expression
Hypotheses	line2.i	⊢ 𝐼 = { 1 , 2 }
	line2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	line2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	line2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	line2.g	⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
	line2.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ }
	line2.y	⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ }
Assertion	line2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐺 = ( 𝑋 𝐿 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		line2.i	⊢ 𝐼 = { 1 , 2 }
2		line2.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		line2.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		line2.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
5		line2.g	⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
6		line2.x	⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ }
7		line2.y	⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ }
8		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
9	8	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
10	1 3	rrx2pxel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℝ )
12	9 11	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℝ )
13	12	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
14		simpl2l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
15	1 3	rrx2pyel	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
16	15	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℝ )
17	14 16	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℝ )
18	17	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
19		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
20	19	recnd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
21	20	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
22	21	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
23		simp2r	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ≠ 0 )
24	23	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ≠ 0 )
25	13 18 22 24	divdird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) / 𝐵 ) ) )
26	15	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℂ )
27	26	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℂ )
28	27 22 24	divcan3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) / 𝐵 ) = ( 𝑝 ‘ 2 ) )
29	28	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( ( 𝐵 · ( 𝑝 ‘ 2 ) ) / 𝐵 ) ) = ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝑝 ‘ 2 ) ) )
30	25 29	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝑝 ‘ 2 ) ) )
31	30	eqeq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( 𝐶 / 𝐵 ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝑝 ‘ 2 ) ) = ( 𝐶 / 𝐵 ) ) )
32	12 14 24	redivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ∈ ℝ )
33	32	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ∈ ℂ )
34		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
35	19	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
36	34 35 23	redivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
37	36	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℂ )
38	37	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) ∈ ℂ )
39	33 27 38	addrsub	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝑝 ‘ 2 ) ) = ( 𝐶 / 𝐵 ) ↔ ( 𝑝 ‘ 2 ) = ( ( 𝐶 / 𝐵 ) − ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ) ) )
40		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℝ )
41	40 14 24	redivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
42	41	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) ∈ ℂ )
43	33 42	negsubdi2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) = ( ( 𝐶 / 𝐵 ) − ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ) )
44	33 42	negsubdid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) = ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) )
45	43 44	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) − ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ) = ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) )
46	45	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( ( 𝐶 / 𝐵 ) − ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) ) ↔ ( 𝑝 ‘ 2 ) = ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) ) )
47	31 39 46	3bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( 𝐶 / 𝐵 ) ↔ ( 𝑝 ‘ 2 ) = ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) ) )
48	12 17	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) ∈ ℝ )
49	48	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) ∈ ℂ )
50	34	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
51	50	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
52		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
53	52	anim1i	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
54	53	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
55	54	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
56		div11	⊢ ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( 𝐶 / 𝐵 ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
57	49 51 55 56	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) / 𝐵 ) = ( 𝐶 / 𝐵 ) ↔ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ) )
58	13 22 24	divnegd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( - ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) )
59	8	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
60	59	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ ℂ )
61	10	recnd	⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
62	61	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
63	60 62	mulneg1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( - 𝐴 · ( 𝑝 ‘ 1 ) ) = - ( 𝐴 · ( 𝑝 ‘ 1 ) ) )
64	63	eqcomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( - 𝐴 · ( 𝑝 ‘ 1 ) ) )
65	64	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( ( - 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) )
66	58 65	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( ( - 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) )
67		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
68	67	recnd	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℂ )
69	68	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → - 𝐴 ∈ ℂ )
70	69	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - 𝐴 ∈ ℂ )
71		div23	⊢ ( ( - 𝐴 ∈ ℂ ∧ ( 𝑝 ‘ 1 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( - 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( ( - 𝐴 / 𝐵 ) · ( 𝑝 ‘ 1 ) ) )
72	70 62 55 71	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( - 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( ( - 𝐴 / 𝐵 ) · ( 𝑝 ‘ 1 ) ) )
73	6	fveq1i	⊢ ( 𝑋 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 )
74		1ex	⊢ 1 ∈ V
75		c0ex	⊢ 0 ∈ V
76		1ne2	⊢ 1 ≠ 2
77	74 75 76	3pm3.2i	⊢ ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 )
78		fvpr1g	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 ) = 0 )
79	77 78	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 ) = 0 )
80	73 79	eqtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑋 ‘ 1 ) = 0 )
81	80	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) = 0 )
82	81	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑝 ‘ 1 ) − 0 ) )
83	62	subid1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) − 0 ) = ( 𝑝 ‘ 1 ) )
84	82 83	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) = ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) )
85	84	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( - 𝐴 / 𝐵 ) · ( 𝑝 ‘ 1 ) ) = ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
86	66 72 85	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) = ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
87	86	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) = ( ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) )
88	87	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( - ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) / 𝐵 ) + ( 𝐶 / 𝐵 ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ) )
89	47 57 88	3bitr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ) )
90		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
91	90	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
92		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
93	92	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
94		sub32	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 − 𝐴 ) − 𝐶 ) = ( ( 𝐶 − 𝐶 ) − 𝐴 ) )
95		subid	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 𝐶 ) = 0 )
96	95	3ad2ant1	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐶 ) = 0 )
97	96	oveq1d	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 − 𝐶 ) − 𝐴 ) = ( 0 − 𝐴 ) )
98		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
99	97 98	eqtr4di	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 − 𝐶 ) − 𝐴 ) = - 𝐴 )
100	94 99	eqtr2d	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - 𝐴 = ( ( 𝐶 − 𝐴 ) − 𝐶 ) )
101	91 93 91 100	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → - 𝐴 = ( ( 𝐶 − 𝐴 ) − 𝐶 ) )
102	101	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → - 𝐴 = ( ( 𝐶 − 𝐴 ) − 𝐶 ) )
103	102	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( - 𝐴 / 𝐵 ) = ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) )
104	103	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( - 𝐴 / 𝐵 ) = ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) )
105	104	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
106	105	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) = ( ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) )
107	106	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( ( ( - 𝐴 / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ) )
108	89 107	bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ) )
109	7	fveq1i	⊢ ( 𝑌 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 2 )
110		2ex	⊢ 2 ∈ V
111	110	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 2 ∈ V )
112		resubcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
113	112	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
114	113	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
115	114 35 23	redivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ )
116	76	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 1 ≠ 2 )
117	111 115 116	3jca	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 2 ∈ V ∧ ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ ∧ 1 ≠ 2 ) )
118	117	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 2 ∈ V ∧ ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ ∧ 1 ≠ 2 ) )
119		fvpr2g	⊢ ( ( 2 ∈ V ∧ ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 2 ) = ( ( 𝐶 − 𝐴 ) / 𝐵 ) )
120	118 119	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 2 ) = ( ( 𝐶 − 𝐴 ) / 𝐵 ) )
121	109 120	eqtrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) = ( ( 𝐶 − 𝐴 ) / 𝐵 ) )
122	6	fveq1i	⊢ ( 𝑋 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 2 )
123		fvpr2g	⊢ ( ( 2 ∈ V ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 2 ) = ( 𝐶 / 𝐵 ) )
124	110 36 116 123	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 2 ) = ( 𝐶 / 𝐵 ) )
125	122 124	eqtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑋 ‘ 2 ) = ( 𝐶 / 𝐵 ) )
126	125	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) = ( 𝐶 / 𝐵 ) )
127	121 126	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( ( 𝐶 − 𝐴 ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) )
128	34 8	resubcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
129	128	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
130		divsubdir	⊢ ( ( ( 𝐶 − 𝐴 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) = ( ( ( 𝐶 − 𝐴 ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) )
131	129 50 54 130	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) = ( ( ( 𝐶 − 𝐴 ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) )
132	131	eqcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐴 ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) = ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) )
133	132	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐶 − 𝐴 ) / 𝐵 ) − ( 𝐶 / 𝐵 ) ) = ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) )
134	127 133	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
135	134	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
136	135	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) )
137	136	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝐶 − 𝐴 ) − 𝐶 ) / 𝐵 ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ) )
138	7	fveq1i	⊢ ( 𝑌 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 1 )
139	74 74	fvpr1	⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 1 ) = 1 )
140	76 139	ax-mp	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 1 ) = 1
141	138 140	eqtri	⊢ ( 𝑌 ‘ 1 ) = 1
142	74 75	fvpr1	⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 ) = 0 )
143	76 142	ax-mp	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 ) = 0
144	73 143	eqtri	⊢ ( 𝑋 ‘ 1 ) = 0
145	141 144	oveq12i	⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( 1 − 0 )
146		1m0e1	⊢ ( 1 − 0 ) = 1
147	145 146	eqtri	⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 1
148	147	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 1 )
149	148	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / 1 ) )
150	110 115 116 119	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 2 ) = ( ( 𝐶 − 𝐴 ) / 𝐵 ) )
151	109 150	eqtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑌 ‘ 2 ) = ( ( 𝐶 − 𝐴 ) / 𝐵 ) )
152	115	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℂ )
153	151 152	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
154	125 37	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
155	153 154	subcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ∈ ℂ )
156	155	div1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / 1 ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
157	149 156	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) )
158	157	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) )
159	158 125	oveq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) )
160	159	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) )
161	160	eqcomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) )
162	161	eqeq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝐶 / 𝐵 ) ) ↔ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) ) )
163	108 137 162	3bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) ) )
164	163	rabbidva	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) } )
165	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
166	74 110	pm3.2i	⊢ ( 1 ∈ V ∧ 2 ∈ V )
167	36 75	jctil	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 0 ∈ V ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) )
168		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ { 0 , ( 𝐶 / 𝐵 ) } )
169	166 167 116 168	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ { 0 , ( 𝐶 / 𝐵 ) } )
170		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 0 ∈ ℝ )
171	170 36	prssd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { 0 , ( 𝐶 / 𝐵 ) } ⊆ ℝ )
172	169 171	fssd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ ℝ )
173	6	feq1i	⊢ ( 𝑋 : { 1 , 2 } ⟶ ℝ ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ ℝ )
174	172 173	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑋 : { 1 , 2 } ⟶ ℝ )
175		reex	⊢ ℝ ∈ V
176		prex	⊢ { 1 , 2 } ∈ V
177	175 176	elmap	⊢ ( 𝑋 ∈ ( ℝ ↑m { 1 , 2 } ) ↔ 𝑋 : { 1 , 2 } ⟶ ℝ )
178	174 177	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑋 ∈ ( ℝ ↑m { 1 , 2 } ) )
179	1	oveq2i	⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m { 1 , 2 } )
180	3 179	eqtri	⊢ 𝑃 = ( ℝ ↑m { 1 , 2 } )
181	178 180	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑋 ∈ 𝑃 )
182	115 74	jctil	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 1 ∈ V ∧ ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ ) )
183		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 1 ∈ V ∧ ( ( 𝐶 − 𝐴 ) / 𝐵 ) ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ { 1 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) } )
184	166 182 116 183	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ { 1 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) } )
185		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 1 ∈ ℝ )
186	185 115	prssd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { 1 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) } ⊆ ℝ )
187	184 186	fssd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ ℝ )
188	7	feq1i	⊢ ( 𝑌 : { 1 , 2 } ⟶ ℝ ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } : { 1 , 2 } ⟶ ℝ )
189	187 188	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑌 : { 1 , 2 } ⟶ ℝ )
190	175 176	elmap	⊢ ( 𝑌 ∈ ( ℝ ↑m { 1 , 2 } ) ↔ 𝑌 : { 1 , 2 } ⟶ ℝ )
191	189 190	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑌 ∈ ( ℝ ↑m { 1 , 2 } ) )
192	191 180	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝑌 ∈ 𝑃 )
193		0ne1	⊢ 0 ≠ 1
194	77 78	ax-mp	⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , ( 𝐶 / 𝐵 ) ⟩ } ‘ 1 ) = 0
195	73 194	eqtri	⊢ ( 𝑋 ‘ 1 ) = 0
196	74 74 76	3pm3.2i	⊢ ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 )
197		fvpr1g	⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 1 ) = 1 )
198	196 197	ax-mp	⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , ( ( 𝐶 − 𝐴 ) / 𝐵 ) ⟩ } ‘ 1 ) = 1
199	138 198	eqtri	⊢ ( 𝑌 ‘ 1 ) = 1
200	195 199	neeq12i	⊢ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ↔ 0 ≠ 1 )
201	193 200	mpbir	⊢ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 )
202	201	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
203		eqid	⊢ ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) )
204	1 2 3 4 203	rrx2linesl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) } )
205	181 192 202 204	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 2 ) = ( ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) / ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) · ( ( 𝑝 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ) + ( 𝑋 ‘ 2 ) ) } )
206	164 165 205	3eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐺 = ( 𝑋 𝐿 𝑌 ) )