Metamath Proof Explorer


Theorem btwnhl

Description: Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020)

Ref Expression
Hypotheses ishlg.p P=BaseG
ishlg.i I=ItvG
ishlg.k K=hl𝒢G
ishlg.a φAP
ishlg.b φBP
ishlg.c φCP
hlln.1 φG𝒢Tarski
hltr.d φDP
btwnhl.1 φAKDB
btwnhl.3 φDAIC
Assertion btwnhl φDBIC

Proof

Step Hyp Ref Expression
1 ishlg.p P=BaseG
2 ishlg.i I=ItvG
3 ishlg.k K=hl𝒢G
4 ishlg.a φAP
5 ishlg.b φBP
6 ishlg.c φCP
7 hlln.1 φG𝒢Tarski
8 hltr.d φDP
9 btwnhl.1 φAKDB
10 btwnhl.3 φDAIC
11 eqid distG=distG
12 7 adantr φADIBG𝒢Tarski
13 6 adantr φADIBCP
14 8 adantr φADIBDP
15 5 adantr φADIBBP
16 4 adantr φADIBAP
17 1 2 3 4 5 8 7 ishlg φAKDBADBDADIBBDIA
18 9 17 mpbid φADBDADIBBDIA
19 18 simp1d φAD
20 19 necomd φDA
21 20 adantr φADIBDA
22 10 adantr φADIBDAIC
23 1 11 2 12 16 14 13 22 tgbtwncom φADIBDCIA
24 simpr φADIBADIB
25 1 11 2 12 13 14 16 15 21 23 24 tgbtwnouttr φADIBDCIB
26 1 11 2 12 13 14 15 25 tgbtwncom φADIBDBIC
27 7 adantr φBDIAG𝒢Tarski
28 4 adantr φBDIAAP
29 5 adantr φBDIABP
30 8 adantr φBDIADP
31 6 adantr φBDIACP
32 simpr φBDIABDIA
33 1 11 2 27 30 29 28 32 tgbtwncom φBDIABAID
34 10 adantr φBDIADAIC
35 1 11 2 27 28 29 30 31 33 34 tgbtwnexch3 φBDIADBIC
36 18 simp3d φADIBBDIA
37 26 35 36 mpjaodan φDBIC