Theorem footeq

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

	Ref	Expression
Hypotheses	isperp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	isperp.d	⊢ − = ( dist ‘ 𝐺 )
	isperp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	isperp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	isperp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	isperp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	footeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	footeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	footeq.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	footeq.1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
	footeq.2	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
Assertion	footeq	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		isperp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		isperp.d	⊢ − = ( dist ‘ 𝐺 )
3		isperp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		isperp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		isperp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		isperp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7		footeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		footeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
9		footeq.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10		footeq.1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
11		footeq.2	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
12		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑍 𝐿 𝑥 ) = ( 𝑍 𝐿 𝑋 ) )
13	12	breq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑍 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 ↔ ( 𝑍 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) )
14		oveq2	⊢ ( 𝑥 = 𝑌 → ( 𝑍 𝐿 𝑥 ) = ( 𝑍 𝐿 𝑌 ) )
15	14	breq1d	⊢ ( 𝑥 = 𝑌 → ( ( 𝑍 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 ↔ ( 𝑍 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) )
16	1 2 3 4 5 6 7 9 10	footne	⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝐴 )
17	1 2 3 4 5 6 9 16	foot	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 ( 𝑍 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
18	1 4 3 5 6 7	tglnpt	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
19	4 5 10	perpln1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
20	1 3 4 5 18 9 19	tglnne	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
21	1 3 4 5 18 9 20	tglinecom	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
22	21 10	eqbrtrrd	⊢ ( 𝜑 → ( 𝑍 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
23	1 4 3 5 6 8	tglnpt	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
24	4 5 11	perpln1	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
25	1 3 4 5 23 9 24	tglnne	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
26	1 3 4 5 23 9 25	tglinecom	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑌 ) )
27	26 11	eqbrtrrd	⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
28	13 15 17 7 8 22 27	reu2eqd	⊢ ( 𝜑 → 𝑋 = 𝑌 )