Theorem footne

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

	Ref	Expression
Hypotheses	isperp.p	$$⊢P={\mathrm{Base}}_G$$
	isperp.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	isperp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	isperp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	isperp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	isperp.a	$$⊢\phi \to A\in \mathrm{ran}L$$
	footne.x	$$⊢\phi \to X\in A$$
	footne.y	$$⊢\phi \to Y\in P$$
	footne.1	$$⊢\phi \to \left(XLY\right){⟂}_{𝒢}\left(G\right)A$$
Assertion	footne	$$⊢\phi \to \neg Y\in A$$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$$⊢P={\mathrm{Base}}_G$$
2		isperp.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		isperp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		isperp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		isperp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		isperp.a	$$⊢\phi \to A\in \mathrm{ran}L$$
7		footne.x	$$⊢\phi \to X\in A$$
8		footne.y	$$⊢\phi \to Y\in P$$
9		footne.1	$$⊢\phi \to \left(XLY\right){⟂}_{𝒢}\left(G\right)A$$
10	5	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
11	6	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to A\in \mathrm{ran}L$$
12	4 5 9	perpln1	$$⊢\phi \to XLY\in \mathrm{ran}L$$
13	12	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to XLY\in \mathrm{ran}L$$
14	1 2 3 4 5 12 6 9	perpneq	$$⊢\phi \to XLY\ne A$$
15	14	necomd	$$⊢\phi \to A\ne XLY$$
16	15	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to A\ne XLY$$
17	7	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to X\in A$$
18	1 4 3 5 6 7	tglnpt	$$⊢\phi \to X\in P$$
19	1 3 4 5 18 8 12	tglnne	$$⊢\phi \to X\ne Y$$
20	1 3 4 5 18 8 19	tglinerflx1	$$⊢\phi \to X\in \left(XLY\right)$$
21	20	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to X\in \left(XLY\right)$$
22	17 21	elind	$$⊢\left(\phi \wedge Y\in A\right)\to X\in \left(A\cap \left(XLY\right)\right)$$
23		simpr	$$⊢\left(\phi \wedge Y\in A\right)\to Y\in A$$
24	1 3 4 5 18 8 19	tglinerflx2	$$⊢\phi \to Y\in \left(XLY\right)$$
25	24	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to Y\in \left(XLY\right)$$
26	23 25	elind	$$⊢\left(\phi \wedge Y\in A\right)\to Y\in \left(A\cap \left(XLY\right)\right)$$
27	1 3 4 10 11 13 16 22 26	tglineineq	$$⊢\left(\phi \wedge Y\in A\right)\to X=Y$$
28	19	adantr	$$⊢\left(\phi \wedge Y\in A\right)\to X\ne Y$$
29	27 28	pm2.21ddne	$$⊢\left(\phi \wedge Y\in A\right)\to \neg Y\in A$$
30	29	pm2.01da	$$⊢\phi \to \neg Y\in A$$