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	$⊢ P = {Base}_{G}$
	lmiopp.m	$⊢ \underset{˙}{-} = dist (G)$
	lmiopp.i	$⊢ I = Itv (G)$
	lmiopp.l	$⊢ L = {Line}_{𝒢} (G)$
	lmiopp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	lmiopp.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	lmiopp.d	$⊢ φ \to D \in ran L$
	lmiopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	lnperpex.a	$⊢ φ \to A \in D$
	lnperpex.q	$⊢ φ \to Q \in P$
	lnperpex.1	$⊢ φ \to \neg Q \in D$
Assertion	lnperpex	$⊢ φ \to \exists p \in P (D ⟂_{𝒢} (G) (p L A) \land p {hp}_{𝒢} (G) (D) Q)$

Proof

Step	Hyp	Ref	Expression
1		lmiopp.p	$⊢ P = {Base}_{G}$
2		lmiopp.m	$⊢ \underset{˙}{-} = dist (G)$
3		lmiopp.i	$⊢ I = Itv (G)$
4		lmiopp.l	$⊢ L = {Line}_{𝒢} (G)$
5		lmiopp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		lmiopp.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
7		lmiopp.d	$⊢ φ \to D \in ran L$
8		lmiopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
9		lnperpex.a	$⊢ φ \to A \in D$
10		lnperpex.q	$⊢ φ \to Q \in P$
11		lnperpex.1	$⊢ φ \to \neg Q \in D$
12	5	ad4antr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to G \in 𝒢_{Tarski}$
13	12	adantr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to G \in 𝒢_{Tarski}$
14		simprl	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p \in P$
15	1 4 3 5 7 9	tglnpt	$⊢ φ \to A \in P$
16	15	ad2antrr	$⊢ ((φ \land d \in D) \land A \neq d) \to A \in P$
17	16	ad3antrrr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to A \in P$
18		simprrl	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to (A L p) ⟂_{𝒢} (G) D$
19	4 13 18	perpln1	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to A L p \in ran L$
20	1 3 4 13 17 14 19	tglnne	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to A \neq p$
21	20	necomd	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p \neq A$
22	1 3 4 13 14 17 21	tgelrnln	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p L A \in ran L$
23	7	ad4antr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to D \in ran L$
24	23	adantr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to D \in ran L$
25	1 3 4 13 14 17 21	tglinecom	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p L A = A L p$
26	25 18	eqbrtrd	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to (p L A) ⟂_{𝒢} (G) D$
27	1 2 3 4 13 22 24 26	perpcom	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to D ⟂_{𝒢} (G) (p L A)$
28		simplr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to Q O c$
29	10	ad4antr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to Q \in P$
30	29	adantr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to Q \in P$
31		simplr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to c \in P$
32	31	adantr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to c \in P$
33		simprrr	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to c O p$
34	1 2 3 8 4 24 13 32 14 33	oppcom	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p O c$
35	1 3 4 8 13 24 14 30 32 34	lnopp2hpgb	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to (Q O c \leftrightarrow p {hp}_{𝒢} (G) (D) Q)$
36	28 35	mpbid	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to p {hp}_{𝒢} (G) (D) Q$
37	27 36	jca	$⊢ (((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) D \land c O p))) \to (D ⟂_{𝒢} (G) (p L A) \land p {hp}_{𝒢} (G) (D) Q)$
38		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
39	9	ad4antr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to A \in D$
40		simpr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to Q O c$
41	1 2 3 8 4 23 12 29 31 40	oppne2	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to \neg c \in D$
42	6	ad4antr	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to G {Dim}_{𝒢} \geq 2$
43	1 2 3 8 4 23 12 38 39 31 41 42	oppperpex	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) D \land c O p)$
44	37 43	reximddv	$⊢ ((((φ \land d \in D) \land A \neq d) \land c \in P) \land Q O c) \to \exists p \in P (D ⟂_{𝒢} (G) (p L A) \land p {hp}_{𝒢} (G) (D) Q)$
45	1 3 4 5 7 10 8 11	hpgerlem	$⊢ φ \to \exists c \in P Q O c$
46	45	ad2antrr	$⊢ ((φ \land d \in D) \land A \neq d) \to \exists c \in P Q O c$
47	44 46	r19.29a	$⊢ ((φ \land d \in D) \land A \neq d) \to \exists p \in P (D ⟂_{𝒢} (G) (p L A) \land p {hp}_{𝒢} (G) (D) Q)$
48	1 3 4 5 7 9	tglnpt2	$⊢ φ \to \exists d \in D A \neq d$
49	47 48	r19.29a	$⊢ φ \to \exists p \in P (D ⟂_{𝒢} (G) (p L A) \land p {hp}_{𝒢} (G) (D) Q)$

Metamath Proof Explorer

Theorem lnperpex

Proof