Theorem hlperpnel

Description: A point on a half-line which is perpendicular to a line cannot be on that line. (Contributed by Thierry Arnoux, 1-Mar-2020)

	Ref	Expression
Hypotheses	colperpex.p	|- P = ( Base ` G )
	colperpex.d	|- .- = ( dist ` G )
	colperpex.i	|- I = ( Itv ` G )
	colperpex.l	|- L = ( LineG ` G )
	colperpex.g	|- ( ph -> G e. TarskiG )
	hlperpnel.a	|- ( ph -> A e. ran L )
	hlperpnel.k	|- K = ( hlG ` G )
	hlperpnel.1	|- ( ph -> U e. A )
	hlperpnel.2	|- ( ph -> V e. P )
	hlperpnel.3	|- ( ph -> W e. P )
	hlperpnel.4	|- ( ph -> A ( perpG ` G ) ( U L V ) )
	hlperpnel.5	|- ( ph -> V ( K ` U ) W )
Assertion	hlperpnel	|- ( ph -> -. W e. A )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	|- P = ( Base ` G )
2		colperpex.d	|- .- = ( dist ` G )
3		colperpex.i	|- I = ( Itv ` G )
4		colperpex.l	|- L = ( LineG ` G )
5		colperpex.g	|- ( ph -> G e. TarskiG )
6		hlperpnel.a	|- ( ph -> A e. ran L )
7		hlperpnel.k	|- K = ( hlG ` G )
8		hlperpnel.1	|- ( ph -> U e. A )
9		hlperpnel.2	|- ( ph -> V e. P )
10		hlperpnel.3	|- ( ph -> W e. P )
11		hlperpnel.4	|- ( ph -> A ( perpG ` G ) ( U L V ) )
12		hlperpnel.5	|- ( ph -> V ( K ` U ) W )
13	1 4 3 5 6 8	tglnpt	|- ( ph -> U e. P )
14	4 5 11	perpln2	|- ( ph -> ( U L V ) e. ran L )
15	1 3 4 5 13 9 14	tglnne	|- ( ph -> U =/= V )
16	1 3 7 9 10 13 5 12	hlne2	|- ( ph -> W =/= U )
17	1 3 7 9 10 13 5 4 12	hlln	|- ( ph -> V e. ( W L U ) )
18	1 3 4 5 13 9 10 15 17 16	lnrot1	|- ( ph -> W e. ( U L V ) )
19	1 3 4 5 13 9 15 10 16 18	tglineelsb2	|- ( ph -> ( U L V ) = ( U L W ) )
20	1 2 3 4 5 6 14 11	perpcom	|- ( ph -> ( U L V ) ( perpG ` G ) A )
21	19 20	eqbrtrrd	|- ( ph -> ( U L W ) ( perpG ` G ) A )
22	1 2 3 4 5 6 8 10 21	footne	|- ( ph -> -. W e. A )