Metamath Proof Explorer

Theorem line2x

Description: Example for a horizontal 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 ) ) ) = 𝐶 }
line2x.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
line2x.y ⊢ 𝑌 = ⟨“ 1 𝑀 ”⟩
Assertion line2x ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 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 line2x.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
7 line2x.y ⊢ 𝑌 = ⟨“ 1 𝑀 ”⟩
8 5 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } )
9 s2len ⊢ ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ ) = 2
10 9 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ )
11 10 a1i ⊢ ( 𝑀 ∈ ℝ → 2 = ( ♯ ‘ ⟨“ 0 𝑀 ”⟩ ) )
12 0red ⊢ ( 𝑀 ∈ ℝ → 0 ∈ ℝ )
13 id ⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℝ )
14 12 13 s2cld ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ ∈ Word ℝ )
15 11 14 wrdfd ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
16 1 feq2i ⊢ ( ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ ↔ ⟨“ 0 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
17 15 16 sylibr ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ )
18 reex ⊢ ℝ ∈ V
19 1 ovexi ⊢ 𝐼 ∈ V
20 18 19 elmap ⊢ ( ⟨“ 0 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 0 𝑀 ”⟩ : 𝐼 ⟶ ℝ )
21 17 20 sylibr ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) )
22 21 6 3 3eltr4g ⊢ ( 𝑀 ∈ ℝ → 𝑋 ∈ 𝑃 )
23 s2len ⊢ ( ♯ ‘ ⟨“ 1 𝑀 ”⟩ ) = 2
24 23 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ 1 𝑀 ”⟩ )
25 24 a1i ⊢ ( 𝑀 ∈ ℝ → 2 = ( ♯ ‘ ⟨“ 1 𝑀 ”⟩ ) )
26 1re ⊢ 1 ∈ ℝ
27 26 a1i ⊢ ( 𝑀 ∈ ℝ → 1 ∈ ℝ )
28 27 13 s2cld ⊢ ( 𝑀 ∈ ℝ → ⟨“ 1 𝑀 ”⟩ ∈ Word ℝ )
29 25 28 wrdfd ⊢ ( 𝑀 ∈ ℝ → ⟨“ 1 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
30 1 feq2i ⊢ ( ⟨“ 1 𝑀 ”⟩ : 𝐼 ⟶ ℝ ↔ ⟨“ 1 𝑀 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ )
31 29 30 sylibr ⊢ ( 𝑀 ∈ ℝ → ⟨“ 1 𝑀 ”⟩ : 𝐼 ⟶ ℝ )
32 18 19 pm3.2i ⊢ ( ℝ ∈ V ∧ 𝐼 ∈ V )
33 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝐼 ∈ V ) → ( ⟨“ 1 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 1 𝑀 ”⟩ : 𝐼 ⟶ ℝ ) )
34 32 33 mp1i ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 1 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) ↔ ⟨“ 1 𝑀 ”⟩ : 𝐼 ⟶ ℝ ) )
35 31 34 mpbird ⊢ ( 𝑀 ∈ ℝ → ⟨“ 1 𝑀 ”⟩ ∈ ( ℝ ↑m 𝐼 ) )
36 35 7 3 3eltr4g ⊢ ( 𝑀 ∈ ℝ → 𝑌 ∈ 𝑃 )
37 0ne1 ⊢ 0 ≠ 1
38 37 a1i ⊢ ( 𝑀 ∈ ℝ → 0 ≠ 1 )
39 0red ⊢ ( ( 𝑀 ∈ ℝ ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → 0 ∈ ℝ )
40 simpl ⊢ ( ( 𝑀 ∈ ℝ ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → 𝑀 ∈ ℝ )
41 40 26 jctil ⊢ ( ( 𝑀 ∈ ℝ ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
42 simpr ⊢ ( ( 𝑀 ∈ ℝ ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ )
43 s2eq2seq ⊢ ( ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) → ( ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ↔ ( 0 = 1 ∧ 𝑀 = 𝑀 ) ) )
44 43 simprbda ⊢ ( ( ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → 0 = 1 )
45 39 40 41 42 44 syl1111anc ⊢ ( ( 𝑀 ∈ ℝ ∧ ⟨“ 0 𝑀 ”⟩ = ⟨“ 1 𝑀 ”⟩ ) → 0 = 1 )
46 38 45 mteqand ⊢ ( 𝑀 ∈ ℝ → ⟨“ 0 𝑀 ”⟩ ≠ ⟨“ 1 𝑀 ”⟩ )
47 46 6 7 3netr4g ⊢ ( 𝑀 ∈ ℝ → 𝑋 ≠ 𝑌 )
48 22 36 47 3jca ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
49 48 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
50 eqid ⊢ ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
51 eqid ⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
52 eqid ⊢ ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
53 1 2 3 4 50 51 52 rrx2linest ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) } )
54 49 53 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) } )
55 8 54 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) } ) )
56 rabbi ⊢ ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) } )
57 7 fveq1i ⊢ ( 𝑌 ‘ 0 ) = ( ⟨“ 1 𝑀 ”⟩ ‘ 0 )
58 s2fv0 ⊢ ( 1 ∈ ℝ → ( ⟨“ 1 𝑀 ”⟩ ‘ 0 ) = 1 )
59 26 58 mp1i ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 1 𝑀 ”⟩ ‘ 0 ) = 1 )
60 57 59 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 0 ) = 1 )
61 6 fveq1i ⊢ ( 𝑋 ‘ 0 ) = ( ⟨“ 0 𝑀 ”⟩ ‘ 0 )
62 0re ⊢ 0 ∈ ℝ
63 s2fv0 ⊢ ( 0 ∈ ℝ → ( ⟨“ 0 𝑀 ”⟩ ‘ 0 ) = 0 )
64 62 63 mp1i ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 0 𝑀 ”⟩ ‘ 0 ) = 0 )
65 61 64 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 0 ) = 0 )
66 60 65 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = ( 1 − 0 ) )
67 1m0e1 ⊢ ( 1 − 0 ) = 1
68 66 67 eqtrdi ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = 1 )
69 68 oveq1d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( 1 · ( 𝑝 ‘ 1 ) ) )
70 7 fveq1i ⊢ ( 𝑌 ‘ 1 ) = ( ⟨“ 1 𝑀 ”⟩ ‘ 1 )
71 s2fv1 ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 1 𝑀 ”⟩ ‘ 1 ) = 𝑀 )
72 70 71 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 1 ) = 𝑀 )
73 6 fveq1i ⊢ ( 𝑋 ‘ 1 ) = ( ⟨“ 0 𝑀 ”⟩ ‘ 1 )
74 s2fv1 ⊢ ( 𝑀 ∈ ℝ → ( ⟨“ 0 𝑀 ”⟩ ‘ 1 ) = 𝑀 )
75 73 74 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 1 ) = 𝑀 )
76 72 75 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( 𝑀 − 𝑀 ) )
77 recn ⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℂ )
78 77 subidd ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 𝑀 ) = 0 )
79 76 78 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 0 )
80 79 oveq1d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) = ( 0 · ( 𝑝 ‘ 0 ) ) )
81 75 60 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) = ( 𝑀 · 1 ) )
82 ax-1rid ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 · 1 ) = 𝑀 )
83 81 82 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) = 𝑀 )
84 65 72 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) = ( 0 · 𝑀 ) )
85 77 mul02d ⊢ ( 𝑀 ∈ ℝ → ( 0 · 𝑀 ) = 0 )
86 84 85 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) = 0 )
87 83 86 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = ( 𝑀 − 0 ) )
88 77 subid1d ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 0 ) = 𝑀 )
89 87 88 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = 𝑀 )
90 80 89 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) = ( ( 0 · ( 𝑝 ‘ 0 ) ) + 𝑀 ) )
91 69 90 eqeq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 1 ) ) = ( ( 0 · ( 𝑝 ‘ 0 ) ) + 𝑀 ) ) )
92 91 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 1 ) ) = ( ( 0 · ( 𝑝 ‘ 0 ) ) + 𝑀 ) ) )
93 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
94 93 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
95 94 mullidd ⊢ ( 𝑝 ∈ 𝑃 → ( 1 · ( 𝑝 ‘ 1 ) ) = ( 𝑝 ‘ 1 ) )
96 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℝ )
97 96 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 0 ) ∈ ℂ )
98 97 mul02d ⊢ ( 𝑝 ∈ 𝑃 → ( 0 · ( 𝑝 ‘ 0 ) ) = 0 )
99 98 oveq1d ⊢ ( 𝑝 ∈ 𝑃 → ( ( 0 · ( 𝑝 ‘ 0 ) ) + 𝑀 ) = ( 0 + 𝑀 ) )
100 95 99 eqeq12d ⊢ ( 𝑝 ∈ 𝑃 → ( ( 1 · ( 𝑝 ‘ 1 ) ) = ( ( 0 · ( 𝑝 ‘ 0 ) ) + 𝑀 ) ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) )
101 92 100 sylan9bb ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) )
102 101 bibi2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) ) )
103 102 ralbidva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) ) )
104 77 addlidd ⊢ ( 𝑀 ∈ ℝ → ( 0 + 𝑀 ) = 𝑀 )
105 104 adantr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( 0 + 𝑀 ) = 𝑀 )
106 105 eqeq2d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
107 106 bibi2d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
108 107 ralbidva ⊢ ( 𝑀 ∈ ℝ → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
109 108 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
110 1 2 3 4 5 6 7 line2xlem ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
111 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 0 · ( 𝑝 ‘ 0 ) ) )
112 111 adantr ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 0 · ( 𝑝 ‘ 0 ) ) )
113 112 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 0 · ( 𝑝 ‘ 0 ) ) )
114 98 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 · ( 𝑝 ‘ 0 ) ) = 0 )
115 113 114 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = 0 )
116 115 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( 0 + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) )
117 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
118 117 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
119 118 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
120 119 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
121 94 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 1 ) ∈ ℂ )
122 120 121 mulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 1 ) ) ∈ ℂ )
123 122 addlidd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 1 ) ) )
124 116 123 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 1 ) ) )
125 124 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝐵 · ( 𝑝 ‘ 1 ) ) = 𝐶 ) )
126 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
127 126 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
128 127 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
129 simp2r ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ≠ 0 )
130 129 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ≠ 0 )
131 128 120 121 130 divmuld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 1 ) ↔ ( 𝐵 · ( 𝑝 ‘ 1 ) ) = 𝐶 ) )
132 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → 𝑀 = ( 𝐶 / 𝐵 ) )
133 132 eqcomd ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐶 / 𝐵 ) = 𝑀 )
134 133 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) = 𝑀 )
135 134 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 1 ) ↔ 𝑀 = ( 𝑝 ‘ 1 ) ) )
136 125 131 135 3bitr2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ 𝑀 = ( 𝑝 ‘ 1 ) ) )
137 eqcom ⊢ ( 𝑀 = ( 𝑝 ‘ 1 ) ↔ ( 𝑝 ‘ 1 ) = 𝑀 )
138 136 137 bitrdi ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
139 138 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
140 139 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
141 110 140 impbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
142 103 109 141 3bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
143 56 142 bitr3id ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) } ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
144 55 143 bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )