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 = ( 0 ..^ 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C }
line2x.x 
|- X = <" 0 M ">
line2x.y 
|- Y = <" 1 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 = ( 0 ..^ 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C }
6 line2x.x 
 |-  X = <" 0 M ">
7 line2x.y 
 |-  Y = <" 1 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } )
9 s2len 
 |-  ( # ` <" 0 M "> ) = 2
10 9 eqcomi 
 |-  2 = ( # ` <" 0 M "> )
11 10 a1i 
 |-  ( M e. RR -> 2 = ( # ` <" 0 M "> ) )
12 0red 
 |-  ( M e. RR -> 0 e. RR )
13 id 
 |-  ( M e. RR -> M e. RR )
14 12 13 s2cld 
 |-  ( M e. RR -> <" 0 M "> e. Word RR )
15 11 14 wrdfd 
 |-  ( M e. RR -> <" 0 M "> : ( 0 ..^ 2 ) --> RR )
16 1 feq2i 
 |-  ( <" 0 M "> : I --> RR <-> <" 0 M "> : ( 0 ..^ 2 ) --> RR )
17 15 16 sylibr 
 |-  ( M e. RR -> <" 0 M "> : I --> RR )
18 reex 
 |-  RR e. _V
19 1 ovexi 
 |-  I e. _V
20 18 19 elmap 
 |-  ( <" 0 M "> e. ( RR ^m I ) <-> <" 0 M "> : I --> RR )
21 17 20 sylibr 
 |-  ( M e. RR -> <" 0 M "> e. ( RR ^m I ) )
22 21 6 3 3eltr4g 
 |-  ( M e. RR -> X e. P )
23 s2len 
 |-  ( # ` <" 1 M "> ) = 2
24 23 eqcomi 
 |-  2 = ( # ` <" 1 M "> )
25 24 a1i 
 |-  ( M e. RR -> 2 = ( # ` <" 1 M "> ) )
26 1re 
 |-  1 e. RR
27 26 a1i 
 |-  ( M e. RR -> 1 e. RR )
28 27 13 s2cld 
 |-  ( M e. RR -> <" 1 M "> e. Word RR )
29 25 28 wrdfd 
 |-  ( M e. RR -> <" 1 M "> : ( 0 ..^ 2 ) --> RR )
30 1 feq2i 
 |-  ( <" 1 M "> : I --> RR <-> <" 1 M "> : ( 0 ..^ 2 ) --> RR )
31 29 30 sylibr 
 |-  ( M e. RR -> <" 1 M "> : I --> RR )
32 18 19 pm3.2i 
 |-  ( RR e. _V /\ I e. _V )
33 elmapg 
 |-  ( ( RR e. _V /\ I e. _V ) -> ( <" 1 M "> e. ( RR ^m I ) <-> <" 1 M "> : I --> RR ) )
34 32 33 mp1i 
 |-  ( M e. RR -> ( <" 1 M "> e. ( RR ^m I ) <-> <" 1 M "> : I --> RR ) )
35 31 34 mpbird 
 |-  ( M e. RR -> <" 1 M "> e. ( RR ^m I ) )
36 35 7 3 3eltr4g 
 |-  ( M e. RR -> Y e. P )
37 0ne1 
 |-  0 =/= 1
38 37 a1i 
 |-  ( M e. RR -> 0 =/= 1 )
39 0red 
 |-  ( ( M e. RR /\ <" 0 M "> = <" 1 M "> ) -> 0 e. RR )
40 simpl 
 |-  ( ( M e. RR /\ <" 0 M "> = <" 1 M "> ) -> M e. RR )
41 40 26 jctil 
 |-  ( ( M e. RR /\ <" 0 M "> = <" 1 M "> ) -> ( 1 e. RR /\ M e. RR ) )
42 simpr 
 |-  ( ( M e. RR /\ <" 0 M "> = <" 1 M "> ) -> <" 0 M "> = <" 1 M "> )
43 s2eq2seq 
 |-  ( ( ( 0 e. RR /\ M e. RR ) /\ ( 1 e. RR /\ M e. RR ) ) -> ( <" 0 M "> = <" 1 M "> <-> ( 0 = 1 /\ M = M ) ) )
44 43 simprbda 
 |-  ( ( ( ( 0 e. RR /\ M e. RR ) /\ ( 1 e. RR /\ M e. RR ) ) /\ <" 0 M "> = <" 1 M "> ) -> 0 = 1 )
45 39 40 41 42 44 syl1111anc 
 |-  ( ( M e. RR /\ <" 0 M "> = <" 1 M "> ) -> 0 = 1 )
46 38 45 mteqand 
 |-  ( M e. RR -> <" 0 M "> =/= <" 1 M "> )
47 46 6 7 3netr4g 
 |-  ( M e. RR -> X =/= Y )
48 22 36 47 3jca 
 |-  ( M e. RR -> ( X e. P /\ Y e. P /\ X =/= Y ) )
49 48 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
50 eqid 
 |-  ( ( Y ` 0 ) - ( X ` 0 ) ) = ( ( Y ` 0 ) - ( X ` 0 ) )
51 eqid 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( X ` 1 ) )
52 eqid 
 |-  ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) = ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) )
53 1 2 3 4 50 51 52 rrx2linest 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) } )
54 49 53 syl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( X L Y ) = { p e. P | ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) } )
55 8 54 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) } ) )
56 rabbi 
 |-  ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) ) <-> { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) } )
57 7 fveq1i 
 |-  ( Y ` 0 ) = ( <" 1 M "> ` 0 )
58 s2fv0 
 |-  ( 1 e. RR -> ( <" 1 M "> ` 0 ) = 1 )
59 26 58 mp1i 
 |-  ( M e. RR -> ( <" 1 M "> ` 0 ) = 1 )
60 57 59 eqtrid 
 |-  ( M e. RR -> ( Y ` 0 ) = 1 )
61 6 fveq1i 
 |-  ( X ` 0 ) = ( <" 0 M "> ` 0 )
62 0re 
 |-  0 e. RR
63 s2fv0 
 |-  ( 0 e. RR -> ( <" 0 M "> ` 0 ) = 0 )
64 62 63 mp1i 
 |-  ( M e. RR -> ( <" 0 M "> ` 0 ) = 0 )
65 61 64 eqtrid 
 |-  ( M e. RR -> ( X ` 0 ) = 0 )
66 60 65 oveq12d 
 |-  ( M e. RR -> ( ( Y ` 0 ) - ( X ` 0 ) ) = ( 1 - 0 ) )
67 1m0e1 
 |-  ( 1 - 0 ) = 1
68 66 67 eqtrdi 
 |-  ( M e. RR -> ( ( Y ` 0 ) - ( X ` 0 ) ) = 1 )
69 68 oveq1d 
 |-  ( M e. RR -> ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( 1 x. ( p ` 1 ) ) )
70 7 fveq1i 
 |-  ( Y ` 1 ) = ( <" 1 M "> ` 1 )
71 s2fv1 
 |-  ( M e. RR -> ( <" 1 M "> ` 1 ) = M )
72 70 71 eqtrid 
 |-  ( M e. RR -> ( Y ` 1 ) = M )
73 6 fveq1i 
 |-  ( X ` 1 ) = ( <" 0 M "> ` 1 )
74 s2fv1 
 |-  ( M e. RR -> ( <" 0 M "> ` 1 ) = M )
75 73 74 eqtrid 
 |-  ( M e. RR -> ( X ` 1 ) = M )
76 72 75 oveq12d 
 |-  ( M e. RR -> ( ( Y ` 1 ) - ( X ` 1 ) ) = ( M - M ) )
77 recn 
 |-  ( M e. RR -> M e. CC )
78 77 subidd 
 |-  ( M e. RR -> ( M - M ) = 0 )
79 76 78 eqtrd 
 |-  ( M e. RR -> ( ( Y ` 1 ) - ( X ` 1 ) ) = 0 )
80 79 oveq1d 
 |-  ( M e. RR -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) = ( 0 x. ( p ` 0 ) ) )
81 75 60 oveq12d 
 |-  ( M e. RR -> ( ( X ` 1 ) x. ( Y ` 0 ) ) = ( M x. 1 ) )
82 ax-1rid 
 |-  ( M e. RR -> ( M x. 1 ) = M )
83 81 82 eqtrd 
 |-  ( M e. RR -> ( ( X ` 1 ) x. ( Y ` 0 ) ) = M )
84 65 72 oveq12d 
 |-  ( M e. RR -> ( ( X ` 0 ) x. ( Y ` 1 ) ) = ( 0 x. M ) )
85 77 mul02d 
 |-  ( M e. RR -> ( 0 x. M ) = 0 )
86 84 85 eqtrd 
 |-  ( M e. RR -> ( ( X ` 0 ) x. ( Y ` 1 ) ) = 0 )
87 83 86 oveq12d 
 |-  ( M e. RR -> ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) = ( M - 0 ) )
88 77 subid1d 
 |-  ( M e. RR -> ( M - 0 ) = M )
89 87 88 eqtrd 
 |-  ( M e. RR -> ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) = M )
90 80 89 oveq12d 
 |-  ( M e. RR -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) = ( ( 0 x. ( p ` 0 ) ) + M ) )
91 69 90 eqeq12d 
 |-  ( M e. RR -> ( ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) <-> ( 1 x. ( p ` 1 ) ) = ( ( 0 x. ( p ` 0 ) ) + M ) ) )
92 91 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) <-> ( 1 x. ( p ` 1 ) ) = ( ( 0 x. ( p ` 0 ) ) + M ) ) )
93 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
94 93 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
95 94 mullidd 
 |-  ( p e. P -> ( 1 x. ( p ` 1 ) ) = ( p ` 1 ) )
96 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 0 ) e. RR )
97 96 recnd 
 |-  ( p e. P -> ( p ` 0 ) e. CC )
98 97 mul02d 
 |-  ( p e. P -> ( 0 x. ( p ` 0 ) ) = 0 )
