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