Theorem hlopp

Description: If two points X and Y lie on opposite sides of a line A , then given a point Z on A , any point W on the line ( X L Z ) opposite to Y lies on the half line ( Z X ) (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	hlopp.p	|- P = ( Base ` G )
	hlopp.i	|- I = ( Itv ` G )
	hlopp.l	|- L = ( LineG ` G )
	hlopp.o	|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
	hlopp.k	|- K = ( hlG ` G )
	hlopp.g	|- ( ph -> G e. TarskiG )
	hlopp.a	|- ( ph -> A e. ran L )
	hlopp.x	|- ( ph -> X e. P )
	hlopp.y	|- ( ph -> Y e. P )
	hlopp.1	|- ( ph -> X O Y )
	hlopp.2	|- ( ph -> Z e. A )
	hlopp.3	|- ( ph -> W O Y )
	hlopp.4	|- ( ph -> W e. ( X L Z ) )
Assertion	hlopp	|- ( ph -> W ( K ` Z ) X )

Proof

Step	Hyp	Ref	Expression
1		hlopp.p	|- P = ( Base ` G )
2		hlopp.i	|- I = ( Itv ` G )
3		hlopp.l	|- L = ( LineG ` G )
4		hlopp.o	|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
5		hlopp.k	|- K = ( hlG ` G )
6		hlopp.g	|- ( ph -> G e. TarskiG )
7		hlopp.a	|- ( ph -> A e. ran L )
8		hlopp.x	|- ( ph -> X e. P )
9		hlopp.y	|- ( ph -> Y e. P )
10		hlopp.1	|- ( ph -> X O Y )
11		hlopp.2	|- ( ph -> Z e. A )
12		hlopp.3	|- ( ph -> W O Y )
13		hlopp.4	|- ( ph -> W e. ( X L Z ) )
14	1 3 2 6 7 11	tglnpt	|- ( ph -> Z e. P )
15	1 3 2 6 8 14 13	tglngne	|- ( ph -> X =/= Z )
16	1 2 3 6 8 14 15	tgelrnln	|- ( ph -> ( X L Z ) e. ran L )
17	1 3 2 6 16 13	tglnpt	|- ( ph -> W e. P )
18	1 2 3 4 6 7 17 8 9 12	lnopp2hpgb	|- ( ph -> ( X O Y <-> W ( ( hpG ` G ) ` A ) X ) )
19	10 18	mpbid	|- ( ph -> W ( ( hpG ` G ) ` A ) X )
20	13	orcd	|- ( ph -> ( W e. ( X L Z ) \/ X = Z ) )
21	1 3 2 6 8 14 17 20	colrot2	|- ( ph -> ( Z e. ( W L X ) \/ W = X ) )
22	1 2 3 6 7 17 4 8 11 21 5	colhp	|- ( ph -> ( W ( ( hpG ` G ) ` A ) X <-> ( W ( K ` Z ) X /\ -. W e. A ) ) )
23	19 22	mpbid	|- ( ph -> ( W ( K ` Z ) X /\ -. W e. A ) )
24	23	simpld	|- ( ph -> W ( K ` Z ) X )