Metamath Proof Explorer


Theorem axtglowdim2

Description: Lower dimension axiom for dimension 2, Axiom A8 of Schwabhauser p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses axtrkge.p P = Base G
axtrkge.d - ˙ = dist G
axtrkge.i I = Itv G
axtglowdim2.v φ G V
axtglowdim2.g φ G Dim 𝒢 2
Assertion axtglowdim2 φ x P y P z P ¬ z x I y x z I y y x I z

Proof

Step Hyp Ref Expression
1 axtrkge.p P = Base G
2 axtrkge.d - ˙ = dist G
3 axtrkge.i I = Itv G
4 axtglowdim2.v φ G V
5 axtglowdim2.g φ G Dim 𝒢 2
6 1 2 3 istrkg2ld G V G Dim 𝒢 2 x P y P z P ¬ z x I y x z I y y x I z
7 4 6 syl φ G Dim 𝒢 2 x P y P z P ¬ z x I y x z I y y x I z
8 5 7 mpbid φ x P y P z P ¬ z x I y x z I y y x I z