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=BaseG
lmiopp.m -˙=distG
lmiopp.i I=ItvG
lmiopp.l L=Line𝒢G
lmiopp.g φG𝒢Tarski
lmiopp.h φGDim𝒢2
lmiopp.d φDranL
lmiopp.o O=ab|aPDbPDtDtaIb
lnperpex.a φAD
lnperpex.q φQP
lnperpex.1 φ¬QD
Assertion lnperpex φpPD𝒢GpLAphp𝒢GDQ

Proof

Step Hyp Ref Expression
1 lmiopp.p P=BaseG
2 lmiopp.m -˙=distG
3 lmiopp.i I=ItvG
4 lmiopp.l L=Line𝒢G
5 lmiopp.g φG𝒢Tarski
6 lmiopp.h φGDim𝒢2
7 lmiopp.d φDranL
8 lmiopp.o O=ab|aPDbPDtDtaIb
9 lnperpex.a φAD
10 lnperpex.q φQP
11 lnperpex.1 φ¬QD
12 5 ad4antr φdDAdcPQOcG𝒢Tarski
13 12 adantr φdDAdcPQOcpPALp𝒢GDcOpG𝒢Tarski
14 simprl φdDAdcPQOcpPALp𝒢GDcOppP
15 1 4 3 5 7 9 tglnpt φAP
16 15 ad2antrr φdDAdAP
17 16 ad3antrrr φdDAdcPQOcpPALp𝒢GDcOpAP
18 simprrl φdDAdcPQOcpPALp𝒢GDcOpALp𝒢GD
19 4 13 18 perpln1 φdDAdcPQOcpPALp𝒢GDcOpALpranL
20 1 3 4 13 17 14 19 tglnne φdDAdcPQOcpPALp𝒢GDcOpAp
21 20 necomd φdDAdcPQOcpPALp𝒢GDcOppA
22 1 3 4 13 14 17 21 tgelrnln φdDAdcPQOcpPALp𝒢GDcOppLAranL
23 7 ad4antr φdDAdcPQOcDranL
24 23 adantr φdDAdcPQOcpPALp𝒢GDcOpDranL
25 1 3 4 13 14 17 21 tglinecom φdDAdcPQOcpPALp𝒢GDcOppLA=ALp
26 25 18 eqbrtrd φdDAdcPQOcpPALp𝒢GDcOppLA𝒢GD
27 1 2 3 4 13 22 24 26 perpcom φdDAdcPQOcpPALp𝒢GDcOpD𝒢GpLA
28 simplr φdDAdcPQOcpPALp𝒢GDcOpQOc
29 10 ad4antr φdDAdcPQOcQP
30 29 adantr φdDAdcPQOcpPALp𝒢GDcOpQP
31 simplr φdDAdcPQOccP
32 31 adantr φdDAdcPQOcpPALp𝒢GDcOpcP
33 simprrr φdDAdcPQOcpPALp𝒢GDcOpcOp
34 1 2 3 8 4 24 13 32 14 33 oppcom φdDAdcPQOcpPALp𝒢GDcOppOc
35 1 3 4 8 13 24 14 30 32 34 lnopp2hpgb φdDAdcPQOcpPALp𝒢GDcOpQOcphp𝒢GDQ
36 28 35 mpbid φdDAdcPQOcpPALp𝒢GDcOpphp𝒢GDQ
37 27 36 jca φdDAdcPQOcpPALp𝒢GDcOpD𝒢GpLAphp𝒢GDQ
38 eqid hl𝒢G=hl𝒢G
39 9 ad4antr φdDAdcPQOcAD
40 simpr φdDAdcPQOcQOc
41 1 2 3 8 4 23 12 29 31 40 oppne2 φdDAdcPQOc¬cD
42 6 ad4antr φdDAdcPQOcGDim𝒢2
43 1 2 3 8 4 23 12 38 39 31 41 42 oppperpex φdDAdcPQOcpPALp𝒢GDcOp
44 37 43 reximddv φdDAdcPQOcpPD𝒢GpLAphp𝒢GDQ
45 1 3 4 5 7 10 8 11 hpgerlem φcPQOc
46 45 ad2antrr φdDAdcPQOc
47 44 46 r19.29a φdDAdpPD𝒢GpLAphp𝒢GDQ
48 1 3 4 5 7 9 tglnpt2 φdDAd
49 47 48 r19.29a φpPD𝒢GpLAphp𝒢GDQ