Theorem footeq

Description: Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-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$$
	footeq.x	$$⊢\phi \to X\in A$$
	footeq.y	$$⊢\phi \to Y\in A$$
	footeq.z	$$⊢\phi \to Z\in P$$
	footeq.1	$$⊢\phi \to \left(XLZ\right){⟂}_{𝒢}\left(G\right)A$$
	footeq.2	$$⊢\phi \to \left(YLZ\right){⟂}_{𝒢}\left(G\right)A$$
Assertion	footeq	$$⊢\phi \to X=Y$$

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		footeq.x	$$⊢\phi \to X\in A$$
8		footeq.y	$$⊢\phi \to Y\in A$$
9		footeq.z	$$⊢\phi \to Z\in P$$
10		footeq.1	$$⊢\phi \to \left(XLZ\right){⟂}_{𝒢}\left(G\right)A$$
11		footeq.2	$$⊢\phi \to \left(YLZ\right){⟂}_{𝒢}\left(G\right)A$$
12		oveq2	$$⊢x=X\to ZLx=ZLX$$
13	12	breq1d	$$⊢x=X\to \left(\left(ZLx\right){⟂}_{𝒢}\left(G\right)A\leftrightarrow \left(ZLX\right){⟂}_{𝒢}\left(G\right)A\right)$$
14		oveq2	$$⊢x=Y\to ZLx=ZLY$$
15	14	breq1d	$$⊢x=Y\to \left(\left(ZLx\right){⟂}_{𝒢}\left(G\right)A\leftrightarrow \left(ZLY\right){⟂}_{𝒢}\left(G\right)A\right)$$
16	1 2 3 4 5 6 7 9 10	footne	$$⊢\phi \to \neg Z\in A$$
17	1 2 3 4 5 6 9 16	foot	$$⊢\phi \to \exists !x\in A\left(ZLx\right){⟂}_{𝒢}\left(G\right)A$$
18	1 4 3 5 6 7	tglnpt	$$⊢\phi \to X\in P$$
19	4 5 10	perpln1	$$⊢\phi \to XLZ\in \mathrm{ran}L$$
20	1 3 4 5 18 9 19	tglnne	$$⊢\phi \to X\ne Z$$
21	1 3 4 5 18 9 20	tglinecom	$$⊢\phi \to XLZ=ZLX$$
22	21 10	eqbrtrrd	$$⊢\phi \to \left(ZLX\right){⟂}_{𝒢}\left(G\right)A$$
23	1 4 3 5 6 8	tglnpt	$$⊢\phi \to Y\in P$$
24	4 5 11	perpln1	$$⊢\phi \to YLZ\in \mathrm{ran}L$$
25	1 3 4 5 23 9 24	tglnne	$$⊢\phi \to Y\ne Z$$
26	1 3 4 5 23 9 25	tglinecom	$$⊢\phi \to YLZ=ZLY$$
27	26 11	eqbrtrrd	$$⊢\phi \to \left(ZLY\right){⟂}_{𝒢}\left(G\right)A$$
28	13 15 17 7 8 22 27	reu2eqd	$$⊢\phi \to X=Y$$