perpeq

Description: Uniqueness of the perpendicular to a line A within a plane H at a point X . Theorem 11.20 of Schwabhauser p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	perpeq.1	$⊢ P = {Base}_{G}$
	perpeq.2	$⊢ L = {Line}_{𝒢} (G)$
	perpeq.3	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	perpeq.4	$⊢ φ \to G \in 𝒢_{Tarski}$
	perpeq.5	$⊢ φ \to A \in ran L$
	perpeq.6	$⊢ φ \to H \in ran E$
	perpeq.7	$⊢ φ \to X \in A$
	perpeq.8	$⊢ φ \to A \subseteq H$
	perpeq.9	$⊢ φ \to Y \in H$
	perpeq.10	$⊢ φ \to Z \in H$
	perpeq.11	$⊢ φ \to (X L Y) ⟂_{𝒢} (G) A$
	perpeq.12	$⊢ φ \to (X L Z) ⟂_{𝒢} (G) A$
Assertion	perpeq	$⊢ φ \to X L Y = X L Z$

Proof

Step	Hyp	Ref	Expression
1		perpeq.1	$⊢ P = {Base}_{G}$
2		perpeq.2	$⊢ L = {Line}_{𝒢} (G)$
3		perpeq.3	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		perpeq.4	$⊢ φ \to G \in 𝒢_{Tarski}$
5		perpeq.5	$⊢ φ \to A \in ran L$
6		perpeq.6	$⊢ φ \to H \in ran E$
7		perpeq.7	$⊢ φ \to X \in A$
8		perpeq.8	$⊢ φ \to A \subseteq H$
9		perpeq.9	$⊢ φ \to Y \in H$
10		perpeq.10	$⊢ φ \to Z \in H$
11		perpeq.11	$⊢ φ \to (X L Y) ⟂_{𝒢} (G) A$
12		perpeq.12	$⊢ φ \to (X L Z) ⟂_{𝒢} (G) A$
13	4	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to G \in 𝒢_{Tarski}$
14	5	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to A \in ran L$
15	6	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to H \in ran E$
16	7	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to X \in A$
17	8	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to A \subseteq H$
18	9	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to Y \in H$
19	10	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to Z \in H$
20	11	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to (X L Y) ⟂_{𝒢} (G) A$
21	12	adantr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to (X L Z) ⟂_{𝒢} (G) A$
22		simpr	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to Y {hp}_{𝒢} (G) (A) Z$
23	1 2 3 13 14 15 16 17 18 19 20 21 22	perpeqlem	$⊢ (φ \land Y {hp}_{𝒢} (G) (A) Z) \to X L Y = X L Z$
24	4	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to G \in 𝒢_{Tarski}$
25	5	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to A \in ran L$
26	6	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to H \in ran E$
27	7	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to X \in A$
28	8	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to A \subseteq H$
29	9	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to Y \in H$
30		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
31		eqid	$⊢ {pInv}_{𝒢} (G) (X) = {pInv}_{𝒢} (G) (X)$
32	8 7	sseldd	$⊢ φ \to X \in H$
33	32	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to X \in H$
34	10	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to Z \in H$
35	1 3 30 31 24 26 33 34	mirplncl	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to {pInv}_{𝒢} (G) (X) (Z) \in H$
36	11	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to (X L Y) ⟂_{𝒢} (G) A$
37		eqid	$⊢ Itv (G) = Itv (G)$
38	1 2 37 4 5 7	tglnpt	$⊢ φ \to X \in P$
39	1 37 2 3 4 6 10	plngrnssp	$⊢ φ \to Z \in P$
40	2 4 12	perpln1	$⊢ φ \to X L Z \in ran L$
41	1 37 2 4 38 39 40	tglnne	$⊢ φ \to X \neq Z$
42		eqid	$⊢ dist (G) = dist (G)$
43	1 37 2 4 38 39 41	tglinerflx1	$⊢ φ \to X \in (X L Z)$
44	1 37 2 4 38 39 41	tglinerflx2	$⊢ φ \to Z \in (X L Z)$
45	1 42 37 2 30 4 31 40 43 44	mirln	$⊢ φ \to {pInv}_{𝒢} (G) (X) (Z) \in (X L Z)$
46	1 2 37 4 40 45	tglnpt	$⊢ φ \to {pInv}_{𝒢} (G) (X) (Z) \in P$
47	41	necomd	$⊢ φ \to Z \neq X$
48	1 42 37 2 30 4 38 31 39 47	mirne	$⊢ φ \to {pInv}_{𝒢} (G) (X) (Z) \neq X$
49	1 37 2 4 38 39 41 46 48 45	tglineelsb2	$⊢ φ \to X L Z = X L {pInv}_{𝒢} (G) (X) (Z)$
50	49 12	breq1dd	$⊢ φ \to (X L {pInv}_{𝒢} (G) (X) (Z)) ⟂_{𝒢} (G) A$
51	50	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to (X L {pInv}_{𝒢} (G) (X) (Z)) ⟂_{𝒢} (G) A$
52	1 37 2 3 4 6 9	plngrnssp	$⊢ φ \to Y \in P$
53	1 42 37 2 4 5 7 52 11	footne	$⊢ φ \to \neg Y \in A$
54	52 53	eldifd	$⊢ φ \to Y \in (P ∖ A)$
55	54	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to Y \in (P ∖ A)$
56	9 53	eldifd	$⊢ φ \to Y \in (H ∖ A)$
57	1 2 3 4 6 5 56 8	plng3p	$⊢ φ \to H = A E Y$
58	10 57	eleqtrd	$⊢ φ \to Z \in (A E Y)$
59	1 42 37 2 4 5 7 39 12	footne	$⊢ φ \to \neg Z \in A$
60	58 59	eldifd	$⊢ φ \to Z \in ((A E Y) ∖ A)$
61	60	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to Z \in ((A E Y) ∖ A)$
62		simpr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to \neg Y {hp}_{𝒢} (G) (A) Z$
63	1 2 30 3 31 24 25 27 55 61 62	nhpmirhp	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to Y {hp}_{𝒢} (G) (A) {pInv}_{𝒢} (G) (X) (Z)$
64	1 2 3 24 25 26 27 28 29 35 36 51 63	perpeqlem	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to X L Y = X L {pInv}_{𝒢} (G) (X) (Z)$
65	49	adantr	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to X L Z = X L {pInv}_{𝒢} (G) (X) (Z)$
66	64 65	eqtr4d	$⊢ (φ \land \neg Y {hp}_{𝒢} (G) (A) Z) \to X L Y = X L Z$
67	23 66	pm2.61dan	$⊢ φ \to X L Y = X L Z$

Metamath Proof Explorer

Theorem perpeq

Proof