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	$⊢ P = {Base}_{G}$
	ishlg.i	$⊢ I = Itv (G)$
	ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
	ishlg.a	$⊢ φ \to A \in P$
	ishlg.b	$⊢ φ \to B \in P$
	ishlg.c	$⊢ φ \to C \in P$
	hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	hlln.l	$⊢ L = {Line}_{𝒢} (G)$
	hlln.2	$⊢ φ \to A K (C) B$
Assertion	hlln	$⊢ φ \to A \in (B L C)$

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	$⊢ P = {Base}_{G}$
2		ishlg.i	$⊢ I = Itv (G)$
3		ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
4		ishlg.a	$⊢ φ \to A \in P$
5		ishlg.b	$⊢ φ \to B \in P$
6		ishlg.c	$⊢ φ \to C \in P$
7		hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
8		hlln.l	$⊢ L = {Line}_{𝒢} (G)$
9		hlln.2	$⊢ φ \to A K (C) B$
10		eqid	$⊢ dist (G) = dist (G)$
11	7	adantr	$⊢ (φ \land A \in (C I B)) \to G \in 𝒢_{Tarski}$
12	6	adantr	$⊢ (φ \land A \in (C I B)) \to C \in P$
13	4	adantr	$⊢ (φ \land A \in (C I B)) \to A \in P$
14	5	adantr	$⊢ (φ \land A \in (C I B)) \to B \in P$
15		simpr	$⊢ (φ \land A \in (C I B)) \to A \in (C I B)$
16	1 10 2 11 12 13 14 15	tgbtwncom	$⊢ (φ \land A \in (C I B)) \to A \in (B I C)$
17	16	3mix1d	$⊢ (φ \land A \in (C I B)) \to (A \in (B I C) \lor B \in (A I C) \lor C \in (B I A))$
18	7	adantr	$⊢ (φ \land B \in (C I A)) \to G \in 𝒢_{Tarski}$
19	6	adantr	$⊢ (φ \land B \in (C I A)) \to C \in P$
20	5	adantr	$⊢ (φ \land B \in (C I A)) \to B \in P$
21	4	adantr	$⊢ (φ \land B \in (C I A)) \to A \in P$
22		simpr	$⊢ (φ \land B \in (C I A)) \to B \in (C I A)$
23	1 10 2 18 19 20 21 22	tgbtwncom	$⊢ (φ \land B \in (C I A)) \to B \in (A I C)$
24	23	3mix2d	$⊢ (φ \land B \in (C I A)) \to (A \in (B I C) \lor B \in (A I C) \lor C \in (B I A))$
25	1 2 3 4 5 6 7	ishlg	$⊢ φ \to (A K (C) B \leftrightarrow (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))))$
26	9 25	mpbid	$⊢ φ \to (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A)))$
27	26	simp3d	$⊢ φ \to (A \in (C I B) \lor B \in (C I A))$
28	17 24 27	mpjaodan	$⊢ φ \to (A \in (B I C) \lor B \in (A I C) \lor C \in (B I A))$
29	26	simp2d	$⊢ φ \to B \neq C$
30	1 8 2 7 5 6 29 4	tgellng	$⊢ φ \to (A \in (B L C) \leftrightarrow (A \in (B I C) \lor B \in (A I C) \lor C \in (B I A)))$
31	28 30	mpbird	$⊢ φ \to A \in (B L C)$

Metamath Proof Explorer

Theorem hlln

Proof