Metamath Proof Explorer

Theorem footeq

Description: Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020)

Ref Expression
Hypotheses isperp.p ⊢ P = Base G
isperp.d ⊢ - ˙ = dist ⁡ G
isperp.i ⊢ I = Itv ⁡ G
isperp.l ⊢ L = Line 𝒢 ⁡ G
isperp.g ⊢ φ → G ∈ 𝒢 Tarski
isperp.a ⊢ φ → A ∈ ran ⁡ L
footeq.x ⊢ φ → X ∈ A
footeq.y ⊢ φ → Y ∈ A
footeq.z ⊢ φ → Z ∈ P
footeq.1 ⊢ φ → X L Z ⟂ 𝒢 ⁡ G A
footeq.2 ⊢ φ → Y L Z ⟂ 𝒢 ⁡ G A
Assertion footeq ⊢ φ → X = Y

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ P = Base G
2 isperp.d ⊢ - ˙ = dist ⁡ G
3 isperp.i ⊢ I = Itv ⁡ G
4 isperp.l ⊢ L = Line 𝒢 ⁡ G
5 isperp.g ⊢ φ → G ∈ 𝒢 Tarski
6 isperp.a ⊢ φ → A ∈ ran ⁡ L
7 footeq.x ⊢ φ → X ∈ A
8 footeq.y ⊢ φ → Y ∈ A
9 footeq.z ⊢ φ → Z ∈ P
10 footeq.1 ⊢ φ → X L Z ⟂ 𝒢 ⁡ G A
11 footeq.2 ⊢ φ → Y L Z ⟂ 𝒢 ⁡ G A
12 oveq2 ⊢ x = X → Z L x = Z L X
13 12 breq1d ⊢ x = X → Z L x ⟂ 𝒢 ⁡ G A ↔ Z L X ⟂ 𝒢 ⁡ G A
14 oveq2 ⊢ x = Y → Z L x = Z L Y
15 14 breq1d ⊢ x = Y → Z L x ⟂ 𝒢 ⁡ G A ↔ Z L Y ⟂ 𝒢 ⁡ G A
16 1 2 3 4 5 6 7 9 10 footne ⊢ φ → ¬ Z ∈ A
17 1 2 3 4 5 6 9 16 foot ⊢ φ → ∃! x ∈ A Z L x ⟂ 𝒢 ⁡ G A
18 1 4 3 5 6 7 tglnpt ⊢ φ → X ∈ P
19 4 5 10 perpln1 ⊢ φ → X L Z ∈ ran ⁡ L
20 1 3 4 5 18 9 19 tglnne ⊢ φ → X ≠ Z
21 1 3 4 5 18 9 20 tglinecom ⊢ φ → X L Z = Z L X
22 21 10 eqbrtrrd ⊢ φ → Z L X ⟂ 𝒢 ⁡ G A
23 1 4 3 5 6 8 tglnpt ⊢ φ → Y ∈ P
24 4 5 11 perpln1 ⊢ φ → Y L Z ∈ ran ⁡ L
25 1 3 4 5 23 9 24 tglnne ⊢ φ → Y ≠ Z
26 1 3 4 5 23 9 25 tglinecom ⊢ φ → Y L Z = Z L Y
27 26 11 eqbrtrrd ⊢ φ → Z L Y ⟂ 𝒢 ⁡ G A
28 13 15 17 7 8 22 27 reu2eqd ⊢ φ → X = Y