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 ⊢ 𝐼 = { 1 , 2 }
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
line2x.x ⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
line2x.y ⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
Assertion line2x ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 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 line2x.x ⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
7 line2x.y ⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
8 5 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } )
9 1ex ⊢ 1 ∈ V
10 2ex ⊢ 2 ∈ V
11 9 10 pm3.2i ⊢ ( 1 ∈ V ∧ 2 ∈ V )
12 c0ex ⊢ 0 ∈ V
13 12 jctl ⊢ ( 𝑀 ∈ ℝ → ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) )
14 1ne2 ⊢ 1 ≠ 2
15 14 a1i ⊢ ( 𝑀 ∈ ℝ → 1 ≠ 2 )
16 fprg ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 0 , 𝑀 } )
17 0red ⊢ ( ( 1 ∈ V ∧ 2 ∈ V ) → 0 ∈ ℝ )
18 simpr ⊢ ( ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) → 𝑀 ∈ ℝ )
19 17 18 anim12i ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
20 19 3adant3 ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
21 prssi ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → { 0 , 𝑀 } ⊆ ℝ )
22 20 21 syl ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { 0 , 𝑀 } ⊆ ℝ )
23 16 22 fssd ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 0 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
24 11 13 15 23 mp3an2i ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
25 1 feq2i ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
26 24 25 sylibr ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
27 reex ⊢ ℝ ∈ V
28 prex ⊢ { 1 , 2 } ∈ V
29 1 28 eqeltri ⊢ 𝐼 ∈ V
30 27 29 elmap ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
31 26 30 sylibr ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
32 31 6 3 3eltr4g ⊢ ( 𝑀 ∈ ℝ → 𝑋 ∈ 𝑃 )
33 9 jctl ⊢ ( 𝑀 ∈ ℝ → ( 1 ∈ V ∧ 𝑀 ∈ ℝ ) )
34 fprg ⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 1 ∈ V ∧ 𝑀 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 1 , 𝑀 } )
35 11 33 15 34 mp3an2i ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ { 1 , 𝑀 } )
36 1re ⊢ 1 ∈ ℝ
37 prssi ⊢ ( ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → { 1 , 𝑀 } ⊆ ℝ )
38 36 37 mpan ⊢ ( 𝑀 ∈ ℝ → { 1 , 𝑀 } ⊆ ℝ )
39 35 38 fssd ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
40 1 feq2i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : { 1 , 2 } ⟶ ℝ )
41 39 40 sylibr ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ )
42 27 29 pm3.2i ⊢ ( ℝ ∈ V ∧ 𝐼 ∈ V )
43 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝐼 ∈ V ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ) )
44 42 43 mp1i ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } : 𝐼 ⟶ ℝ ) )
45 41 44 mpbird ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ∈ ( ℝ ↑m 𝐼 ) )
46 45 7 3 3eltr4g ⊢ ( 𝑀 ∈ ℝ → 𝑌 ∈ 𝑃 )
47 opex ⊢ ⟨ 1 , 0 ⟩ ∈ V
48 opex ⊢ ⟨ 2 , 𝑀 ⟩ ∈ V
49 47 48 pm3.2i ⊢ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V )
50 opex ⊢ ⟨ 1 , 1 ⟩ ∈ V
51 50 48 pm3.2i ⊢ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V )
52 49 51 pm3.2i ⊢ ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) )
53 14 orci ⊢ ( 1 ≠ 2 ∨ 0 ≠ 𝑀 )
54 9 12 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ↔ ( 1 ≠ 2 ∨ 0 ≠ 𝑀 ) )
55 53 54 mpbir ⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩
56 55 a1i ⊢ ( 𝑀 ∈ ℝ → ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ )
57 0ne1 ⊢ 0 ≠ 1
58 57 olci ⊢ ( 1 ≠ 1 ∨ 0 ≠ 1 )
59 9 12 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ↔ ( 1 ≠ 1 ∨ 0 ≠ 1 ) )
60 58 59 mpbir ⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩
61 56 60 jctil ⊢ ( 𝑀 ∈ ℝ → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) )
62 61 orcd ⊢ ( 𝑀 ∈ ℝ → ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ∨ ( ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ) )
63 prneimg ⊢ ( ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ∧ ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 𝑀 ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ∨ ( ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 1 , 1 ⟩ ∧ ⟨ 2 , 𝑀 ⟩ ≠ ⟨ 2 , 𝑀 ⟩ ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ) )
64 52 62 63 mpsyl ⊢ ( 𝑀 ∈ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ≠ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } )
65 64 6 7 3netr4g ⊢ ( 𝑀 ∈ ℝ → 𝑋 ≠ 𝑌 )
66 32 46 65 3jca ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
67 66 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
68 eqid ⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
69 eqid ⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
70 eqid ⊢ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
71 1 2 3 4 68 69 70 rrx2linest ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
72 67 71 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
73 8 72 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } ) )
74 rabbi ⊢ ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } )
75 7 fveq1i ⊢ ( 𝑌 ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 )
76 9 9 14 3pm3.2i ⊢ ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 )
77 fvpr1g ⊢ ( ( 1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
78 76 77 mp1i ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
79 75 78 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 1 ) = 1 )
80 6 fveq1i ⊢ ( 𝑋 ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 )
81 9 12 14 3pm3.2i ⊢ ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 )
82 fvpr1g ⊢ ( ( 1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
83 81 82 mp1i ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
84 80 83 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 1 ) = 0 )
85 79 84 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( 1 − 0 ) )
86 1m0e1 ⊢ ( 1 − 0 ) = 1
87 85 86 eqtrdi ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 1 )
88 87 oveq1d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( 1 · ( 𝑝 ‘ 2 ) ) )
89 7 fveq1i ⊢ ( 𝑌 ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 )
90 fvpr2g ⊢ ( ( 2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
91 10 14 90 mp3an13 ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
92 89 91 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 2 ) = 𝑀 )
93 6 fveq1i ⊢ ( 𝑋 ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 )
94 fvpr2g ⊢ ( ( 2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
95 10 14 94 mp3an13 ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 2 ) = 𝑀 )
96 93 95 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 2 ) = 𝑀 )
97 92 96 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( 𝑀 − 𝑀 ) )
98 recn ⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℂ )
99 98 subidd ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 𝑀 ) = 0 )
100 97 99 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 )
101 100 oveq1d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
102 9 9 15 77 mp3an12i ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 1 )
103 75 102 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 1 ) = 1 )
104 96 103 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) = ( 𝑀 · 1 ) )
105 ax-1rid ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 · 1 ) = 𝑀 )
106 104 105 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) = 𝑀 )
107 9 12 15 82 mp3an12i ⊢ ( 𝑀 ∈ ℝ → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ } ‘ 1 ) = 0 )
108 80 107 eqtrid ⊢ ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 1 ) = 0 )
109 108 92 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = ( 0 · 𝑀 ) )
110 98 mul02d ⊢ ( 𝑀 ∈ ℝ → ( 0 · 𝑀 ) = 0 )
111 109 110 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) = 0 )
112 106 111 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( 𝑀 − 0 ) )
113 98 subid1d ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 0 ) = 𝑀 )
114 112 113 eqtrd ⊢ ( 𝑀 ∈ ℝ → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = 𝑀 )
115 101 114 oveq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) )
116 88 115 eqeq12d ⊢ ( 𝑀 ∈ ℝ → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ) )
117 116 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ) )
118 1 3 rrx2pyel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℝ )
119 118 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 2 ) ∈ ℂ )
120 119 mullidd ⊢ ( 𝑝 ∈ 𝑃 → ( 1 · ( 𝑝 ‘ 2 ) ) = ( 𝑝 ‘ 2 ) )
121 1 3 rrx2pxel ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℝ )
122 121 recnd ⊢ ( 𝑝 ∈ 𝑃 → ( 𝑝 ‘ 1 ) ∈ ℂ )
123 122 mul02d ⊢ ( 𝑝 ∈ 𝑃 → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
124 123 oveq1d ⊢ ( 𝑝 ∈ 𝑃 → ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) = ( 0 + 𝑀 ) )
125 120 124 eqeq12d ⊢ ( 𝑝 ∈ 𝑃 → ( ( 1 · ( 𝑝 ‘ 2 ) ) = ( ( 0 · ( 𝑝 ‘ 1 ) ) + 𝑀 ) ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) )
126 117 125 sylan9bb ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) )
127 126 bibi2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ) )
128 127 ralbidva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ) )
129 98 addlidd ⊢ ( 𝑀 ∈ ℝ → ( 0 + 𝑀 ) = 𝑀 )
130 129 adantr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( 0 + 𝑀 ) = 𝑀 )
131 130 eqeq2d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
132 131 bibi2d ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
133 132 ralbidva ⊢ ( 𝑀 ∈ ℝ → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
134 133 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = ( 0 + 𝑀 ) ) ↔ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
135 1 2 3 4 5 6 7 line2xlem ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
136 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
137 136 adantr ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
138 137 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 0 · ( 𝑝 ‘ 1 ) ) )
139 123 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 · ( 𝑝 ‘ 1 ) ) = 0 )
140 138 139 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = 0 )
141 140 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 0 + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) )
142 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
143 142 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
144 143 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
145 144 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
146 119 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ‘ 2 ) ∈ ℂ )
147 145 146 mulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐵 · ( 𝑝 ‘ 2 ) ) ∈ ℂ )
148 147 addlidd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
149 141 148 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( 𝐵 · ( 𝑝 ‘ 2 ) ) )
150 149 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = 𝐶 ) )
151 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
152 151 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
153 152 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐶 ∈ ℂ )
154 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
155 154 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
156 155 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
157 156 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ∈ ℂ )
158 simp2r ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ≠ 0 )
159 158 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝐵 ≠ 0 )
160 153 157 146 159 divmuld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 2 ) ↔ ( 𝐵 · ( 𝑝 ‘ 2 ) ) = 𝐶 ) )
161 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → 𝑀 = ( 𝐶 / 𝐵 ) )
162 161 eqcomd ⊢ ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ( 𝐶 / 𝐵 ) = 𝑀 )
163 162 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝐶 / 𝐵 ) = 𝑀 )
164 163 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝐶 / 𝐵 ) = ( 𝑝 ‘ 2 ) ↔ 𝑀 = ( 𝑝 ‘ 2 ) ) )
165 150 160 164 3bitr2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ 𝑀 = ( 𝑝 ‘ 2 ) ) )
166 eqcom ⊢ ( 𝑀 = ( 𝑝 ‘ 2 ) ↔ ( 𝑝 ‘ 2 ) = 𝑀 )
167 165 166 bitrdi ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
168 167 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) )
169 168 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ) )
170 135 169 impbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
171 128 134 170 3bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
172 74 171 bitr3id ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) } ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )
173 73 172 bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐺 = ( 𝑋 𝐿 𝑌 ) ↔ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )