Theorem footne

Description: Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-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 )
	footne.x	|- ( ph -> X e. A )
	footne.y	|- ( ph -> Y e. P )
	footne.1	|- ( ph -> ( X L Y ) ( perpG ` G ) A )
Assertion	footne	|- ( ph -> -. Y e. A )

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		footne.x	|- ( ph -> X e. A )
8		footne.y	|- ( ph -> Y e. P )
9		footne.1	|- ( ph -> ( X L Y ) ( perpG ` G ) A )
10	5	adantr	|- ( ( ph /\ Y e. A ) -> G e. TarskiG )
11	6	adantr	|- ( ( ph /\ Y e. A ) -> A e. ran L )
12	4 5 9	perpln1	|- ( ph -> ( X L Y ) e. ran L )
13	12	adantr	|- ( ( ph /\ Y e. A ) -> ( X L Y ) e. ran L )
14	1 2 3 4 5 12 6 9	perpneq	|- ( ph -> ( X L Y ) =/= A )
15	14	necomd	|- ( ph -> A =/= ( X L Y ) )
16	15	adantr	|- ( ( ph /\ Y e. A ) -> A =/= ( X L Y ) )
17	7	adantr	|- ( ( ph /\ Y e. A ) -> X e. A )
18	1 4 3 5 6 7	tglnpt	|- ( ph -> X e. P )
19	1 3 4 5 18 8 12	tglnne	|- ( ph -> X =/= Y )
20	1 3 4 5 18 8 19	tglinerflx1	|- ( ph -> X e. ( X L Y ) )
21	20	adantr	|- ( ( ph /\ Y e. A ) -> X e. ( X L Y ) )
22	17 21	elind	|- ( ( ph /\ Y e. A ) -> X e. ( A i^i ( X L Y ) ) )
23		simpr	|- ( ( ph /\ Y e. A ) -> Y e. A )
24	1 3 4 5 18 8 19	tglinerflx2	|- ( ph -> Y e. ( X L Y ) )
25	24	adantr	|- ( ( ph /\ Y e. A ) -> Y e. ( X L Y ) )
26	23 25	elind	|- ( ( ph /\ Y e. A ) -> Y e. ( A i^i ( X L Y ) ) )
27	1 3 4 10 11 13 16 22 26	tglineineq	|- ( ( ph /\ Y e. A ) -> X = Y )
28	19	adantr	|- ( ( ph /\ Y e. A ) -> X =/= Y )
29	27 28	pm2.21ddne	|- ( ( ph /\ Y e. A ) -> -. Y e. A )
30	29	pm2.01da	|- ( ph -> -. Y e. A )