Theorem tgbtwnconnln3

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

	Ref	Expression
Hypotheses	tgbtwnconn.p	|- P = ( Base ` G )
	tgbtwnconn.i	|- I = ( Itv ` G )
	tgbtwnconn.g	|- ( ph -> G e. TarskiG )
	tgbtwnconn.a	|- ( ph -> A e. P )
	tgbtwnconn.b	|- ( ph -> B e. P )
	tgbtwnconn.c	|- ( ph -> C e. P )
	tgbtwnconn.d	|- ( ph -> D e. P )
	tgbtwnconn3.1	|- ( ph -> B e. ( A I D ) )
	tgbtwnconn3.2	|- ( ph -> C e. ( A I D ) )
	tgbtwnconnln3.l	|- L = ( LineG ` G )
Assertion	tgbtwnconnln3	|- ( ph -> ( B e. ( A L C ) \/ A = C ) )

Proof

Step	Hyp	Ref	Expression
1		tgbtwnconn.p	|- P = ( Base ` G )
2		tgbtwnconn.i	|- I = ( Itv ` G )
3		tgbtwnconn.g	|- ( ph -> G e. TarskiG )
4		tgbtwnconn.a	|- ( ph -> A e. P )
5		tgbtwnconn.b	|- ( ph -> B e. P )
6		tgbtwnconn.c	|- ( ph -> C e. P )
7		tgbtwnconn.d	|- ( ph -> D e. P )
8		tgbtwnconn3.1	|- ( ph -> B e. ( A I D ) )
9		tgbtwnconn3.2	|- ( ph -> C e. ( A I D ) )
10		tgbtwnconnln3.l	|- L = ( LineG ` G )
11	3	adantr	|- ( ( ph /\ B e. ( A I C ) ) -> G e. TarskiG )
12	4	adantr	|- ( ( ph /\ B e. ( A I C ) ) -> A e. P )
13	6	adantr	|- ( ( ph /\ B e. ( A I C ) ) -> C e. P )
14	5	adantr	|- ( ( ph /\ B e. ( A I C ) ) -> B e. P )
15		simpr	|- ( ( ph /\ B e. ( A I C ) ) -> B e. ( A I C ) )
16	1 10 2 11 12 13 14 15	btwncolg1	|- ( ( ph /\ B e. ( A I C ) ) -> ( B e. ( A L C ) \/ A = C ) )
17	3	adantr	|- ( ( ph /\ C e. ( A I B ) ) -> G e. TarskiG )
18	4	adantr	|- ( ( ph /\ C e. ( A I B ) ) -> A e. P )
19	6	adantr	|- ( ( ph /\ C e. ( A I B ) ) -> C e. P )
20	5	adantr	|- ( ( ph /\ C e. ( A I B ) ) -> B e. P )
21		simpr	|- ( ( ph /\ C e. ( A I B ) ) -> C e. ( A I B ) )
22	1 10 2 17 18 19 20 21	btwncolg3	|- ( ( ph /\ C e. ( A I B ) ) -> ( B e. ( A L C ) \/ A = C ) )
23	1 2 3 4 5 6 7 8 9	tgbtwnconn3	|- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
24	16 22 23	mpjaodan	|- ( ph -> ( B e. ( A L C ) \/ A = C ) )