Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lnperpex Structured version   Unicode version

Theorem lnperpex 24832
 Description: Existence of a perpendicular to a line at a given point . Theorem 10.15 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.)
Hypotheses
Ref Expression
lmiopp.p
lmiopp.m
lmiopp.i Itv
lmiopp.l LineG
lmiopp.g TarskiG
lmiopp.h DimTarskiG
lmiopp.d
lmiopp.o
lnperpex.a
lnperpex.q
lnperpex.1
Assertion
Ref Expression
lnperpex ⟂G hpG
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,

Proof of Theorem lnperpex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmiopp.p . . . . . 6
2 lmiopp.m . . . . . 6
3 lmiopp.i . . . . . 6 Itv
4 lmiopp.l . . . . . 6 LineG
5 lmiopp.g . . . . . . . . 9 TarskiG
65ad2antrr 730 . . . . . . . 8 TarskiG
76ad2antrr 730 . . . . . . 7 TarskiG
87adantr 466 . . . . . 6 ⟂G TarskiG
9 simprl 762 . . . . . . 7 ⟂G
10 lmiopp.d . . . . . . . . . 10
11 lnperpex.a . . . . . . . . . 10
121, 4, 3, 5, 10, 11tglnpt 24581 . . . . . . . . 9
1312ad2antrr 730 . . . . . . . 8
1413ad3antrrr 734 . . . . . . 7 ⟂G
15 simprrl 772 . . . . . . . . . 10 ⟂G ⟂G
164, 8, 15perpln1 24742 . . . . . . . . 9 ⟂G
171, 3, 4, 8, 14, 9, 16tglnne 24660 . . . . . . . 8 ⟂G
1817necomd 2695 . . . . . . 7 ⟂G
191, 3, 4, 8, 9, 14, 18tgelrnln 24662 . . . . . 6 ⟂G
2010ad2antrr 730 . . . . . . . 8
2120ad2antrr 730 . . . . . . 7
2221adantr 466 . . . . . 6 ⟂G
231, 3, 4, 8, 9, 14, 18tglinecom 24667 . . . . . . 7 ⟂G
2423, 15eqbrtrd 4441 . . . . . 6 ⟂G ⟂G
251, 2, 3, 4, 8, 19, 22, 24perpcom 24745 . . . . 5 ⟂G ⟂G
26 simpr 462 . . . . . . 7
2726adantr 466 . . . . . 6 ⟂G
28 lmiopp.o . . . . . . 7
29 lnperpex.q . . . . . . . . . 10
3029ad2antrr 730 . . . . . . . . 9
3130ad2antrr 730 . . . . . . . 8
3231adantr 466 . . . . . . 7 ⟂G
33 simplr 760 . . . . . . . 8
3433adantr 466 . . . . . . 7 ⟂G
35 simprrr 773 . . . . . . . 8 ⟂G
361, 2, 3, 28, 4, 22, 8, 34, 9, 35oppcom 24773 . . . . . . 7 ⟂G
371, 3, 4, 28, 8, 22, 9, 32, 34, 36lnopp2hpgb 24792 . . . . . 6 ⟂G hpG
3827, 37mpbid 213 . . . . 5 ⟂G hpG
3925, 38jca 534 . . . 4 ⟂G ⟂G hpG
40 eqid 2422 . . . . 5 hlG hlG
4111ad2antrr 730 . . . . . 6
4241ad2antrr 730 . . . . 5
431, 2, 3, 28, 4, 21, 7, 31, 33, 26oppne2 24771 . . . . 5
44 lmiopp.h . . . . . . 7 DimTarskiG
4544ad2antrr 730 . . . . . 6 DimTarskiG
4645ad2antrr 730 . . . . 5 DimTarskiG
471, 2, 3, 28, 4, 21, 7, 40, 42, 33, 43, 46oppperpex 24782 . . . 4 ⟂G
4839, 47reximddv 2901 . . 3 ⟂G hpG
49 lnperpex.1 . . . . 5
501, 3, 4, 5, 10, 29, 28, 49hpgerlem 24794 . . . 4