Metamath Proof Explorer

Theorem tgdim01

Description: In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tgdim01.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgdim01.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgdim01.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
tgdim01.1 ⊢ ( 𝜑 → ¬ 𝐺 DimTarskiG≥ 2 )
tgdim01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgdim01.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgdim01.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion tgdim01 ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 tgdim01.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgdim01.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgdim01.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 tgdim01.1 ⊢ ( 𝜑 → ¬ 𝐺 DimTarskiG≥ 2 )
5 tgdim01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tgdim01.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgdim01.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
9 1 8 2 istrkg2ld ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
10 3 9 syl ⊢ ( 𝜑 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
11 4 10 mtbid ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
12 rexnal3 ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
13 12 con2bii ⊢ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ¬ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
14 11 13 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
15 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑦 ) )
16 15 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ) )
17 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ) )
18 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
19 18 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) )
20 16 17 19 3orbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
21 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑌 ) )
22 21 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ) )
23 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝐼 𝑌 ) )
24 23 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ) )
25 eleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
26 22 24 25 3orbi123d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑦 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
27 eleq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
28 oveq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 𝐼 𝑌 ) = ( 𝑍 𝐼 𝑌 ) )
29 28 eleq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ↔ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) )
30 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) )
31 30 eleq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
32 27 29 31 3orbi123d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
33 20 26 32 rspc3v ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
34 33 imp ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
35 5 6 7 14 34 syl31anc ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )