Metamath Proof Explorer


Theorem foot

Description: From a point C outside of a line A , there exists a unique point x on A such that ( C L x ) is perpendicular to A . That point is called the foot from C on A . Theorem 8.18 of Schwabhauser p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019)

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
foot.x φ C P
foot.y φ ¬ C A
Assertion foot φ ∃! x A C L x 𝒢 G A

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 foot.x φ C P
8 foot.y φ ¬ C A
9 1 2 3 4 5 6 7 8 footex φ x A C L x 𝒢 G A
10 eqid pInv 𝒢 G = pInv 𝒢 G
11 5 ad2antrr φ x A z A C L x 𝒢 G A C L z 𝒢 G A G 𝒢 Tarski
12 7 ad2antrr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C P
13 5 adantr φ x A z A G 𝒢 Tarski
14 6 adantr φ x A z A A ran L
15 simprl φ x A z A x A
16 1 4 3 13 14 15 tglnpt φ x A z A x P
17 16 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A x P
18 simprr φ x A z A z A
19 1 4 3 13 14 18 tglnpt φ x A z A z P
20 19 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A z P
21 8 adantr φ x A z A ¬ C A
22 nelne2 x A ¬ C A x C
23 15 21 22 syl2anc φ x A z A x C
24 23 necomd φ x A z A C x
25 24 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C x
26 1 3 4 11 12 17 25 tglinerflx1 φ x A z A C L x 𝒢 G A C L z 𝒢 G A C C L x
27 18 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A z A
28 simprl φ x A z A C L x 𝒢 G A C L z 𝒢 G A C L x 𝒢 G A
29 7 adantr φ x A z A C P
30 1 3 4 13 29 16 24 tgelrnln φ x A z A C L x ran L
31 1 3 4 13 29 16 24 tglinerflx2 φ x A z A x C L x
32 31 15 elind φ x A z A x C L x A
33 1 2 3 4 13 30 14 32 isperp2 φ x A z A C L x 𝒢 G A u C L x v A ⟨“ uxv ”⟩ 𝒢 G
34 33 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C L x 𝒢 G A u C L x v A ⟨“ uxv ”⟩ 𝒢 G
35 28 34 mpbid φ x A z A C L x 𝒢 G A C L z 𝒢 G A u C L x v A ⟨“ uxv ”⟩ 𝒢 G
36 id u = C u = C
37 eqidd u = C x = x
38 eqidd u = C v = v
39 36 37 38 s3eqd u = C ⟨“ uxv ”⟩ = ⟨“ Cxv ”⟩
40 39 eleq1d u = C ⟨“ uxv ”⟩ 𝒢 G ⟨“ Cxv ”⟩ 𝒢 G
41 eqidd v = z C = C
42 eqidd v = z x = x
43 id v = z v = z
44 41 42 43 s3eqd v = z ⟨“ Cxv ”⟩ = ⟨“ Cxz ”⟩
45 44 eleq1d v = z ⟨“ Cxv ”⟩ 𝒢 G ⟨“ Cxz ”⟩ 𝒢 G
46 40 45 rspc2va C C L x z A u C L x v A ⟨“ uxv ”⟩ 𝒢 G ⟨“ Cxz ”⟩ 𝒢 G
47 26 27 35 46 syl21anc φ x A z A C L x 𝒢 G A C L z 𝒢 G A ⟨“ Cxz ”⟩ 𝒢 G
48 nelne2 z A ¬ C A z C
49 18 21 48 syl2anc φ x A z A z C
50 49 necomd φ x A z A C z
51 50 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C z
52 1 3 4 11 12 20 51 tglinerflx1 φ x A z A C L x 𝒢 G A C L z 𝒢 G A C C L z
53 15 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A x A
54 simprr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C L z 𝒢 G A
55 1 3 4 13 29 19 50 tgelrnln φ x A z A C L z ran L
56 1 3 4 13 29 19 50 tglinerflx2 φ x A z A z C L z
57 56 18 elind φ x A z A z C L z A
58 1 2 3 4 13 55 14 57 isperp2 φ x A z A C L z 𝒢 G A u C L z v A ⟨“ uzv ”⟩ 𝒢 G
59 58 adantr φ x A z A C L x 𝒢 G A C L z 𝒢 G A C L z 𝒢 G A u C L z v A ⟨“ uzv ”⟩ 𝒢 G
60 54 59 mpbid φ x A z A C L x 𝒢 G A C L z 𝒢 G A u C L z v A ⟨“ uzv ”⟩ 𝒢 G
61 eqidd u = C z = z
62 36 61 38 s3eqd u = C ⟨“ uzv ”⟩ = ⟨“ Czv ”⟩
63 62 eleq1d u = C ⟨“ uzv ”⟩ 𝒢 G ⟨“ Czv ”⟩ 𝒢 G
64 eqidd v = x C = C
65 eqidd v = x z = z
66 id v = x v = x
67 64 65 66 s3eqd v = x ⟨“ Czv ”⟩ = ⟨“ Czx ”⟩
68 67 eleq1d v = x ⟨“ Czv ”⟩ 𝒢 G ⟨“ Czx ”⟩ 𝒢 G
69 63 68 rspc2va C C L z x A u C L z v A ⟨“ uzv ”⟩ 𝒢 G ⟨“ Czx ”⟩ 𝒢 G
70 52 53 60 69 syl21anc φ x A z A C L x 𝒢 G A C L z 𝒢 G A ⟨“ Czx ”⟩ 𝒢 G
71 1 2 3 4 10 11 12 17 20 47 70 ragflat φ x A z A C L x 𝒢 G A C L z 𝒢 G A x = z
72 71 ex φ x A z A C L x 𝒢 G A C L z 𝒢 G A x = z
73 72 ralrimivva φ x A z A C L x 𝒢 G A C L z 𝒢 G A x = z
74 oveq2 x = z C L x = C L z
75 74 breq1d x = z C L x 𝒢 G A C L z 𝒢 G A
76 75 rmo4 * x A C L x 𝒢 G A x A z A C L x 𝒢 G A C L z 𝒢 G A x = z
77 73 76 sylibr φ * x A C L x 𝒢 G A
78 reu5 ∃! x A C L x 𝒢 G A x A C L x 𝒢 G A * x A C L x 𝒢 G A
79 9 77 78 sylanbrc φ ∃! x A C L x 𝒢 G A