Metamath Proof Explorer

Theorem tgcolg

Description: We choose the notation ( Z e. ( X L Y ) \/ X = Y ) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion tgcolg ( 𝜑 → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 animorr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
9 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
10 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐺 ∈ TarskiG )
11 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 ∈ 𝑃 )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝑃 )
13 1 9 3 10 11 12 tgbtwntriv2 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( 𝑍 𝐼 𝑋 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
15 14 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑍 𝐼 𝑋 ) = ( 𝑍 𝐼 𝑌 ) )
16 13 15 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) )
17 16 3mix2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
18 8 17 2thd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
20 19 neneqd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑋 = 𝑌 )
21 biorf ⊢ ( ¬ 𝑋 = 𝑌 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 = 𝑌 ∨ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 = 𝑌 ∨ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) )
23 orcom ⊢ ( ( 𝑋 = 𝑌 ∨ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
24 22 23 bitrdi ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ) )
25 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐺 ∈ TarskiG )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝑃 )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝑃 )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑍 ∈ 𝑃 )
29 1 2 3 25 26 27 19 28 tgellng ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
30 24 29 bitr3d ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
31 18 30 pm2.61dane ⊢ ( 𝜑 → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )