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 = ( LineG ` G )
isperp.g 
|- ( ph -> G e. TarskiG )
isperp.a 
|- ( ph -> A e. ran L )
foot.x 
|- ( ph -> C e. P )
foot.y 
|- ( ph -> -. C e. A )
Assertion foot 
|- ( ph -> E! x e. A ( C L x ) ( perpG ` 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 = ( LineG ` G )
5 isperp.g 
 |-  ( ph -> G e. TarskiG )
6 isperp.a 
 |-  ( ph -> A e. ran L )
7 foot.x 
 |-  ( ph -> C e. P )
8 foot.y 
 |-  ( ph -> -. C e. A )
9 1 2 3 4 5 6 7 8 footex 
 |-  ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A )
10 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
11 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> G e. TarskiG )
12 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> C e. P )
13 5 adantr 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> G e. TarskiG )
14 6 adantr 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> A e. ran L )
15 simprl 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> x e. A )
16 1 4 3 13 14 15 tglnpt 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> x e. P )
17 16 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> x e. P )
18 simprr 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> z e. A )
19 1 4 3 13 14 18 tglnpt 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> z e. P )
20 19 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> z e. P )
21 8 adantr 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> -. C e. A )
22 nelne2 
 |-  ( ( x e. A /\ -. C e. A ) -> x =/= C )
23 15 21 22 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> x =/= C )
24 23 necomd 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> C =/= x )
25 24 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> C =/= x )
26 1 3 4 11 12 17 25 tglinerflx1 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> C e. ( C L x ) )
27 18 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> z e. A )
28 simprl 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> ( C L x ) ( perpG ` G ) A )
29 7 adantr 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> C e. P )
30 1 3 4 13 29 16 24 tgelrnln 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> ( C L x ) e. ran L )
31 1 3 4 13 29 16 24 tglinerflx2 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> x e. ( C L x ) )
32 31 15 elind 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> x e. ( ( C L x ) i^i A ) )
33 1 2 3 4 13 30 14 32 isperp2 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> ( ( C L x ) ( perpG ` G ) A <-> A. u e. ( C L x ) A. v e. A <" u x v "> e. ( raG ` G ) ) )
34 33 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> ( ( C L x ) ( perpG ` G ) A <-> A. u e. ( C L x ) A. v e. A <" u x v "> e. ( raG ` G ) ) )
35 28 34 mpbid 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> A. u e. ( C L x ) A. v e. A <" u x v "> e. ( raG ` 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 -> <" u x v "> = <" C x v "> )
40 39 eleq1d 
 |-  ( u = C -> ( <" u x v "> e. ( raG ` G ) <-> <" C x v "> e. ( raG ` 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 -> <" C x v "> = <" C x z "> )
45 44 eleq1d 
 |-  ( v = z -> ( <" C x v "> e. ( raG ` G ) <-> <" C x z "> e. ( raG ` G ) ) )
46 40 45 rspc2va 
 |-  ( ( ( C e. ( C L x ) /\ z e. A ) /\ A. u e. ( C L x ) A. v e. A <" u x v "> e. ( raG ` G ) ) -> <" C x z "> e. ( raG ` G ) )
47 26 27 35 46 syl21anc 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> <" C x z "> e. ( raG ` G ) )
48 nelne2 
 |-  ( ( z e. A /\ -. C e. A ) -> z =/= C )
49 18 21 48 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> z =/= C )
50 49 necomd 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> C =/= z )
51 50 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> C =/= z )
52 1 3 4 11 12 20 51 tglinerflx1 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> C e. ( C L z ) )
53 15 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> x e. A )
54 simprr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> ( C L z ) ( perpG ` G ) A )
55 1 3 4 13 29 19 50 tgelrnln 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> ( C L z ) e. ran L )
56 1 3 4 13 29 19 50 tglinerflx2 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> z e. ( C L z ) )
57 56 18 elind 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> z e. ( ( C L z ) i^i A ) )
58 1 2 3 4 13 55 14 57 isperp2 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> ( ( C L z ) ( perpG ` G ) A <-> A. u e. ( C L z ) A. v e. A <" u z v "> e. ( raG ` G ) ) )
59 58 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> ( ( C L z ) ( perpG ` G ) A <-> A. u e. ( C L z ) A. v e. A <" u z v "> e. ( raG ` G ) ) )
60 54 59 mpbid 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> A. u e. ( C L z ) A. v e. A <" u z v "> e. ( raG ` G ) )
61 eqidd 
 |-  ( u = C -> z = z )
62 36 61 38 s3eqd 
 |-  ( u = C -> <" u z v "> = <" C z v "> )
63 62 eleq1d 
 |-  ( u = C -> ( <" u z v "> e. ( raG ` G ) <-> <" C z v "> e. ( raG ` 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 -> <" C z v "> = <" C z x "> )
68 67 eleq1d 
 |-  ( v = x -> ( <" C z v "> e. ( raG ` G ) <-> <" C z x "> e. ( raG ` G ) ) )
69 63 68 rspc2va 
 |-  ( ( ( C e. ( C L z ) /\ x e. A ) /\ A. u e. ( C L z ) A. v e. A <" u z v "> e. ( raG ` G ) ) -> <" C z x "> e. ( raG ` G ) )
70 52 53 60 69 syl21anc 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> <" C z x "> e. ( raG ` G ) )
71 1 2 3 4 10 11 12 17 20 47 70 ragflat 
 |-  ( ( ( ph /\ ( x e. A /\ z e. A ) ) /\ ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) ) -> x = z )
72 71 ex 
 |-  ( ( ph /\ ( x e. A /\ z e. A ) ) -> ( ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) -> x = z ) )
73 72 ralrimivva 
 |-  ( ph -> A. x e. A A. z e. A ( ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) -> x = z ) )
74 oveq2 
 |-  ( x = z -> ( C L x ) = ( C L z ) )
75 74 breq1d 
 |-  ( x = z -> ( ( C L x ) ( perpG ` G ) A <-> ( C L z ) ( perpG ` G ) A ) )
76 75 rmo4 
 |-  ( E* x e. A ( C L x ) ( perpG ` G ) A <-> A. x e. A A. z e. A ( ( ( C L x ) ( perpG ` G ) A /\ ( C L z ) ( perpG ` G ) A ) -> x = z ) )
77 73 76 sylibr 
 |-  ( ph -> E* x e. A ( C L x ) ( perpG ` G ) A )
78 reu5 
 |-  ( E! x e. A ( C L x ) ( perpG ` G ) A <-> ( E. x e. A ( C L x ) ( perpG ` G ) A /\ E* x e. A ( C L x ) ( perpG ` G ) A ) )
79 9 77 78 sylanbrc 
 |-  ( ph -> E! x e. A ( C L x ) ( perpG ` G ) A )