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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	colperpex.d	⊢ − = ( dist ‘ 𝐺 )
	colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hlperpnel.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	hlperpnel.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	hlperpnel.1	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
	hlperpnel.2	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	hlperpnel.3	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	hlperpnel.4	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) ( 𝑈 𝐿 𝑉 ) )
	hlperpnel.5	⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑈 ) 𝑊 )
Assertion	hlperpnel	⊢ ( 𝜑 → ¬ 𝑊 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		colperpex.d	⊢ − = ( dist ‘ 𝐺 )
3		colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		hlperpnel.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7		hlperpnel.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
8		hlperpnel.1	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
9		hlperpnel.2	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10		hlperpnel.3	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11		hlperpnel.4	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) ( 𝑈 𝐿 𝑉 ) )
12		hlperpnel.5	⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑈 ) 𝑊 )
13	1 4 3 5 6 8	tglnpt	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
14	4 5 11	perpln2	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) ∈ ran 𝐿 )
15	1 3 4 5 13 9 14	tglnne	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
16	1 3 7 9 10 13 5 12	hlne2	⊢ ( 𝜑 → 𝑊 ≠ 𝑈 )
17	1 3 7 9 10 13 5 4 12	hlln	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑊 𝐿 𝑈 ) )
18	1 3 4 5 13 9 10 15 17 16	lnrot1	⊢ ( 𝜑 → 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) )
19	1 3 4 5 13 9 15 10 16 18	tglineelsb2	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) = ( 𝑈 𝐿 𝑊 ) )
20	1 2 3 4 5 6 14 11	perpcom	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
21	19 20	eqbrtrrd	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑊 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
22	1 2 3 4 5 6 8 10 21	footne	⊢ ( 𝜑 → ¬ 𝑊 ∈ 𝐴 )