colperpex

Description: In dimension 2 and above, on a line ( A L B ) there is always a perpendicular P from A on a given plane (here given by C , in case C does not lie on the line). Theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	colperpex.1	$⊢ φ \to A \in P$
	colperpex.2	$⊢ φ \to B \in P$
	colperpex.3	$⊢ φ \to C \in P$
	colperpex.4	$⊢ φ \to A \neq B$
	colperpex.5	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
Assertion	colperpex	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		colperpex.1	$⊢ φ \to A \in P$
7		colperpex.2	$⊢ φ \to B \in P$
8		colperpex.3	$⊢ φ \to C \in P$
9		colperpex.4	$⊢ φ \to A \neq B$
10		colperpex.5	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
11	5	ad3antrrr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to G \in 𝒢_{Tarski}$
12	6	ad3antrrr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to A \in P$
13	7	ad3antrrr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to B \in P$
14		simplr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to d \in P$
15	9	ad3antrrr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to A \neq B$
16		simpr	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to \neg d \in (A L B)$
17	1 2 3 4 11 12 13 14 15 16	colperpexlem3	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))$
18		simprl	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to (A L p) ⟂_{𝒢} (G) (A L B)$
19	8	ad5antr	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to C \in P$
20		simp-5r	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to C \in (A L B)$
21	20	orcd	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to (C \in (A L B) \lor A = B)$
22	5	ad5antr	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to G \in 𝒢_{Tarski}$
23		simplr	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to p \in P$
24	1 2 3 22 19 23	tgbtwntriv1	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to C \in (C I p)$
25		eleq1	$⊢ t = C \to (t \in (A L B) \leftrightarrow C \in (A L B))$
26	25	orbi1d	$⊢ t = C \to ((t \in (A L B) \lor A = B) \leftrightarrow (C \in (A L B) \lor A = B))$
27		eleq1	$⊢ t = C \to (t \in (C I p) \leftrightarrow C \in (C I p))$
28	26 27	anbi12d	$⊢ t = C \to (((t \in (A L B) \lor A = B) \land t \in (C I p)) \leftrightarrow ((C \in (A L B) \lor A = B) \land C \in (C I p)))$
29	28	rspcev	$⊢ (C \in P \land ((C \in (A L B) \lor A = B) \land C \in (C I p))) \to \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))$
30	19 21 24 29	syl12anc	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))$
31	18 30	jca	$⊢ (((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p)))) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
32	31	ex	$⊢ ((((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \land p \in P) \to (((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p))) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
33	32	reximdva	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to (\exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists s \in P ((s \in (A L B) \lor A = B) \land s \in (d I p))) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
34	17 33	mpd	$⊢ (((φ \land C \in (A L B)) \land d \in P) \land \neg d \in (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
35	5	adantr	$⊢ (φ \land C \in (A L B)) \to G \in 𝒢_{Tarski}$
36	10	adantr	$⊢ (φ \land C \in (A L B)) \to G {Dim}_{𝒢} \geq 2$
37	6	adantr	$⊢ (φ \land C \in (A L B)) \to A \in P$
38	7	adantr	$⊢ (φ \land C \in (A L B)) \to B \in P$
39	9	adantr	$⊢ (φ \land C \in (A L B)) \to A \neq B$
40	1 3 4 35 36 37 38 39	tglowdim2ln	$⊢ (φ \land C \in (A L B)) \to \exists d \in P \neg d \in (A L B)$
41	34 40	r19.29a	$⊢ (φ \land C \in (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
42	5	adantr	$⊢ (φ \land \neg C \in (A L B)) \to G \in 𝒢_{Tarski}$
43	6	adantr	$⊢ (φ \land \neg C \in (A L B)) \to A \in P$
44	7	adantr	$⊢ (φ \land \neg C \in (A L B)) \to B \in P$
45	8	adantr	$⊢ (φ \land \neg C \in (A L B)) \to C \in P$
46	9	adantr	$⊢ (φ \land \neg C \in (A L B)) \to A \neq B$
47		simpr	$⊢ (φ \land \neg C \in (A L B)) \to \neg C \in (A L B)$
48	1 2 3 4 42 43 44 45 46 47	colperpexlem3	$⊢ (φ \land \neg C \in (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
49	41 48	pm2.61dan	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$

Metamath Proof Explorer

Theorem colperpex

Proof