Theorem lnhl

Description: Either a point C on the line AB is on the same side as A or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-2020)

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

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		hltr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		lnhl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
10		lnhl.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → 𝐶 = 𝐵 )
12		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
13	1 12 2 7 4 6	tgbtwntriv2	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐶 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ ( 𝐴 𝐼 𝐶 ) )
15	11 14	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
16	15	olcd	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
17	1 9 2 7 4 5 10	tglngne	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
18	1 9 2 7 4 5 17 6	tgellng	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
19	10 18	mpbid	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
20		df-3or	⊢ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ↔ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
21	19 20	sylib	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
23	1 2 3 6 4 5 7	ishlg	⊢ ( 𝜑 → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
25		df-3an	⊢ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ↔ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
26	24 25	bitrdi	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
27	17	anim1ci	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
28	27	biantrurd	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ↔ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
29	7	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
30	5	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
31	6	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → 𝐶 ∈ 𝑃 )
32	4	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
33	1 12 2 29 30 31 32	tgbtwncomb	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ↔ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
34	1 12 2 29 30 32 31	tgbtwncomb	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ↔ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) )
35	33 34	orbi12d	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) )
36	26 28 35	3bitr2d	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) )
37	36	orbi1d	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ↔ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
38	22 37	mpbird	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐵 ) → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
39	16 38	pm2.61dane	⊢ ( 𝜑 → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )