Metamath Proof Explorer

Theorem line2

Description: Example for a 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 }
line2.x 
|- X = { <. 1 , 0 >. , <. 2 , ( C / B ) >. }
line2.y 
|- Y = { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. }
Assertion line2 
|- ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> G = ( X L Y ) )

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 line2.x 
 |-  X = { <. 1 , 0 >. , <. 2 , ( C / B ) >. }
7 line2.y 
 |-  Y = { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. }
8 simp1 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> A e. RR )
9 8 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> A e. RR )
10 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
11 10 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( p ` 1 ) e. RR )
12 9 11 remulcld 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. RR )
13 12 recnd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. CC )
14 simpl2l 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> B e. RR )
15 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
16 15 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( p ` 2 ) e. RR )
17 14 16 remulcld 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. RR )
18 17 recnd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. CC )
19 simpl 
 |-  ( ( B e. RR /\ B =/= 0 ) -> B e. RR )
20 19 recnd 
 |-  ( ( B e. RR /\ B =/= 0 ) -> B e. CC )
21 20 3ad2ant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> B e. CC )
22 21 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> B e. CC )
23 simp2r 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> B =/= 0 )
24 23 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> B =/= 0 )
25 13 18 22 24 divdird 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( ( ( A x. ( p ` 1 ) ) / B ) + ( ( B x. ( p ` 2 ) ) / B ) ) )
26 15 recnd 
 |-  ( p e. P -> ( p ` 2 ) e. CC )
27 26 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( p ` 2 ) e. CC )
28 27 22 24 divcan3d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) / B ) = ( p ` 2 ) )
29 28 oveq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) / B ) + ( ( B x. ( p ` 2 ) ) / B ) ) = ( ( ( A x. ( p ` 1 ) ) / B ) + ( p ` 2 ) ) )
30 25 29 eqtrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( ( ( A x. ( p ` 1 ) ) / B ) + ( p ` 2 ) ) )
31 30 eqeq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( C / B ) <-> ( ( ( A x. ( p ` 1 ) ) / B ) + ( p ` 2 ) ) = ( C / B ) ) )
32 12 14 24 redivcld 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) / B ) e. RR )
33 32 recnd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) / B ) e. CC )
34 simp3 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> C e. RR )
35 19 3ad2ant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> B e. RR )
36 34 35 23 redivcld 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( C / B ) e. RR )
37 36 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( C / B ) e. CC )
38 37 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( C / B ) e. CC )
39 33 27 38 addrsub 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( A x. ( p ` 1 ) ) / B ) + ( p ` 2 ) ) = ( C / B ) <-> ( p ` 2 ) = ( ( C / B ) - ( ( A x. ( p ` 1 ) ) / B ) ) ) )
40 simpl3 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> C e. RR )
41 40 14 24 redivcld 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( C / B ) e. RR )
42 41 recnd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( C / B ) e. CC )
43 33 42 negsubdi2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( ( ( A x. ( p ` 1 ) ) / B ) - ( C / B ) ) = ( ( C / B ) - ( ( A x. ( p ` 1 ) ) / B ) ) )
44 33 42 negsubdid 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( ( ( A x. ( p ` 1 ) ) / B ) - ( C / B ) ) = ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) )
45 43 44 eqtr3d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( C / B ) - ( ( A x. ( p ` 1 ) ) / B ) ) = ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) )
46 45 eqeq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 2 ) = ( ( C / B ) - ( ( A x. ( p ` 1 ) ) / B ) ) <-> ( p ` 2 ) = ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) ) )
47 31 39 46 3bitrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( C / B ) <-> ( p ` 2 ) = ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) ) )
48 12 17 readdcld 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) e. RR )
49 48 recnd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) e. CC )
50 34 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> C e. CC )
51 50 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> C e. CC )
52 recn 
 |-  ( B e. RR -> B e. CC )
53 52 anim1i 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
54 53 3ad2ant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( B e. CC /\ B =/= 0 ) )
55 54 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( B e. CC /\ B =/= 0 ) )
56 div11 
 |-  ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( C / B ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
57 49 51 55 56 syl3anc 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) / B ) = ( C / B ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
58 13 22 24 divnegd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( ( A x. ( p ` 1 ) ) / B ) = ( -u ( A x. ( p ` 1 ) ) / B ) )
59 8 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> A e. CC )
60 59 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> A e. CC )
61 10 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
62 61 adantl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( p ` 1 ) e. CC )
63 60 62 mulneg1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( -u A x. ( p ` 1 ) ) = -u ( A x. ( p ` 1 ) ) )
64 63 eqcomd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( A x. ( p ` 1 ) ) = ( -u A x. ( p ` 1 ) ) )
65 64 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( -u ( A x. ( p ` 1 ) ) / B ) = ( ( -u A x. ( p ` 1 ) ) / B ) )
66 58 65 eqtrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( ( A x. ( p ` 1 ) ) / B ) = ( ( -u A x. ( p ` 1 ) ) / B ) )
67 renegcl 
 |-  ( A e. RR -> -u A e. RR )