99 98 oveq1d 
 |-  ( p e. P -> ( ( 0 x. ( p ` 0 ) ) + M ) = ( 0 + M ) )
100 95 99 eqeq12d 
 |-  ( p e. P -> ( ( 1 x. ( p ` 1 ) ) = ( ( 0 x. ( p ` 0 ) ) + M ) <-> ( p ` 1 ) = ( 0 + M ) ) )
101 92 100 sylan9bb 
 |-  ( ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) /\ p e. P ) -> ( ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) <-> ( p ` 1 ) = ( 0 + M ) ) )
102 101 bibi2d 
 |-  ( ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) /\ p e. P ) -> ( ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) ) <-> ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = ( 0 + M ) ) ) )
103 102 ralbidva 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) ) <-> A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = ( 0 + M ) ) ) )
104 77 addlidd 
 |-  ( M e. RR -> ( 0 + M ) = M )
105 104 adantr 
 |-  ( ( M e. RR /\ p e. P ) -> ( 0 + M ) = M )
106 105 eqeq2d 
 |-  ( ( M e. RR /\ p e. P ) -> ( ( p ` 1 ) = ( 0 + M ) <-> ( p ` 1 ) = M ) )
107 106 bibi2d 
 |-  ( ( M e. RR /\ p e. P ) -> ( ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = ( 0 + M ) ) <-> ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) ) )
108 107 ralbidva 
 |-  ( M e. RR -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = ( 0 + M ) ) <-> A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) ) )
109 108 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = ( 0 + M ) ) <-> A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) ) )
110 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) -> ( A = 0 /\ M = ( C / B ) ) ) )
111 oveq1 
 |-  ( A = 0 -> ( A x. ( p ` 0 ) ) = ( 0 x. ( p ` 0 ) ) )
112 111 adantr 
 |-  ( ( A = 0 /\ M = ( C / B ) ) -> ( A x. ( p ` 0 ) ) = ( 0 x. ( p ` 0 ) ) )
113 112 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 ` 0 ) ) = ( 0 x. ( p ` 0 ) ) )
114 98 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 ` 0 ) ) = 0 )
115 113 114 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 ` 0 ) ) = 0 )
116 115 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = ( 0 + ( B x. ( p ` 1 ) ) ) )
117 recn 
 |-  ( B e. RR -> B e. CC )
