Metamath Proof Explorer


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 ( 𝜑 → ¬ 𝑊𝐴 )