68 67 recnd 
 |-  ( A e. RR -> -u A e. CC )
69 68 3ad2ant1 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> -u A e. CC )
70 69 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u A e. CC )
71 div23 
 |-  ( ( -u A e. CC /\ ( p ` 1 ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( -u A x. ( p ` 1 ) ) / B ) = ( ( -u A / B ) x. ( p ` 1 ) ) )
72 70 62 55 71 syl3anc 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( -u A x. ( p ` 1 ) ) / B ) = ( ( -u A / B ) x. ( p ` 1 ) ) )
73 6 fveq1i 
 |-  ( X ` 1 ) = ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 )
74 1ex 
 |-  1 e. _V
75 c0ex 
 |-  0 e. _V
76 1ne2 
 |-  1 =/= 2
77 74 75 76 3pm3.2i 
 |-  ( 1 e. _V /\ 0 e. _V /\ 1 =/= 2 )
78 fvpr1g 
 |-  ( ( 1 e. _V /\ 0 e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 ) = 0 )
79 77 78 mp1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 ) = 0 )
80 73 79 syl5eq 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( X ` 1 ) = 0 )
81 80 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( X ` 1 ) = 0 )
82 81 oveq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 1 ) - ( X ` 1 ) ) = ( ( p ` 1 ) - 0 ) )
83 62 subid1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 1 ) - 0 ) = ( p ` 1 ) )
84 82 83 eqtr2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( p ` 1 ) = ( ( p ` 1 ) - ( X ` 1 ) ) )
85 84 oveq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( -u A / B ) x. ( p ` 1 ) ) = ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) )
86 66 72 85 3eqtrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> -u ( ( A x. ( p ` 1 ) ) / B ) = ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) )
87 86 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) = ( ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) )
88 87 eqeq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 2 ) = ( -u ( ( A x. ( p ` 1 ) ) / B ) + ( C / B ) ) <-> ( p ` 2 ) = ( ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) ) )
89 47 57 88 3bitr3d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 2 ) = ( ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) ) )
90 recn 
 |-  ( C e. RR -> C e. CC )
91 90 adantl 
 |-  ( ( A e. RR /\ C e. RR ) -> C e. CC )
92 recn 
 |-  ( A e. RR -> A e. CC )
93 92 adantr 
 |-  ( ( A e. RR /\ C e. RR ) -> A e. CC )
94 sub32 
 |-  ( ( C e. CC /\ A e. CC /\ C e. CC ) -> ( ( C - A ) - C ) = ( ( C - C ) - A ) )
95 subid 
 |-  ( C e. CC -> ( C - C ) = 0 )
96 95 3ad2ant1 
 |-  ( ( C e. CC /\ A e. CC /\ C e. CC ) -> ( C - C ) = 0 )
97 96 oveq1d 
 |-  ( ( C e. CC /\ A e. CC /\ C e. CC ) -> ( ( C - C ) - A ) = ( 0 - A ) )
98 df-neg 
 |-  -u A = ( 0 - A )
99 97 98 eqtr4di 
 |-  ( ( C e. CC /\ A e. CC /\ C e. CC ) -> ( ( C - C ) - A ) = -u A )
100 94 99 eqtr2d 
 |-  ( ( C e. CC /\ A e. CC /\ C e. CC ) -> -u A = ( ( C - A ) - C ) )
101 91 93 91 100 syl3anc 
 |-  ( ( A e. RR /\ C e. RR ) -> -u A = ( ( C - A ) - C ) )
