hlln

Description: The half-line relation implies colinearity, part of Theorem 6.4 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020)

	Ref	Expression
Hypotheses	ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hlln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	hlln.2	⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
Assertion	hlln	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5		ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6		ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7		hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		hlln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
9		hlln.2	⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
10		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
14	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )
16	1 10 2 11 12 13 14 15	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
17	16	3mix1d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
18	7	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐶 ∈ 𝑃 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
21	4	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
23	1 10 2 18 19 20 21 22	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
24	23	3mix2d	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
25	1 2 3 4 5 6 7	ishlg	⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
26	9 25	mpbid	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) )
27	26	simp3d	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )
28	17 24 27	mpjaodan	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
29	26	simp2d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
30	1 8 2 7 5 6 29 4	tgellng	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ↔ ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) ) )
31	28 30	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )

Metamath Proof Explorer

Theorem hlln

Proof