118 117 adantr 
 |-  ( ( B e. RR /\ B =/= 0 ) -> B e. CC )
119 118 3ad2ant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> B e. CC )
120 119 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 )
121 94 adantl 
 |-  ( ( ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) /\ ( A = 0 /\ M = ( C / B ) ) ) /\ p e. P ) -> ( p ` 1 ) e. CC )
122 120 121 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 ` 1 ) ) e. CC )
123 122 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 ` 1 ) ) ) = ( B x. ( p ` 1 ) ) )
124 116 123 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = ( B x. ( p ` 1 ) ) )
125 124 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( B x. ( p ` 1 ) ) = C ) )
126 simp3 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> C e. RR )
127 126 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> C e. CC )
128 127 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 )
129 simp2r 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> B =/= 0 )
130 129 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 )
131 128 120 121 130 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 ` 1 ) <-> ( B x. ( p ` 1 ) ) = C ) )
132 simpr 
 |-  ( ( A = 0 /\ M = ( C / B ) ) -> M = ( C / B ) )
133 132 eqcomd 
 |-  ( ( A = 0 /\ M = ( C / B ) ) -> ( C / B ) = M )
134 133 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 )
135 134 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 ` 1 ) <-> M = ( p ` 1 ) ) )
136 125 131 135 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> M = ( p ` 1 ) ) )
137 eqcom 
 |-  ( M = ( p ` 1 ) <-> ( p ` 1 ) = M )
138 136 137 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) )
139 138 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) )
140 139 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) ) )
141 110 140 impbid 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) <-> ( A = 0 /\ M = ( C / B ) ) ) )
142 103 109 141 3bitrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) ) <-> ( A = 0 /\ M = ( C / B ) ) ) )
143 56 142 bitr3id 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( p ` 1 ) ) = ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 0 ) ) + ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) } <-> ( A = 0 /\ M = ( C / B ) ) ) )
144 55 143 bitrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( G = ( X L Y ) <-> ( A = 0 /\ M = ( C / B ) ) ) )