102 101 3adant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> -u A = ( ( C - A ) - C ) )
103 102 oveq1d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( -u A / B ) = ( ( ( C - A ) - C ) / B ) )
104 103 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( -u A / B ) = ( ( ( C - A ) - C ) / B ) )
105 104 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) = ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) )
106 105 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) = ( ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) )
107 106 eqeq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 2 ) = ( ( ( -u A / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) <-> ( p ` 2 ) = ( ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) ) )
108 89 107 bitrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 2 ) = ( ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) ) )
109 7 fveq1i 
 |-  ( Y ` 2 ) = ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 2 )
110 2ex 
 |-  2 e. _V
111 110 a1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> 2 e. _V )
112 resubcl 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C - A ) e. RR )
113 112 ancoms 
 |-  ( ( A e. RR /\ C e. RR ) -> ( C - A ) e. RR )
114 113 3adant2 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( C - A ) e. RR )
115 114 35 23 redivcld 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( C - A ) / B ) e. RR )
116 76 a1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> 1 =/= 2 )
117 111 115 116 3jca 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( 2 e. _V /\ ( ( C - A ) / B ) e. RR /\ 1 =/= 2 ) )
118 117 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( 2 e. _V /\ ( ( C - A ) / B ) e. RR /\ 1 =/= 2 ) )
119 fvpr2g 
 |-  ( ( 2 e. _V /\ ( ( C - A ) / B ) e. RR /\ 1 =/= 2 ) -> ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 2 ) = ( ( C - A ) / B ) )
120 118 119 syl 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 2 ) = ( ( C - A ) / B ) )
121 109 120 syl5eq 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( Y ` 2 ) = ( ( C - A ) / B ) )
122 6 fveq1i 
 |-  ( X ` 2 ) = ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 2 )
123 fvpr2g 
 |-  ( ( 2 e. _V /\ ( C / B ) e. RR /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 2 ) = ( C / B ) )
124 110 36 116 123 mp3an2i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 2 ) = ( C / B ) )
125 122 124 syl5eq 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( X ` 2 ) = ( C / B ) )
126 125 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( X ` 2 ) = ( C / B ) )
127 121 126 oveq12d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( ( C - A ) / B ) - ( C / B ) ) )
128 34 8 resubcld 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( C - A ) e. RR )
129 128 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( C - A ) e. CC )
130 divsubdir 
 |-  ( ( ( C - A ) e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( C - A ) - C ) / B ) = ( ( ( C - A ) / B ) - ( C / B ) ) )
131 129 50 54 130 syl3anc 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( C - A ) - C ) / B ) = ( ( ( C - A ) / B ) - ( C / B ) ) )
132 131 eqcomd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( C - A ) / B ) - ( C / B ) ) = ( ( ( C - A ) - C ) / B ) )
133 132 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( C - A ) / B ) - ( C / B ) ) = ( ( ( C - A ) - C ) / B ) )
134 127 133 eqtr2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( C - A ) - C ) / B ) = ( ( Y ` 2 ) - ( X ` 2 ) ) )
135 134 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) )
136 135 oveq1d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) )
137 136 eqeq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 2 ) = ( ( ( ( ( C - A ) - C ) / B ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) <-> ( p ` 2 ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) ) )
138 7 fveq1i 
 |-  ( Y ` 1 ) = ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 1 )
139 74 74 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 1 ) = 1 )
140 76 139 ax-mp 
 |-  ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 1 ) = 1
141 138 140 eqtri 
 |-  ( Y ` 1 ) = 1
142 74 75 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 ) = 0 )
143 76 142 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 ) = 0
144 73 143 eqtri 
 |-  ( X ` 1 ) = 0
145 141 144 oveq12i 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = ( 1 - 0 )
146 1m0e1 
 |-  ( 1 - 0 ) = 1
147 145 146 eqtri 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = 1
148 147 a1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) = 1 )
149 148 oveq2d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / 1 ) )
150 110 115 116 119 mp3an2i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 2 ) = ( ( C - A ) / B ) )
151 109 150 syl5eq 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( Y ` 2 ) = ( ( C - A ) / B ) )
152 115 recnd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( C - A ) / B ) e. CC )
153 151 152 eqeltrd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( Y ` 2 ) e. CC )
154 125 37 eqeltrd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( X ` 2 ) e. CC )
155 153 154 subcld 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
156 155 div1d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) / 1 ) = ( ( Y ` 2 ) - ( X ` 2 ) ) )
157 149 156 eqtrd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) = ( ( Y ` 2 ) - ( X ` 2 ) ) )
158 157 oveq1d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) )
159 158 125 oveq12d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) )
160 159 adantr 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) )
161 160 eqcomd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) )
162 161 eqeq2d 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( p ` 2 ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( C / B ) ) <-> ( p ` 2 ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) ) )
163 108 137 162 3bitrd 
 |-  ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 2 ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) ) )
164 163 rabbidva 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 2 ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )
165 5 a1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> G = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )
166 74 110 pm3.2i 
 |-  ( 1 e. _V /\ 2 e. _V )
167 36 75 jctil 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( 0 e. _V /\ ( C / B ) e. RR ) )
168 fprg 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 0 e. _V /\ ( C / B ) e. RR ) /\ 1 =/= 2 ) -> { <. 1 , 0 >. , <. 2 , ( C / B ) >. } : { 1 , 2 } --> { 0 , ( C / B ) } )
169 166 167 116 168 mp3an2i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { <. 1 , 0 >. , <. 2 , ( C / B ) >. } : { 1 , 2 } --> { 0 , ( C / B ) } )
170 0red 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> 0 e. RR )
171 170 36 prssd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { 0 , ( C / B ) } C_ RR )
172 169 171 fssd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { <. 1 , 0 >. , <. 2 , ( C / B ) >. } : { 1 , 2 } --> RR )
173 6 feq1i 
 |-  ( X : { 1 , 2 } --> RR <-> { <. 1 , 0 >. , <. 2 , ( C / B ) >. } : { 1 , 2 } --> RR )
174 172 173 sylibr 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> X : { 1 , 2 } --> RR )
175 reex 
 |-  RR e. _V
176 prex 
 |-  { 1 , 2 } e. _V
177 175 176 elmap 
 |-  ( X e. ( RR ^m { 1 , 2 } ) <-> X : { 1 , 2 } --> RR )
178 174 177 sylibr 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> X e. ( RR ^m { 1 , 2 } ) )
179 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m { 1 , 2 } )
180 3 179 eqtri 
 |-  P = ( RR ^m { 1 , 2 } )
181 178 180 eleqtrrdi 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> X e. P )
182 115 74 jctil 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( 1 e. _V /\ ( ( C - A ) / B ) e. RR ) )
183 fprg 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 1 e. _V /\ ( ( C - A ) / B ) e. RR ) /\ 1 =/= 2 ) -> { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } : { 1 , 2 } --> { 1 , ( ( C - A ) / B ) } )
184 166 182 116 183 mp3an2i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } : { 1 , 2 } --> { 1 , ( ( C - A ) / B ) } )
185 1red 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> 1 e. RR )
186 185 115 prssd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { 1 , ( ( C - A ) / B ) } C_ RR )
187 184 186 fssd 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } : { 1 , 2 } --> RR )
188 7 feq1i 
 |-  ( Y : { 1 , 2 } --> RR <-> { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } : { 1 , 2 } --> RR )
189 187 188 sylibr 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> Y : { 1 , 2 } --> RR )
190 175 176 elmap 
 |-  ( Y e. ( RR ^m { 1 , 2 } ) <-> Y : { 1 , 2 } --> RR )
191 189 190 sylibr 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> Y e. ( RR ^m { 1 , 2 } ) )
192 191 180 eleqtrrdi 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> Y e. P )
193 0ne1 
 |-  0 =/= 1
194 77 78 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , ( C / B ) >. } ` 1 ) = 0
195 73 194 eqtri 
 |-  ( X ` 1 ) = 0
196 74 74 76 3pm3.2i 
 |-  ( 1 e. _V /\ 1 e. _V /\ 1 =/= 2 )
197 fvpr1g 
 |-  ( ( 1 e. _V /\ 1 e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 1 ) = 1 )
198 196 197 ax-mp 
 |-  ( { <. 1 , 1 >. , <. 2 , ( ( C - A ) / B ) >. } ` 1 ) = 1
199 138 198 eqtri 
 |-  ( Y ` 1 ) = 1
200 195 199 neeq12i 
 |-  ( ( X ` 1 ) =/= ( Y ` 1 ) <-> 0 =/= 1 )
201 193 200 mpbir 
 |-  ( X ` 1 ) =/= ( Y ` 1 )
202 201 a1i 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
203 eqid 
 |-  ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) )
204 1 2 3 4 203 rrx2linesl 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( p ` 2 ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )
205 181 192 202 204 syl3anc 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> ( X L Y ) = { p e. P | ( p ` 2 ) = ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) ) x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )
206 164 165 205 3eqtr4d 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) -> G = ( X L Y ) )