Metamath Proof Explorer

Theorem lnperpex

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 lmiopp.p 
|- P = ( Base ` G )
lmiopp.m 
|- .- = ( dist ` G )
lmiopp.i 
|- I = ( Itv ` G )
lmiopp.l 
|- L = ( LineG ` G )
lmiopp.g 
|- ( ph -> G e. TarskiG )
lmiopp.h 
|- ( ph -> G TarskiGDim>= 2 )
lmiopp.d 
|- ( ph -> D e. ran L )
lmiopp.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
lnperpex.a 
|- ( ph -> A e. D )
lnperpex.q 
|- ( ph -> Q e. P )
lnperpex.1 
|- ( ph -> -. Q e. D )
Assertion lnperpex 
|- ( ph -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )

Proof

Step Hyp Ref Expression
1 lmiopp.p 
 |-  P = ( Base ` G )
2 lmiopp.m 
 |-  .- = ( dist ` G )
3 lmiopp.i 
 |-  I = ( Itv ` G )
4 lmiopp.l 
 |-  L = ( LineG ` G )
5 lmiopp.g 
 |-  ( ph -> G e. TarskiG )
6 lmiopp.h 
 |-  ( ph -> G TarskiGDim>= 2 )
7 lmiopp.d 
 |-  ( ph -> D e. ran L )
8 lmiopp.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
9 lnperpex.a 
 |-  ( ph -> A e. D )
10 lnperpex.q 
 |-  ( ph -> Q e. P )
11 lnperpex.1 
 |-  ( ph -> -. Q e. D )
12 5 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> G e. TarskiG )
13 12 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> G e. TarskiG )
14 simprl 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> p e. P )
15 1 4 3 5 7 9 tglnpt 
 |-  ( ph -> A e. P )
16 15 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ A =/= d ) -> A e. P )
17 16 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> A e. P )
18 simprrl 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( A L p ) ( perpG ` G ) D )
19 4 13 18 perpln1 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( A L p ) e. ran L )
20 1 3 4 13 17 14 19 tglnne 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> A =/= p )
21 20 necomd 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> p =/= A )
22 1 3 4 13 14 17 21 tgelrnln 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( p L A ) e. ran L )
23 7 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> D e. ran L )
24 23 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> D e. ran L )
25 1 3 4 13 14 17 21 tglinecom 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( p L A ) = ( A L p ) )
26 25 18 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( p L A ) ( perpG ` G ) D )
27 1 2 3 4 13 22 24 26 perpcom 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> D ( perpG ` G ) ( p L A ) )
28 simplr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> Q O c )
29 10 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> Q e. P )
30 29 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> Q e. P )
31 simplr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> c e. P )
32 31 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> c e. P )
33 simprrr 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> c O p )
34 1 2 3 8 4 24 13 32 14 33 oppcom 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> p O c )
35 1 3 4 8 13 24 14 30 32 34 lnopp2hpgb 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( Q O c <-> p ( ( hpG ` G ) ` D ) Q ) )
36 28 35 mpbid 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> p ( ( hpG ` G ) ` D ) Q )
37 27 36 jca 
 |-  ( ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) D /\ c O p ) ) ) -> ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )
38 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
39 9 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> A e. D )
40 simpr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> Q O c )
41 1 2 3 8 4 23 12 29 31 40 oppne2 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> -. c e. D )
42 6 ad4antr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> G TarskiGDim>= 2 )
43 1 2 3 8 4 23 12 38 39 31 41 42 oppperpex 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> E. p e. P ( ( A L p ) ( perpG ` G ) D /\ c O p ) )
44 37 43 reximddv 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ A =/= d ) /\ c e. P ) /\ Q O c ) -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )
45 1 3 4 5 7 10 8 11 hpgerlem 
 |-  ( ph -> E. c e. P Q O c )
46 45 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ A =/= d ) -> E. c e. P Q O c )
47 44 46 r19.29a 
 |-  ( ( ( ph /\ d e. D ) /\ A =/= d ) -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )
48 1 3 4 5 7 9 tglnpt2 
 |-  ( ph -> E. d e. D A =/= d )
49 47 48 r19.29a 
 |-  ( ph -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )