Metamath Proof Explorer

Theorem perprag

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

Ref Expression
Hypotheses colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
perprag.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
perprag.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
perprag.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
perprag.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
perprag.5 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝐷 ) )
Assertion perprag ( 𝜑 → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∈ ( ∟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 perprag.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 perprag.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 perprag.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
9 perprag.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 perprag.5 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝐷 ) )
11 eqidd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝐴 = 𝐴 )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝐶 = 𝐷 )
13 eqidd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝐷 = 𝐷 )
14 11 12 13 s3eqd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → ⟨“ 𝐴 𝐶 𝐷 ”⟩ = ⟨“ 𝐴 𝐷 𝐷 ”⟩ )
15 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
16 1 2 3 4 15 5 6 9 9 ragtrivb ⊢ ( 𝜑 → ⟨“ 𝐴 𝐷 𝐷 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → ⟨“ 𝐴 𝐷 𝐷 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
18 14 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐺 ∈ TarskiG )
20 1 4 3 5 6 7 8 tglngne ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
21 1 3 4 5 6 7 20 tgelrnln ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
23 1 4 3 5 21 8 tglnpt ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ 𝑃 )
25 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐷 ∈ 𝑃 )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ≠ 𝐷 )
27 1 3 4 19 24 25 26 tgelrnln ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → ( 𝐶 𝐿 𝐷 ) ∈ ran 𝐿 )
28 8 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
29 1 3 4 19 24 25 26 tglinerflx1 ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ ( 𝐶 𝐿 𝐷 ) )
30 28 29 elind ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ∈ ( ( 𝐴 𝐿 𝐵 ) ∩ ( 𝐶 𝐿 𝐷 ) ) )
31 1 3 4 5 6 7 20 tglinerflx1 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
33 1 3 4 19 24 25 26 tglinerflx2 ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → 𝐷 ∈ ( 𝐶 𝐿 𝐷 ) )
34 10 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝐷 ) )
35 1 2 3 4 19 22 27 30 32 33 34 isperp2d ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝐷 ) → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
36 18 35 pm2.61dane ⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )