Metamath Proof Explorer


Theorem lncom

Description: Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019)

Ref Expression
Hypotheses btwnlng1.p P = Base G
btwnlng1.i I = Itv G
btwnlng1.l L = Line 𝒢 G
btwnlng1.g φ G 𝒢 Tarski
btwnlng1.x φ X P
btwnlng1.y φ Y P
btwnlng1.z φ Z P
btwnlng1.d φ X Y
lncom.1 φ Z Y L X
Assertion lncom φ Z X L Y

Proof

Step Hyp Ref Expression
1 btwnlng1.p P = Base G
2 btwnlng1.i I = Itv G
3 btwnlng1.l L = Line 𝒢 G
4 btwnlng1.g φ G 𝒢 Tarski
5 btwnlng1.x φ X P
6 btwnlng1.y φ Y P
7 btwnlng1.z φ Z P
8 btwnlng1.d φ X Y
9 lncom.1 φ Z Y L X
10 3orcomb Z X I Y X Z I Y Y X I Z Z X I Y Y X I Z X Z I Y
11 eqid dist G = dist G
12 1 11 2 4 5 7 6 tgbtwncomb φ Z X I Y Z Y I X
13 1 11 2 4 5 6 7 tgbtwncomb φ Y X I Z Y Z I X
14 1 11 2 4 7 5 6 tgbtwncomb φ X Z I Y X Y I Z
15 12 13 14 3orbi123d φ Z X I Y Y X I Z X Z I Y Z Y I X Y Z I X X Y I Z
16 10 15 syl5bb φ Z X I Y X Z I Y Y X I Z Z Y I X Y Z I X X Y I Z
17 1 3 2 4 5 6 8 7 tgellng φ Z X L Y Z X I Y X Z I Y Y X I Z
18 8 necomd φ Y X
19 1 3 2 4 6 5 18 7 tgellng φ Z Y L X Z Y I X Y Z I X X Y I Z
20 16 17 19 3bitr4d φ Z X L Y Z Y L X
21 9 20 mpbird φ Z X L Y