Metamath Proof Explorer


Theorem tgbtwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (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 ( 𝜑𝐷𝑃 )
tgbtwnconn3.1 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
tgbtwnconn3.2 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnconn3 ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )

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 tgbtwnconn3.1 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
9 tgbtwnconn3.2 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
10 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11 3 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
12 5 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵𝑃 )
13 4 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴𝑃 )
14 6 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐶𝑃 )
15 simpr ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
16 1 10 2 11 12 13 14 15 tgldim0itv ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
17 16 orcd ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
18 3 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐺 ∈ TarskiG )
19 simplr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝑝𝑃 )
20 4 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴𝑃 )
21 5 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐵𝑃 )
22 6 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐶𝑃 )
23 simprr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴𝑝 )
24 23 necomd ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝑝𝐴 )
25 7 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐷𝑃 )
26 8 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
27 simprl ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) )
28 1 10 2 18 25 20 19 27 tgbtwncom ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐷 ) )
29 1 10 2 18 21 20 19 25 26 28 tgbtwnintr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑝 ) )
30 1 10 2 18 21 20 19 29 tgbtwncom ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐵 ) )
31 9 ad3antrrr ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
32 1 10 2 18 20 22 25 31 tgbtwncom ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
33 1 10 2 18 25 22 20 19 32 27 tgbtwnexch3 ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
34 1 10 2 18 22 20 19 33 tgbtwncom ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐶 ) )
35 1 2 18 19 20 21 22 24 30 34 tgbtwnconn2 ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
36 3 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐺 ∈ TarskiG )
37 7 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐷𝑃 )
38 4 adantr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐴𝑃 )
39 simpr ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
40 1 10 2 36 37 38 39 tgbtwndiff ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑝𝑃 ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴𝑝 ) )
41 35 40 r19.29a ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
42 1 4 tgldimor ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
43 17 41 42 mpjaodan ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )