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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑌 ‘ 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 syl5eq ( 𝑀 ∈ ℝ → ( 𝑋 ‘ 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 mulid2d ( 𝑝𝑃 → ( 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 addid2d ( 𝑀 ∈ ℝ → ( 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 addid2d ( ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )