footne

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

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

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		footne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		footne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9		footne.1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
11	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝐴 ∈ ran 𝐿 )
12	4 5 9	perpln1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
14	1 2 3 4 5 12 6 9	perpneq	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ 𝐴 )
15	14	necomd	⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
17	7	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
18	1 4 3 5 6 7	tglnpt	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
19	1 3 4 5 18 8 12	tglnne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
20	1 3 4 5 18 8 19	tglinerflx1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
22	17 21	elind	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
24	1 3 4 5 18 8 19	tglinerflx2	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
26	23 25	elind	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) )
27	1 3 4 10 11 13 16 22 26	tglineineq	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 = 𝑌 )
28	19	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ≠ 𝑌 )
29	27 28	pm2.21ddne	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ¬ 𝑌 ∈ 𝐴 )
30	29	pm2.01da	⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐴 )

Metamath Proof Explorer

Theorem footne

Proof