Metamath Proof Explorer

Theorem lnperpexs

Description: Existence of a perpendicular to a line L at a given point A . Theorem 10.15 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses lnperpexs.p ⊢ P = Base G
lnperpexs.l ⊢ L = Line 𝒢 ⁡ G
lnperpexs.g ⊢ φ → G ∈ 𝒢 Tarski
lnperpexs.h ⊢ φ → G Dim 𝒢 ≥ 2
lnperpexs.d ⊢ φ → D ∈ ran ⁡ L
lnperpexs.a ⊢ φ → A ∈ D
lnperpexs.q ⊢ φ → Q ∈ P
lnperpexs.1 ⊢ φ → ¬ Q ∈ D
Assertion lnperpexs ⊢ φ → ∃ p ∈ P D ⟂ 𝒢 ⁡ G p L A ∧ p hp 𝒢 ⁡ G ⁡ D Q

Proof

Step Hyp Ref Expression
1 lnperpexs.p ⊢ P = Base G
2 lnperpexs.l ⊢ L = Line 𝒢 ⁡ G
3 lnperpexs.g ⊢ φ → G ∈ 𝒢 Tarski
4 lnperpexs.h ⊢ φ → G Dim 𝒢 ≥ 2
5 lnperpexs.d ⊢ φ → D ∈ ran ⁡ L
6 lnperpexs.a ⊢ φ → A ∈ D
7 lnperpexs.q ⊢ φ → Q ∈ P
8 lnperpexs.1 ⊢ φ → ¬ Q ∈ D
9 eqid ⊢ dist ⁡ G = dist ⁡ G
10 eqid ⊢ Itv ⁡ G = Itv ⁡ G
11 eleq1w ⊢ a = c → a ∈ P ∖ D ↔ c ∈ P ∖ D
12 eleq1w ⊢ b = d → b ∈ P ∖ D ↔ d ∈ P ∖ D
13 11 12 bi2anan9 ⊢ a = c ∧ b = d → a ∈ P ∖ D ∧ b ∈ P ∖ D ↔ c ∈ P ∖ D ∧ d ∈ P ∖ D
14 oveq12 ⊢ a = c ∧ b = d → a Itv ⁡ G b = c Itv ⁡ G d
15 14 eleq2d ⊢ a = c ∧ b = d → s ∈ a Itv ⁡ G b ↔ s ∈ c Itv ⁡ G d
16 15 rexbidv ⊢ a = c ∧ b = d → ∃ s ∈ D s ∈ a Itv ⁡ G b ↔ ∃ s ∈ D s ∈ c Itv ⁡ G d
17 eleq1w ⊢ s = t → s ∈ c Itv ⁡ G d ↔ t ∈ c Itv ⁡ G d
18 17 cbvrexvw ⊢ ∃ s ∈ D s ∈ c Itv ⁡ G d ↔ ∃ t ∈ D t ∈ c Itv ⁡ G d
19 16 18 bitrdi ⊢ a = c ∧ b = d → ∃ s ∈ D s ∈ a Itv ⁡ G b ↔ ∃ t ∈ D t ∈ c Itv ⁡ G d
20 13 19 anbi12d ⊢ a = c ∧ b = d → a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ s ∈ D s ∈ a Itv ⁡ G b ↔ c ∈ P ∖ D ∧ d ∈ P ∖ D ∧ ∃ t ∈ D t ∈ c Itv ⁡ G d
21 20 cbvopabv ⊢ a b | a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ s ∈ D s ∈ a Itv ⁡ G b = c d | c ∈ P ∖ D ∧ d ∈ P ∖ D ∧ ∃ t ∈ D t ∈ c Itv ⁡ G d
22 1 9 10 2 3 4 5 21 6 7 8 lnperpex ⊢ φ → ∃ p ∈ P D ⟂ 𝒢 ⁡ G p L A ∧ p hp 𝒢 ⁡ G ⁡ D Q