Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 syl5eq ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 syl5eq ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 ) ∧ 𝐶 ∈ ℝ ) → 𝐺 = ( 𝑋 𝐿 𝑌 ) )