Metamath Proof Explorer


Theorem colperp

Description: Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019)

Ref Expression
Hypotheses colperpex.p 𝑃 = ( Base ‘ 𝐺 )
colperpex.d = ( dist ‘ 𝐺 )
colperpex.i 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ( 𝜑𝐺 ∈ TarskiG )
colperp.a ( 𝜑𝐴𝑃 )
colperp.b ( 𝜑𝐵𝑃 )
colperp.c ( 𝜑𝐶𝑃 )
colperp.1 ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
colperp.2 ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
colperp.3 ( 𝜑𝐴𝐶 )
Assertion colperp ( 𝜑 → ( 𝐴 𝐿 𝐶 ) ( ⟂G ‘ 𝐺 ) 𝐷 )

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 colperp.a ( 𝜑𝐴𝑃 )
7 colperp.b ( 𝜑𝐵𝑃 )
8 colperp.c ( 𝜑𝐶𝑃 )
9 colperp.1 ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
10 colperp.2 ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
11 colperp.3 ( 𝜑𝐴𝐶 )
12 4 5 9 perpln1 ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
13 1 3 4 5 6 7 12 tglnne ( 𝜑𝐴𝐵 )
14 1 3 4 5 6 7 13 tglinerflx1 ( 𝜑𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
15 13 neneqd ( 𝜑 → ¬ 𝐴 = 𝐵 )
16 10 orcomd ( 𝜑 → ( 𝐴 = 𝐵𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
17 16 ord ( 𝜑 → ( ¬ 𝐴 = 𝐵𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
18 15 17 mpd ( 𝜑𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
19 1 3 4 5 6 8 11 11 12 14 18 tglinethru ( 𝜑 → ( 𝐴 𝐿 𝐵 ) = ( 𝐴 𝐿 𝐶 ) )
20 19 9 eqbrtrrd ( 𝜑 → ( 𝐴 𝐿 𝐶 ) ( ⟂G ‘ 𝐺 ) 𝐷 )