tgbtwnconnln3

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	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgbtwnconn3.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
	tgbtwnconn3.2	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
	tgbtwnconnln3.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
Assertion	tgbtwnconnln3	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )

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		tgbtwnconnln3.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
14	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
16	1 10 2 11 12 13 14 15	btwncolg1	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
17	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
18	4	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
22	1 10 2 17 18 19 20 21	btwncolg3	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
23	1 2 3 4 5 6 7 8 9	tgbtwnconn3	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
24	16 22 23	mpjaodan	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )

Metamath Proof Explorer

Theorem tgbtwnconnln3

Proof