Metamath Proof Explorer

Theorem line2y

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

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 line2y.x 
 |-  X = { <. 1 , 0 >. , <. 2 , M >. }
7 line2y.y 
 |-  Y = { <. 1 , 0 >. , <. 2 , N >. }
8 5 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> 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. _V /\ M e. RR ) /\ 1 =/= 2 ) -> 0 e. RR )
18 simp2r 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 0 e. _V /\ M e. RR ) /\ 1 =/= 2 ) -> M e. RR )
19 17 18 prssd 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 0 e. _V /\ M e. RR ) /\ 1 =/= 2 ) -> { 0 , M } C_ RR )
20 16 19 fssd 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 0 e. _V /\ M e. RR ) /\ 1 =/= 2 ) -> { <. 1 , 0 >. , <. 2 , M >. } : { 1 , 2 } --> RR )
21 11 13 15 20 mp3an2i 
 |-  ( M e. RR -> { <. 1 , 0 >. , <. 2 , M >. } : { 1 , 2 } --> RR )
22 1 feq2i 
 |-  ( { <. 1 , 0 >. , <. 2 , M >. } : I --> RR <-> { <. 1 , 0 >. , <. 2 , M >. } : { 1 , 2 } --> RR )
23 21 22 sylibr 
 |-  ( M e. RR -> { <. 1 , 0 >. , <. 2 , M >. } : I --> RR )
24 reex 
 |-  RR e. _V
25 prex 
 |-  { 1 , 2 } e. _V
26 1 25 eqeltri 
 |-  I e. _V
27 24 26 elmap 
 |-  ( { <. 1 , 0 >. , <. 2 , M >. } e. ( RR ^m I ) <-> { <. 1 , 0 >. , <. 2 , M >. } : I --> RR )
28 23 27 sylibr 
 |-  ( M e. RR -> { <. 1 , 0 >. , <. 2 , M >. } e. ( RR ^m I ) )
29 28 6 3 3eltr4g 
 |-  ( M e. RR -> X e. P )
30 29 3ad2ant1 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> X e. P )
31 12 jctl 
 |-  ( N e. RR -> ( 0 e. _V /\ N e. RR ) )
32 14 a1i 
 |-  ( N e. RR -> 1 =/= 2 )
33 fprg 
 |-  ( ( ( 1 e. _V /\ 2 e. _V ) /\ ( 0 e. _V /\ N e. RR ) /\ 1 =/= 2 ) -> { <. 1 , 0 >. , <. 2 , N >. } : { 1 , 2 } --> { 0 , N } )
34 11 31 32 33 mp3an2i 
 |-  ( N e. RR -> { <. 1 , 0 >. , <. 2 , N >. } : { 1 , 2 } --> { 0 , N } )
35 0re 
 |-  0 e. RR
36 prssi 
 |-  ( ( 0 e. RR /\ N e. RR ) -> { 0 , N } C_ RR )
37 35 36 mpan 
 |-  ( N e. RR -> { 0 , N } C_ RR )
38 34 37 fssd 
 |-  ( N e. RR -> { <. 1 , 0 >. , <. 2 , N >. } : { 1 , 2 } --> RR )
39 1 feq2i 
 |-  ( { <. 1 , 0 >. , <. 2 , N >. } : I --> RR <-> { <. 1 , 0 >. , <. 2 , N >. } : { 1 , 2 } --> RR )
40 38 39 sylibr 
 |-  ( N e. RR -> { <. 1 , 0 >. , <. 2 , N >. } : I --> RR )
41 24 26 pm3.2i 
 |-  ( RR e. _V /\ I e. _V )
42 elmapg 
 |-  ( ( RR e. _V /\ I e. _V ) -> ( { <. 1 , 0 >. , <. 2 , N >. } e. ( RR ^m I ) <-> { <. 1 , 0 >. , <. 2 , N >. } : I --> RR ) )
43 41 42 mp1i 
 |-  ( N e. RR -> ( { <. 1 , 0 >. , <. 2 , N >. } e. ( RR ^m I ) <-> { <. 1 , 0 >. , <. 2 , N >. } : I --> RR ) )
44 40 43 mpbird 
 |-  ( N e. RR -> { <. 1 , 0 >. , <. 2 , N >. } e. ( RR ^m I ) )
45 44 7 3 3eltr4g 
 |-  ( N e. RR -> Y e. P )
46 45 3ad2ant2 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> Y e. P )
47 6 fveq1i 
 |-  ( X ` 1 ) = ( { <. 1 , 0 >. , <. 2 , M >. } ` 1 )
48 9 12 14 3pm3.2i 
 |-  ( 1 e. _V /\ 0 e. _V /\ 1 =/= 2 )
49 fvpr1g 
 |-  ( ( 1 e. _V /\ 0 e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , M >. } ` 1 ) = 0 )
50 48 49 mp1i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( { <. 1 , 0 >. , <. 2 , M >. } ` 1 ) = 0 )
51 47 50 syl5eq 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 1 ) = 0 )
52 7 fveq1i 
 |-  ( Y ` 1 ) = ( { <. 1 , 0 >. , <. 2 , N >. } ` 1 )
53 fvpr1g 
 |-  ( ( 1 e. _V /\ 0 e. _V /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , N >. } ` 1 ) = 0 )
54 48 53 mp1i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( { <. 1 , 0 >. , <. 2 , N >. } ` 1 ) = 0 )
55 52 54 syl5eq 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( Y ` 1 ) = 0 )
56 51 55 eqtr4d 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 1 ) = ( Y ` 1 ) )
57 simp3 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> M =/= N )
58 6 fveq1i 
 |-  ( X ` 2 ) = ( { <. 1 , 0 >. , <. 2 , M >. } ` 2 )
59 simp1 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> M e. RR )
60 14 a1i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> 1 =/= 2 )
61 fvpr2g 
 |-  ( ( 2 e. _V /\ M e. RR /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , M >. } ` 2 ) = M )
62 10 59 60 61 mp3an2i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( { <. 1 , 0 >. , <. 2 , M >. } ` 2 ) = M )
63 58 62 syl5eq 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 2 ) = M )
64 7 fveq1i 
 |-  ( Y ` 2 ) = ( { <. 1 , 0 >. , <. 2 , N >. } ` 2 )
65 simp2 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> N e. RR )
66 fvpr2g 
 |-  ( ( 2 e. _V /\ N e. RR /\ 1 =/= 2 ) -> ( { <. 1 , 0 >. , <. 2 , N >. } ` 2 ) = N )
67 10 65 60 66 mp3an2i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( { <. 1 , 0 >. , <. 2 , N >. } ` 2 ) = N )
68 64 67 syl5eq 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( Y ` 2 ) = N )
69 57 63 68 3netr4d 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 2 ) =/= ( Y ` 2 ) )
70 56 69 jca 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) )
71 30 46 70 3jca 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
72 71 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
73 1 2 3 4 rrx2vlinest 
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( X ` 1 ) } )
74 72 73 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( X ` 1 ) } )
75 8 74 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( G = ( X L Y ) <-> { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 1 ) = ( X ` 1 ) } ) )
76 48 49 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , M >. } ` 1 ) = 0
77 47 76 eqtri 
 |-  ( X ` 1 ) = 0
78 77 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( X ` 1 ) = 0 )
79 78 eqeq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( ( p ` 1 ) = ( X ` 1 ) <-> ( p ` 1 ) = 0 ) )
80 79 rabbidv 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> { p e. P | ( p ` 1 ) = ( X ` 1 ) } = { p e. P | ( p ` 1 ) = 0 } )
81 80 eqeq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 1 ) = ( X ` 1 ) } <-> { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 1 ) = 0 } ) )
82 rabbi 
 |-  ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 1 ) = 0 } )
83 1 3 line2ylem 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
84 83 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
85 oveq1 
 |-  ( B = 0 -> ( B x. ( p ` 2 ) ) = ( 0 x. ( p ` 2 ) ) )
86 85 3ad2ant2 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( B x. ( p ` 2 ) ) = ( 0 x. ( p ` 2 ) ) )
87 86 oveq2d 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) )
88 simp3 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> C = 0 )
89 87 88 eqeq12d 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) = 0 ) )
90 89 ad2antlr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) = 0 ) )
91 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
92 91 recnd 
 |-  ( p e. P -> ( p ` 2 ) e. CC )
93 92 mul02d 
 |-  ( p e. P -> ( 0 x. ( p ` 2 ) ) = 0 )
94 93 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( 0 x. ( p ` 2 ) ) = 0 )
95 94 oveq2d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) = ( ( A x. ( p ` 1 ) ) + 0 ) )
96 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
97 96 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
98 97 ad3antrrr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> A e. CC )
99 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
100 99 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
101 100 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( p ` 1 ) e. CC )
102 98 101 mulcld 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. CC )
103 102 addid1d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + 0 ) = ( A x. ( p ` 1 ) ) )
104 95 103 eqtrd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) = ( A x. ( p ` 1 ) ) )
105 104 eqeq1d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( 0 x. ( p ` 2 ) ) ) = 0 <-> ( A x. ( p ` 1 ) ) = 0 ) )
106 98 101 mul0ord 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) = 0 <-> ( A = 0 \/ ( p ` 1 ) = 0 ) ) )
107 eqneqall 
 |-  ( A = 0 -> ( A =/= 0 -> ( p ` 1 ) = 0 ) )
108 107 com12 
 |-  ( A =/= 0 -> ( A = 0 -> ( p ` 1 ) = 0 ) )
109 108 3ad2ant1 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( A = 0 -> ( p ` 1 ) = 0 ) )
110 109 ad2antlr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( A = 0 -> ( p ` 1 ) = 0 ) )
111 idd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( p ` 1 ) = 0 -> ( p ` 1 ) = 0 ) )
112 110 111 jaod 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A = 0 \/ ( p ` 1 ) = 0 ) -> ( p ` 1 ) = 0 ) )
113 olc 
 |-  ( ( p ` 1 ) = 0 -> ( A = 0 \/ ( p ` 1 ) = 0 ) )
114 112 113 impbid1 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A = 0 \/ ( p ` 1 ) = 0 ) <-> ( p ` 1 ) = 0 ) )
115 106 114 bitrd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) = 0 <-> ( p ` 1 ) = 0 ) )
116 90 105 115 3bitrd 
 |-  ( ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
117 116 ralrimiva 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) /\ ( A =/= 0 /\ B = 0 /\ C = 0 ) ) -> A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) )
118 117 ex 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) ) )
119 84 118 impbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( A. p e. P ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( p ` 1 ) = 0 ) <-> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
120 82 119 bitr3id 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( p ` 1 ) = 0 } <-> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
121 75 81 120 3bitrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( G = ( X L Y ) <-> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )