Theorem lnperpexs

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	lnperpexs.p	|- P = ( Base ` G )
	lnperpexs.l	|- L = ( LineG ` G )
	lnperpexs.g	|- ( ph -> G e. TarskiG )
	lnperpexs.h	|- ( ph -> G TarskiGDim>= 2 )
	lnperpexs.d	|- ( ph -> D e. ran L )
	lnperpexs.a	|- ( ph -> A e. D )
	lnperpexs.q	|- ( ph -> Q e. P )
	lnperpexs.1	|- ( ph -> -. Q e. D )
Assertion	lnperpexs	|- ( ph -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )

Proof

Step	Hyp	Ref	Expression
1		lnperpexs.p	|- P = ( Base ` G )
2		lnperpexs.l	|- L = ( LineG ` G )
3		lnperpexs.g	|- ( ph -> G e. TarskiG )
4		lnperpexs.h	|- ( ph -> G TarskiGDim>= 2 )
5		lnperpexs.d	|- ( ph -> D e. ran L )
6		lnperpexs.a	|- ( ph -> A e. D )
7		lnperpexs.q	|- ( ph -> Q e. P )
8		lnperpexs.1	|- ( ph -> -. Q e. D )
9		eqid	|- ( dist ` G ) = ( dist ` G )
10		eqid	|- ( Itv ` G ) = ( Itv ` G )
11		eleq1w	|- ( a = c -> ( a e. ( P \ D ) <-> c e. ( P \ D ) ) )
12		eleq1w	|- ( b = d -> ( b e. ( P \ D ) <-> d e. ( P \ D ) ) )
13	11 12	bi2anan9	|- ( ( a = c /\ b = d ) -> ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) <-> ( c e. ( P \ D ) /\ d e. ( P \ D ) ) ) )
14		oveq12	|- ( ( a = c /\ b = d ) -> ( a ( Itv ` G ) b ) = ( c ( Itv ` G ) d ) )
15	14	eleq2d	|- ( ( a = c /\ b = d ) -> ( s e. ( a ( Itv ` G ) b ) <-> s e. ( c ( Itv ` G ) d ) ) )
16	15	rexbidv	|- ( ( a = c /\ b = d ) -> ( E. s e. D s e. ( a ( Itv ` G ) b ) <-> E. s e. D s e. ( c ( Itv ` G ) d ) ) )
17		eleq1w	|- ( s = t -> ( s e. ( c ( Itv ` G ) d ) <-> t e. ( c ( Itv ` G ) d ) ) )
18	17	cbvrexvw	|- ( E. s e. D s e. ( c ( Itv ` G ) d ) <-> E. t e. D t e. ( c ( Itv ` G ) d ) )
19	16 18	bitrdi	|- ( ( a = c /\ b = d ) -> ( E. s e. D s e. ( a ( Itv ` G ) b ) <-> E. t e. D t e. ( c ( Itv ` G ) d ) ) )
20	13 19	anbi12d	|- ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. s e. D s e. ( a ( Itv ` G ) b ) ) <-> ( ( c e. ( P \ D ) /\ d e. ( P \ D ) ) /\ E. t e. D t e. ( c ( Itv ` G ) d ) ) ) )
21	20	cbvopabv	|- { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. s e. D s e. ( a ( Itv ` G ) b ) ) } = { <. c , d >. | ( ( c e. ( P \ D ) /\ d e. ( P \ D ) ) /\ E. t e. D t e. ( c ( Itv ` G ) d ) ) }
22	1 9 10 2 3 4 5 21 6 7 8	lnperpex	|- ( ph -> E. p e. P ( D ( perpG ` G ) ( p L A ) /\ p ( ( hpG ` G ) ` D ) Q ) )