Theorem lnperpex

Description: Existence of a perpendicular to a line L at a given point A . Theorem 10.15 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	lmiopp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	lmiopp.m	⊢ − = ( dist ‘ 𝐺 )
	lmiopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	lmiopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	lmiopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	lmiopp.h	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
	lmiopp.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	lmiopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	lnperpex.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	lnperpex.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
	lnperpex.1	⊢ ( 𝜑 → ¬ 𝑄 ∈ 𝐷 )
Assertion	lnperpex	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) ∧ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		lmiopp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		lmiopp.m	⊢ − = ( dist ‘ 𝐺 )
3		lmiopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		lmiopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		lmiopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		lmiopp.h	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
7		lmiopp.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
8		lmiopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
9		lnperpex.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
10		lnperpex.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
11		lnperpex.1	⊢ ( 𝜑 → ¬ 𝑄 ∈ 𝐷 )
12	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝐺 ∈ TarskiG )
13	12	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
14		simprl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑝 ∈ 𝑃 )
15	1 4 3 5 7 9	tglnpt	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
16	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) → 𝐴 ∈ 𝑃 )
17	16	ad3antrrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝐴 ∈ 𝑃 )
18		simprrl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
19	4 13 18	perpln1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝐴 𝐿 𝑝 ) ∈ ran 𝐿 )
20	1 3 4 13 17 14 19	tglnne	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝐴 ≠ 𝑝 )
21	20	necomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑝 ≠ 𝐴 )
22	1 3 4 13 14 17 21	tgelrnln	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝑝 𝐿 𝐴 ) ∈ ran 𝐿 )
23	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝐷 ∈ ran 𝐿 )
24	23	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝐷 ∈ ran 𝐿 )
25	1 3 4 13 14 17 21	tglinecom	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝑝 𝐿 𝐴 ) = ( 𝐴 𝐿 𝑝 ) )
26	25 18	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝑝 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
27	1 2 3 4 13 22 24 26	perpcom	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) )
28		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑄 𝑂 𝑐 )
29	10	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝑄 ∈ 𝑃 )
30	29	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑄 ∈ 𝑃 )
31		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝑐 ∈ 𝑃 )
32	31	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑐 ∈ 𝑃 )
33		simprrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑐 𝑂 𝑝 )
34	1 2 3 8 4 24 13 32 14 33	oppcom	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑝 𝑂 𝑐 )
35	1 3 4 8 13 24 14 30 32 34	lnopp2hpgb	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝑄 𝑂 𝑐 ↔ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )
36	28 35	mpbid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 )
37	27 36	jca	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) ) ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) ∧ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )
38		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
39	9	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝐴 ∈ 𝐷 )
40		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝑄 𝑂 𝑐 )
41	1 2 3 8 4 23 12 29 31 40	oppne2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → ¬ 𝑐 ∈ 𝐷 )
42	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → 𝐺 DimTarskiG≥ 2 )
43	1 2 3 8 4 23 12 38 39 31 41 42	oppperpex	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝑐 𝑂 𝑝 ) )
44	37 43	reximddv	⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑄 𝑂 𝑐 ) → ∃ 𝑝 ∈ 𝑃 ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) ∧ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )
45	1 3 4 5 7 10 8 11	hpgerlem	⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 𝑄 𝑂 𝑐 )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) → ∃ 𝑐 ∈ 𝑃 𝑄 𝑂 𝑐 )
47	44 46	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑑 ) → ∃ 𝑝 ∈ 𝑃 ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) ∧ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )
48	1 3 4 5 7 9	tglnpt2	⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐷 𝐴 ≠ 𝑑 )
49	47 48	r19.29a	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) ∧ 𝑝 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝑄 ) )