Metamath Proof Explorer


Theorem tgbtwnconnln2

Description: Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tgbtwnconn.p 𝑃 = ( Base ‘ 𝐺 )
tgbtwnconn.i 𝐼 = ( Itv ‘ 𝐺 )
tgbtwnconn.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnconn.a ( 𝜑𝐴𝑃 )
tgbtwnconn.b ( 𝜑𝐵𝑃 )
tgbtwnconn.c ( 𝜑𝐶𝑃 )
tgbtwnconn.d ( 𝜑𝐷𝑃 )
tgbtwnconnln1.l 𝐿 = ( LineG ‘ 𝐺 )
tgbtwnconnln1.1 ( 𝜑𝐴𝐵 )
tgbtwnconnln1.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnconnln1.3 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnconnln2 ( 𝜑 → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwnconn.i 𝐼 = ( Itv ‘ 𝐺 )
3 tgbtwnconn.g ( 𝜑𝐺 ∈ TarskiG )
4 tgbtwnconn.a ( 𝜑𝐴𝑃 )
5 tgbtwnconn.b ( 𝜑𝐵𝑃 )
6 tgbtwnconn.c ( 𝜑𝐶𝑃 )
7 tgbtwnconn.d ( 𝜑𝐷𝑃 )
8 tgbtwnconnln1.l 𝐿 = ( LineG ‘ 𝐺 )
9 tgbtwnconnln1.1 ( 𝜑𝐴𝐵 )
10 tgbtwnconnln1.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
11 tgbtwnconnln1.3 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
12 3 adantr ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐺 ∈ TarskiG )
13 6 adantr ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐶𝑃 )
14 7 adantr ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐷𝑃 )
15 5 adantr ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐵𝑃 )
16 simpr ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
17 1 8 2 12 13 14 15 16 btwncolg2 ( ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
18 3 adantr ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
19 6 adantr ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐶𝑃 )
20 7 adantr ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐷𝑃 )
21 5 adantr ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐵𝑃 )
22 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
23 simpr ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )
24 1 22 2 18 21 20 19 23 tgbtwncom ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐷 ∈ ( 𝐶 𝐼 𝐵 ) )
25 1 8 2 18 19 20 21 24 btwncolg3 ( ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
26 1 2 3 4 5 6 7 9 10 11 tgbtwnconn2 ( 𝜑 → ( 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) )
27 17 25 26 mpjaodan ( 𝜑 → ( 𝐵 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )