Theorem footeq

Description: Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020)

	Ref	Expression
Hypotheses	isperp.p	|- P = ( Base ` G )
	isperp.d	|- .- = ( dist ` G )
	isperp.i	|- I = ( Itv ` G )
	isperp.l	|- L = ( LineG ` G )
	isperp.g	|- ( ph -> G e. TarskiG )
	isperp.a	|- ( ph -> A e. ran L )
	footeq.x	|- ( ph -> X e. A )
	footeq.y	|- ( ph -> Y e. A )
	footeq.z	|- ( ph -> Z e. P )
	footeq.1	|- ( ph -> ( X L Z ) ( perpG ` G ) A )
	footeq.2	|- ( ph -> ( Y L Z ) ( perpG ` G ) A )
Assertion	footeq	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		isperp.p	|- P = ( Base ` G )
2		isperp.d	|- .- = ( dist ` G )
3		isperp.i	|- I = ( Itv ` G )
4		isperp.l	|- L = ( LineG ` G )
5		isperp.g	|- ( ph -> G e. TarskiG )
6		isperp.a	|- ( ph -> A e. ran L )
7		footeq.x	|- ( ph -> X e. A )
8		footeq.y	|- ( ph -> Y e. A )
9		footeq.z	|- ( ph -> Z e. P )
10		footeq.1	|- ( ph -> ( X L Z ) ( perpG ` G ) A )
11		footeq.2	|- ( ph -> ( Y L Z ) ( perpG ` G ) A )
12		oveq2	|- ( x = X -> ( Z L x ) = ( Z L X ) )
13	12	breq1d	|- ( x = X -> ( ( Z L x ) ( perpG ` G ) A <-> ( Z L X ) ( perpG ` G ) A ) )
14		oveq2	|- ( x = Y -> ( Z L x ) = ( Z L Y ) )
15	14	breq1d	|- ( x = Y -> ( ( Z L x ) ( perpG ` G ) A <-> ( Z L Y ) ( perpG ` G ) A ) )
16	1 2 3 4 5 6 7 9 10	footne	|- ( ph -> -. Z e. A )
17	1 2 3 4 5 6 9 16	foot	|- ( ph -> E! x e. A ( Z L x ) ( perpG ` G ) A )
18	1 4 3 5 6 7	tglnpt	|- ( ph -> X e. P )
19	4 5 10	perpln1	|- ( ph -> ( X L Z ) e. ran L )
20	1 3 4 5 18 9 19	tglnne	|- ( ph -> X =/= Z )
21	1 3 4 5 18 9 20	tglinecom	|- ( ph -> ( X L Z ) = ( Z L X ) )
22	21 10	eqbrtrrd	|- ( ph -> ( Z L X ) ( perpG ` G ) A )
23	1 4 3 5 6 8	tglnpt	|- ( ph -> Y e. P )
24	4 5 11	perpln1	|- ( ph -> ( Y L Z ) e. ran L )
25	1 3 4 5 23 9 24	tglnne	|- ( ph -> Y =/= Z )
26	1 3 4 5 23 9 25	tglinecom	|- ( ph -> ( Y L Z ) = ( Z L Y ) )
27	26 11	eqbrtrrd	|- ( ph -> ( Z L Y ) ( perpG ` G ) A )
28	13 15 17 7 8 22 27	reu2eqd	|- ( ph -> X = Y )