Metamath Proof Explorer


Theorem perpdrag

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019)

Ref Expression
Hypotheses colperpex.p 𝑃 = ( Base ‘ 𝐺 )
colperpex.d = ( dist ‘ 𝐺 )
colperpex.i 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ( 𝜑𝐺 ∈ TarskiG )
perpdrag.1 ( 𝜑𝐴𝐷 )
perpdrag.2 ( 𝜑𝐵𝐷 )
perpdrag.3 ( 𝜑𝐶𝑃 )
perpdrag.4 ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
Assertion perpdrag ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟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 perpdrag.1 ( 𝜑𝐴𝐷 )
7 perpdrag.2 ( 𝜑𝐵𝐷 )
8 perpdrag.3 ( 𝜑𝐶𝑃 )
9 perpdrag.4 ( 𝜑𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
10 5 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐺 ∈ TarskiG )
11 9 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
12 4 10 11 perpln1 ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐷 ∈ ran 𝐿 )
13 6 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐴𝐷 )
14 1 4 3 10 12 13 tglnpt ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐴𝑃 )
15 simplr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝑥𝐷 )
16 1 4 3 10 12 15 tglnpt ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝑥𝑃 )
17 7 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐵𝐷 )
18 simpr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐴𝑥 )
19 1 3 4 10 14 16 18 18 12 13 15 tglinethru ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐷 = ( 𝐴 𝐿 𝑥 ) )
20 17 19 eleqtrd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐵 ∈ ( 𝐴 𝐿 𝑥 ) )
21 8 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → 𝐶𝑃 )
22 19 11 eqbrtrrd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
23 1 2 3 4 10 14 16 20 21 22 perprag ( ( ( 𝜑𝑥𝐷 ) ∧ 𝐴𝑥 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
24 4 5 9 perpln1 ( 𝜑𝐷 ∈ ran 𝐿 )
25 1 3 4 5 24 6 tglnpt2 ( 𝜑 → ∃ 𝑥𝐷 𝐴𝑥 )
26 23 25 r19.29a ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )