Metamath Proof Explorer


Theorem tgbtwnconn1

Description: Connectivity law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019)

Ref Expression
Hypotheses tgbtwnconn1.p P = Base G
tgbtwnconn1.i I = Itv G
tgbtwnconn1.g φ G 𝒢 Tarski
tgbtwnconn1.a φ A P
tgbtwnconn1.b φ B P
tgbtwnconn1.c φ C P
tgbtwnconn1.d φ D P
tgbtwnconn1.1 φ A B
tgbtwnconn1.2 φ B A I C
tgbtwnconn1.3 φ B A I D
Assertion tgbtwnconn1 φ C A I D D A I C

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p P = Base G
2 tgbtwnconn1.i I = Itv G
3 tgbtwnconn1.g φ G 𝒢 Tarski
4 tgbtwnconn1.a φ A P
5 tgbtwnconn1.b φ B P
6 tgbtwnconn1.c φ C P
7 tgbtwnconn1.d φ D P
8 tgbtwnconn1.1 φ A B
9 tgbtwnconn1.2 φ B A I C
10 tgbtwnconn1.3 φ B A I D
11 simpllr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D A I e D dist G e = D dist G C
12 11 simpld φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D A I e
13 12 adantr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e D A I e
14 simpr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e C = e
15 14 oveq2d φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e A I C = A I e
16 13 15 eleqtrrd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e D A I C
17 16 olcd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e C A I D D A I C
18 simprl φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C A I f
19 18 adantr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D = f C A I f
20 simpr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D = f D = f
21 20 oveq2d φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D = f A I D = A I f
22 19 21 eleqtrrd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D = f C A I D
23 22 orcd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D = f C A I D D A I C
24 df-ne C e ¬ C = e
25 3 ad4antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D G 𝒢 Tarski
26 25 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f G 𝒢 Tarski
27 4 ad4antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D A P
28 27 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f A P
29 5 ad4antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D B P
30 29 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f B P
31 6 ad4antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C P
32 31 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f C P
33 7 ad4antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D P
34 33 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f D P
35 simp-11l φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f φ
36 35 8 syl φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f A B
37 35 9 syl φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f B A I C
38 35 10 syl φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f B A I D
39 eqid dist G = dist G
40 simp-4r φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D e P
41 40 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f e P
42 simplr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D f P
43 42 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f f P
44 simp-6r φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f h P
45 simp-4r φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f j P
46 12 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f D A I e
47 18 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f C A I f
48 simp-5r φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f e A I h e dist G h = B dist G C
49 48 simpld φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f e A I h
50 simpllr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f f A I j f dist G j = B dist G D
51 50 simpld φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f f A I j
52 11 simprd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D dist G e = D dist G C
53 52 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f D dist G e = D dist G C
54 1 39 2 26 34 41 34 32 53 tgcgrcomlr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f e dist G D = C dist G D
55 simprr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C dist G f = C dist G D
56 55 ad7antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f C dist G f = C dist G D
57 48 simprd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f e dist G h = B dist G C
58 50 simprd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f f dist G j = B dist G D
59 simplr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f x P
60 simprl φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f x C I e
61 simprr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f x D I f
62 simp-7r φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f C e
63 1 2 26 28 30 32 34 36 37 38 39 41 43 44 45 46 47 49 51 54 56 57 58 59 60 61 62 tgbtwnconn1lem3 φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f D = f
64 1 39 2 25 27 31 42 18 tgbtwncom φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C f I A
65 1 39 2 25 27 33 40 12 tgbtwncom φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D D e I A
66 1 39 2 25 42 40 27 31 33 64 65 axtgpasch φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D x P x C I e x D I f
67 66 ad5antr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D x P x C I e x D I f
68 63 67 r19.29a φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D D = f
69 1 39 2 25 27 42 29 33 axtgsegcon φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D j P f A I j f dist G j = B dist G D
70 69 ad3antrrr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C j P f A I j f dist G j = B dist G D
71 68 70 r19.29a φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C D = f
72 1 39 2 25 27 40 29 31 axtgsegcon φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D h P e A I h e dist G h = B dist G C
73 72 adantr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e h P e A I h e dist G h = B dist G C
74 71 73 r19.29a φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e D = f
75 74 ex φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C e D = f
76 24 75 syl5bir φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D ¬ C = e D = f
77 76 orrd φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C = e D = f
78 17 23 77 mpjaodan φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D C A I D D A I C
79 1 39 2 3 4 6 6 7 axtgsegcon φ f P C A I f C dist G f = C dist G D
80 79 ad2antrr φ e P D A I e D dist G e = D dist G C f P C A I f C dist G f = C dist G D
81 78 80 r19.29a φ e P D A I e D dist G e = D dist G C C A I D D A I C
82 1 39 2 3 4 7 7 6 axtgsegcon φ e P D A I e D dist G e = D dist G C
83 81 82 r19.29a φ C A I D D A I C