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 
|- I = { 1 , 2 }
line2.e 
|- E = ( RR^ ` I )
line2.p 
|- P = ( RR ^m I )
line2.l 
|- L = ( LineM ` E )
line2.g 
|- G = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C }
line2x.x 
|- X = { <. 1 , 0 >. , <. 2 , M >. }
line2x.y 
|- Y = { <. 1 , 1 >. , <. 2 , M >. }
Assertion line2x 
|- ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( G = ( X L Y ) <-> ( A = 0 /\ M = ( C / B ) ) ) )

Proof

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