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 ⊢ 𝐼 = ( 0 ..^ 2 )
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 }
line2.x ⊢ 𝑋 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩
line2.y ⊢ 𝑌 = ⟨“ 1 ( ( 𝐶 − 𝐴 ) / 𝐵 ) ”⟩
Assertion line2 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐺 = ( 𝑋 𝐿 𝑌 ) )

Proof

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