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={\mathrm{Base}}_G$$
	colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	hlperpnel.a	$$⊢\phi \to A\in \mathrm{ran}L$$
	hlperpnel.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	hlperpnel.1	$$⊢\phi \to U\in A$$
	hlperpnel.2	$$⊢\phi \to V\in P$$
	hlperpnel.3	$$⊢\phi \to W\in P$$
	hlperpnel.4	$$⊢\phi \to A{⟂}_{𝒢}\left(G\right)\left(ULV\right)$$
	hlperpnel.5	$$⊢\phi \to VK\left(U\right)W$$
Assertion	hlperpnel	$$⊢\phi \to \neg W\in A$$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$$⊢P={\mathrm{Base}}_G$$
2		colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		hlperpnel.a	$$⊢\phi \to A\in \mathrm{ran}L$$
7		hlperpnel.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
8		hlperpnel.1	$$⊢\phi \to U\in A$$
9		hlperpnel.2	$$⊢\phi \to V\in P$$
10		hlperpnel.3	$$⊢\phi \to W\in P$$
11		hlperpnel.4	$$⊢\phi \to A{⟂}_{𝒢}\left(G\right)\left(ULV\right)$$
12		hlperpnel.5	$$⊢\phi \to VK\left(U\right)W$$
13	1 4 3 5 6 8	tglnpt	$$⊢\phi \to U\in P$$
14	4 5 11	perpln2	$$⊢\phi \to ULV\in \mathrm{ran}L$$
15	1 3 4 5 13 9 14	tglnne	$$⊢\phi \to U\ne V$$
16	1 3 7 9 10 13 5 12	hlne2	$$⊢\phi \to W\ne U$$
17	1 3 7 9 10 13 5 4 12	hlln	$$⊢\phi \to V\in \left(WLU\right)$$
18	1 3 4 5 13 9 10 15 17 16	lnrot1	$$⊢\phi \to W\in \left(ULV\right)$$
19	1 3 4 5 13 9 15 10 16 18	tglineelsb2	$$⊢\phi \to ULV=ULW$$
20	1 2 3 4 5 6 14 11	perpcom	$$⊢\phi \to \left(ULV\right){⟂}_{𝒢}\left(G\right)A$$
21	19 20	eqbrtrrd	$$⊢\phi \to \left(ULW\right){⟂}_{𝒢}\left(G\right)A$$
22	1 2 3 4 5 6 8 10 21	footne	$$⊢\phi \to \neg W\in A$$