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 | |
|
lmiopp.m | |
||
lmiopp.i | |
||
lmiopp.l | |
||
lmiopp.g | |
||
lmiopp.h | |
||
lmiopp.d | |
||
lmiopp.o | |
||
lnperpex.a | |
||
lnperpex.q | |
||
lnperpex.1 | |
||
Assertion | lnperpex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmiopp.p | |
|
2 | lmiopp.m | |
|
3 | lmiopp.i | |
|
4 | lmiopp.l | |
|
5 | lmiopp.g | |
|
6 | lmiopp.h | |
|
7 | lmiopp.d | |
|
8 | lmiopp.o | |
|
9 | lnperpex.a | |
|
10 | lnperpex.q | |
|
11 | lnperpex.1 | |
|
12 | 5 | ad4antr | |
13 | 12 | adantr | |
14 | simprl | |
|
15 | 1 4 3 5 7 9 | tglnpt | |
16 | 15 | ad2antrr | |
17 | 16 | ad3antrrr | |
18 | simprrl | |
|
19 | 4 13 18 | perpln1 | |
20 | 1 3 4 13 17 14 19 | tglnne | |
21 | 20 | necomd | |
22 | 1 3 4 13 14 17 21 | tgelrnln | |
23 | 7 | ad4antr | |
24 | 23 | adantr | |
25 | 1 3 4 13 14 17 21 | tglinecom | |
26 | 25 18 | eqbrtrd | |
27 | 1 2 3 4 13 22 24 26 | perpcom | |
28 | simplr | |
|
29 | 10 | ad4antr | |
30 | 29 | adantr | |
31 | simplr | |
|
32 | 31 | adantr | |
33 | simprrr | |
|
34 | 1 2 3 8 4 24 13 32 14 33 | oppcom | |
35 | 1 3 4 8 13 24 14 30 32 34 | lnopp2hpgb | |
36 | 28 35 | mpbid | |
37 | 27 36 | jca | |
38 | eqid | |
|
39 | 9 | ad4antr | |
40 | simpr | |
|
41 | 1 2 3 8 4 23 12 29 31 40 | oppne2 | |
42 | 6 | ad4antr | |
43 | 1 2 3 8 4 23 12 38 39 31 41 42 | oppperpex | |
44 | 37 43 | reximddv | |
45 | 1 3 4 5 7 10 8 11 | hpgerlem | |
46 | 45 | ad2antrr | |
47 | 44 46 | r19.29a | |
48 | 1 3 4 5 7 9 | tglnpt2 | |
49 | 47 48 | r19.29a | |