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