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 = ( 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 }
line2y.x 
|- X = <" 0 M ">
line2y.y 
|- Y = <" 0 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 = ( 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 line2y.x 
 |-  X = <" 0 M ">
7 line2y.y 
 |-  Y = <" 0 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 ` 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 22 3ad2ant1 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> X e. P )
24 s2len 
 |-  ( # ` <" 0 N "> ) = 2
25 24 eqcomi 
 |-  2 = ( # ` <" 0 N "> )
26 25 a1i 
 |-  ( N e. RR -> 2 = ( # ` <" 0 N "> ) )
27 0red 
 |-  ( N e. RR -> 0 e. RR )
28 id 
 |-  ( N e. RR -> N e. RR )
29 27 28 s2cld 
 |-  ( N e. RR -> <" 0 N "> e. Word RR )
30 26 29 wrdfd 
 |-  ( N e. RR -> <" 0 N "> : ( 0 ..^ 2 ) --> RR )
31 1 feq2i 
 |-  ( <" 0 N "> : I --> RR <-> <" 0 N "> : ( 0 ..^ 2 ) --> RR )
32 30 31 sylibr 
 |-  ( N e. RR -> <" 0 N "> : I --> RR )
33 18 19 pm3.2i 
 |-  ( RR e. _V /\ I e. _V )
34 elmapg 
 |-  ( ( RR e. _V /\ I e. _V ) -> ( <" 0 N "> e. ( RR ^m I ) <-> <" 0 N "> : I --> RR ) )
35 33 34 mp1i 
 |-  ( N e. RR -> ( <" 0 N "> e. ( RR ^m I ) <-> <" 0 N "> : I --> RR ) )
36 32 35 mpbird 
 |-  ( N e. RR -> <" 0 N "> e. ( RR ^m I ) )
37 36 7 3 3eltr4g 
 |-  ( N e. RR -> Y e. P )
38 37 3ad2ant2 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> Y e. P )
39 6 fveq1i 
 |-  ( X ` 0 ) = ( <" 0 M "> ` 0 )
40 0re 
 |-  0 e. RR
41 s2fv0 
 |-  ( 0 e. RR -> ( <" 0 M "> ` 0 ) = 0 )
42 40 41 mp1i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( <" 0 M "> ` 0 ) = 0 )
43 39 42 eqtrid 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 0 ) = 0 )
44 7 fveq1i 
 |-  ( Y ` 0 ) = ( <" 0 N "> ` 0 )
45 s2fv0 
 |-  ( 0 e. RR -> ( <" 0 N "> ` 0 ) = 0 )
46 40 45 mp1i 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( <" 0 N "> ` 0 ) = 0 )
47 44 46 eqtrid 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( Y ` 0 ) = 0 )
48 43 47 eqtr4d 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 0 ) = ( Y ` 0 ) )
49 simp3 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> M =/= N )
50 6 fveq1i 
 |-  ( X ` 1 ) = ( <" 0 M "> ` 1 )
51 s2fv1 
 |-  ( M e. RR -> ( <" 0 M "> ` 1 ) = M )
52 51 3ad2ant1 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( <" 0 M "> ` 1 ) = M )
53 50 52 eqtrid 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 1 ) = M )
54 7 fveq1i 
 |-  ( Y ` 1 ) = ( <" 0 N "> ` 1 )
55 s2fv1 
 |-  ( N e. RR -> ( <" 0 N "> ` 1 ) = N )
56 55 3ad2ant2 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( <" 0 N "> ` 1 ) = N )
57 54 56 eqtrid 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( Y ` 1 ) = N )
58 49 53 57 3netr4d 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
59 48 58 jca 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) )
60 23 38 59 3jca 
 |-  ( ( M e. RR /\ N e. RR /\ M =/= N ) -> ( X e. P /\ Y e. P /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) ) )
61 60 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 ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) ) )
62 1 2 3 4 rrx2vlinest 
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) ) -> ( X L Y ) = { p e. P | ( p ` 0 ) = ( X ` 0 ) } )
63 61 62 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 ` 0 ) = ( X ` 0 ) } )
64 8 63 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( p ` 0 ) = ( X ` 0 ) } ) )
65 40 41 ax-mp 
 |-  ( <" 0 M "> ` 0 ) = 0
66 39 65 eqtri 
 |-  ( X ` 0 ) = 0
67 66 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( X ` 0 ) = 0 )
68 67 eqeq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( ( p ` 0 ) = ( X ` 0 ) <-> ( p ` 0 ) = 0 ) )
69 68 rabbidv 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> { p e. P | ( p ` 0 ) = ( X ` 0 ) } = { p e. P | ( p ` 0 ) = 0 } )
70 69 eqeq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( p ` 0 ) = ( X ` 0 ) } <-> { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( p ` 0 ) = 0 } ) )
71 rabbi 
 |-  ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) <-> { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( p ` 0 ) = 0 } )
72 1 3 line2ylem 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
73 72 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) -> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
74 oveq1 
 |-  ( B = 0 -> ( B x. ( p ` 1 ) ) = ( 0 x. ( p ` 1 ) ) )
75 74 3ad2ant2 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( B x. ( p ` 1 ) ) = ( 0 x. ( p ` 1 ) ) )
76 75 oveq2d 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = ( ( A x. ( p ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) )
77 simp3 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> C = 0 )
78 76 77 eqeq12d 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( A x. ( p ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) = 0 ) )
79 78 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( ( A x. ( p ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) = 0 ) )
80 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
81 80 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
82 81 mul02d 
 |-  ( p e. P -> ( 0 x. ( p ` 1 ) ) = 0 )
83 82 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 ` 1 ) ) = 0 )
84 83 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 ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) = ( ( A x. ( p ` 0 ) ) + 0 ) )
85 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
86 85 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
87 86 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 )
88 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 0 ) e. RR )
89 88 recnd 
 |-  ( p e. P -> ( p ` 0 ) e. CC )
90 89 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 ` 0 ) e. CC )
91 87 90 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 ` 0 ) ) e. CC )
92 91 addridd 
 |-  ( ( ( ( ( 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 ` 0 ) ) + 0 ) = ( A x. ( p ` 0 ) ) )
93 84 92 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 ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) = ( A x. ( p ` 0 ) ) )
94 93 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 ` 0 ) ) + ( 0 x. ( p ` 1 ) ) ) = 0 <-> ( A x. ( p ` 0 ) ) = 0 ) )
95 87 90 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 ` 0 ) ) = 0 <-> ( A = 0 \/ ( p ` 0 ) = 0 ) ) )
96 eqneqall 
 |-  ( A = 0 -> ( A =/= 0 -> ( p ` 0 ) = 0 ) )
97 96 com12 
 |-  ( A =/= 0 -> ( A = 0 -> ( p ` 0 ) = 0 ) )
98 97 3ad2ant1 
 |-  ( ( A =/= 0 /\ B = 0 /\ C = 0 ) -> ( A = 0 -> ( p ` 0 ) = 0 ) )
99 98 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 ` 0 ) = 0 ) )
100 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 ` 0 ) = 0 -> ( p ` 0 ) = 0 ) )
101 99 100 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 ` 0 ) = 0 ) -> ( p ` 0 ) = 0 ) )
102 olc 
 |-  ( ( p ` 0 ) = 0 -> ( A = 0 \/ ( p ` 0 ) = 0 ) )
103 101 102 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 ` 0 ) = 0 ) <-> ( p ` 0 ) = 0 ) )
104 95 103 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 ` 0 ) ) = 0 <-> ( p ` 0 ) = 0 ) )
105 79 94 104 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) )
106 105 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) )
107 106 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) ) )
108 73 107 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 ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 0 ) = 0 ) <-> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
109 71 108 bitr3id 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( M e. RR /\ N e. RR /\ M =/= N ) ) -> ( { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C } = { p e. P | ( p ` 0 ) = 0 } <-> ( A =/= 0 /\ B = 0 /\ C = 0 ) ) )
110 64 70 109 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 ) ) )