Metamath Proof Explorer


Theorem colline

Description: Three points are colinear iff there is a line through all three of them. Theorem 6.23 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 28-May-2019)

Ref Expression
Hypotheses tglineintmo.p P=BaseG
tglineintmo.i I=ItvG
tglineintmo.l L=Line𝒢G
tglineintmo.g φG𝒢Tarski
colline.1 φXP
colline.2 φYP
colline.3 φZP
colline.4 φ2P
Assertion colline φXYLZY=ZaranLXaYaZa

Proof

Step Hyp Ref Expression
1 tglineintmo.p P=BaseG
2 tglineintmo.i I=ItvG
3 tglineintmo.l L=Line𝒢G
4 tglineintmo.g φG𝒢Tarski
5 colline.1 φXP
6 colline.2 φYP
7 colline.3 φZP
8 colline.4 φ2P
9 4 ad4antr φY=ZX=ZxPXxG𝒢Tarski
10 5 ad4antr φY=ZX=ZxPXxXP
11 simplr φY=ZX=ZxPXxxP
12 simpr φY=ZX=ZxPXxXx
13 1 2 3 9 10 11 12 tgelrnln φY=ZX=ZxPXxXLxranL
14 1 2 3 9 10 11 12 tglinerflx1 φY=ZX=ZxPXxXXLx
15 simp-4r φY=ZX=ZxPXxY=Z
16 simpllr φY=ZX=ZxPXxX=Z
17 16 14 eqeltrrd φY=ZX=ZxPXxZXLx
18 15 17 eqeltrd φY=ZX=ZxPXxYXLx
19 eleq2 a=XLxXaXXLx
20 eleq2 a=XLxYaYXLx
21 eleq2 a=XLxZaZXLx
22 19 20 21 3anbi123d a=XLxXaYaZaXXLxYXLxZXLx
23 22 rspcev XLxranLXXLxYXLxZXLxaranLXaYaZa
24 13 14 18 17 23 syl13anc φY=ZX=ZxPXxaranLXaYaZa
25 eqid distG=distG
26 1 25 2 4 8 5 tglowdim1i φxPXx
27 26 ad2antrr φY=ZX=ZxPXx
28 24 27 r19.29a φY=ZX=ZaranLXaYaZa
29 4 ad2antrr φY=ZXZG𝒢Tarski
30 5 ad2antrr φY=ZXZXP
31 7 ad2antrr φY=ZXZZP
32 simpr φY=ZXZXZ
33 1 2 3 29 30 31 32 tgelrnln φY=ZXZXLZranL
34 1 2 3 29 30 31 32 tglinerflx1 φY=ZXZXXLZ
35 simplr φY=ZXZY=Z
36 1 2 3 29 30 31 32 tglinerflx2 φY=ZXZZXLZ
37 35 36 eqeltrd φY=ZXZYXLZ
38 eleq2 a=XLZXaXXLZ
39 eleq2 a=XLZYaYXLZ
40 eleq2 a=XLZZaZXLZ
41 38 39 40 3anbi123d a=XLZXaYaZaXXLZYXLZZXLZ
42 41 rspcev XLZranLXXLZYXLZZXLZaranLXaYaZa
43 33 34 37 36 42 syl13anc φY=ZXZaranLXaYaZa
44 28 43 pm2.61dane φY=ZaranLXaYaZa
45 44 adantlr φXYLZY=ZY=ZaranLXaYaZa
46 simpll φXYLZY=ZYZφ
47 simpr φXYLZY=ZYZYZ
48 47 neneqd φXYLZY=ZYZ¬Y=Z
49 simplr φXYLZY=ZYZXYLZY=Z
50 orel2 ¬Y=ZXYLZY=ZXYLZ
51 48 49 50 sylc φXYLZY=ZYZXYLZ
52 4 ad2antrr φXYLZYZG𝒢Tarski
53 6 ad2antrr φXYLZYZYP
54 7 ad2antrr φXYLZYZZP
55 simpr φXYLZYZYZ
56 1 2 3 52 53 54 55 tgelrnln φXYLZYZYLZranL
57 46 51 47 56 syl21anc φXYLZY=ZYZYLZranL
58 1 2 3 52 53 54 55 tglinerflx1 φXYLZYZYYLZ
59 46 51 47 58 syl21anc φXYLZY=ZYZYYLZ
60 1 2 3 52 53 54 55 tglinerflx2 φXYLZYZZYLZ
61 46 51 47 60 syl21anc φXYLZY=ZYZZYLZ
62 eleq2 a=YLZXaXYLZ
63 eleq2 a=YLZYaYYLZ
64 eleq2 a=YLZZaZYLZ
65 62 63 64 3anbi123d a=YLZXaYaZaXYLZYYLZZYLZ
66 65 rspcev YLZranLXYLZYYLZZYLZaranLXaYaZa
67 57 51 59 61 66 syl13anc φXYLZY=ZYZaranLXaYaZa
68 45 67 pm2.61dane φXYLZY=ZaranLXaYaZa
69 df-ne YZ¬Y=Z
70 simplr1 φaranLXaYaZaYZXa
71 4 ad3antrrr φaranLXaYaZaYZG𝒢Tarski
72 6 ad3antrrr φaranLXaYaZaYZYP
73 7 ad3antrrr φaranLXaYaZaYZZP
74 simpr φaranLXaYaZaYZYZ
75 simpllr φaranLXaYaZaYZaranL
76 simplr2 φaranLXaYaZaYZYa
77 simplr3 φaranLXaYaZaYZZa
78 1 2 3 71 72 73 74 74 75 76 77 tglinethru φaranLXaYaZaYZa=YLZ
79 70 78 eleqtrd φaranLXaYaZaYZXYLZ
80 79 ex φaranLXaYaZaYZXYLZ
81 69 80 syl5bir φaranLXaYaZa¬Y=ZXYLZ
82 81 orrd φaranLXaYaZaY=ZXYLZ
83 82 orcomd φaranLXaYaZaXYLZY=Z
84 83 r19.29an φaranLXaYaZaXYLZY=Z
85 68 84 impbida φXYLZY=ZaranLXaYaZa