Theorem perpeq 29102

Description: Uniqueness of the perpendicular to a line 𝐴 within a plane 𝐻 at a point 𝑋. Theorem 11.20 of [Schwabhauser] p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026.)

Hypotheses

Ref	Expression
perpeq.1	⊢ 𝑃 = (Base‘𝐺)
perpeq.2	⊢ 𝐿 = (LineG‘𝐺)
perpeq.3	⊢ 𝐸 = (hlG‘𝐺)
perpeq.4	⊢ (𝜑 → 𝐺 ∈ TarskiG)
perpeq.5	⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
perpeq.6	⊢ (𝜑 → 𝐻 ∈ ran 𝐸)
perpeq.7	⊢ (𝜑 → 𝑋 ∈ 𝐴)
perpeq.8	⊢ (𝜑 → 𝐴 ⊆ 𝐻)
perpeq.9	⊢ (𝜑 → 𝑌 ∈ 𝐻)
perpeq.10	⊢ (𝜑 → 𝑍 ∈ 𝐻)
perpeq.11	⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)
perpeq.12	⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)

Assertion

Ref	Expression
perpeq	⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))

Proof of Theorem perpeq

Step	Hyp	Ref	Expression
1		perpeq.1	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		perpeq.2	. . 3 ⊢ 𝐿 = (LineG‘𝐺)
3		perpeq.3	. . 3 ⊢ 𝐸 = (hlG‘𝐺)
4		perpeq.4	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐺 ∈ TarskiG)
6		perpeq.5	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
7	6	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐴 ∈ ran 𝐿)
8		perpeq.6	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ran 𝐸)
9	8	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐻 ∈ ran 𝐸)
10		perpeq.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
11	10	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑋 ∈ 𝐴)
12		perpeq.8	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ 𝐻)
13	12	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐴 ⊆ 𝐻)
14		perpeq.9	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐻)
15	14	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑌 ∈ 𝐻)
16		perpeq.10	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐻)
17	16	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑍 ∈ 𝐻)
18		perpeq.11	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)
19	18	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)
20		perpeq.12	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)
21	20	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑍)(⟂G‘𝐺)𝐴)
22		simpr 489	. . 3 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑌((hpG‘𝐺)‘𝐴)𝑍)
23	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 22	perpeqlem 29101	. 2 ⊢ ((𝜑 ∧ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))
24	4	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐺 ∈ TarskiG)
25	6	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐴 ∈ ran 𝐿)
26	8	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐻 ∈ ran 𝐸)
27	10	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑋 ∈ 𝐴)
28	12	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝐴 ⊆ 𝐻)
29	14	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑌 ∈ 𝐻)
30		eqid 2769	. . . . 5 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
31		eqid 2769	. . . . 5 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
32	12, 10	sseldd 3946	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐻)
33	32	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑋 ∈ 𝐻)
34	16	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑍 ∈ 𝐻)
35	1, 3, 30, 31, 24, 26, 33, 34	mirplncl 29031	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (((pInvG‘𝐺)‘𝑋)‘𝑍) ∈ 𝐻)
36	18	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑌)(⟂G‘𝐺)𝐴)
37		eqid 2769	. . . . . . 7 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
38	1, 2, 37, 4, 6, 10	tglnpt 28780	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
39	1, 37, 2, 3, 4, 8, 16	plngrnssp 29015	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
40	2, 4, 20	perpln1 28945	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ∈ ran 𝐿)
41	1, 37, 2, 4, 38, 39, 40	tglnne 28859	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
42		eqid 2769	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
43	1, 37, 2, 4, 38, 39, 41	tglinerflx1 28864	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑍))
44	1, 37, 2, 4, 38, 39, 41	tglinerflx2 28865	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑍))
45	1, 42, 37, 2, 30, 4, 31, 40, 43, 44	mirln 28911	. . . . . . . 8 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑍) ∈ (𝑋𝐿𝑍))
46	1, 2, 37, 4, 40, 45	tglnpt 28780	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑍) ∈ 𝑃)
47	41	necomd 3019	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≠ 𝑋)
48	1, 42, 37, 2, 30, 4, 38, 31, 39, 47	mirne 28902	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑍) ≠ 𝑋)
49	1, 37, 2, 4, 38, 39, 41, 46, 48, 45	tglineelsb2 28863	. . . . . 6 ⊢ (𝜑 → (𝑋𝐿𝑍) = (𝑋𝐿(((pInvG‘𝐺)‘𝑋)‘𝑍)))
50	49, 20	breq1dd 5128	. . . . 5 ⊢ (𝜑 → (𝑋𝐿(((pInvG‘𝐺)‘𝑋)‘𝑍))(⟂G‘𝐺)𝐴)
51	50	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿(((pInvG‘𝐺)‘𝑋)‘𝑍))(⟂G‘𝐺)𝐴)
52	1, 37, 2, 3, 4, 8, 14	plngrnssp 29015	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
53	1, 42, 37, 2, 4, 6, 10, 52, 18	footne 28958	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐴)
54	52, 53	eldifd 3924	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ 𝐴))
55	54	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑌 ∈ (𝑃 ∖ 𝐴))
56	14, 53	eldifd 3924	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝐻 ∖ 𝐴))
57	1, 2, 3, 4, 8, 6, 56, 12	plng3p 29033	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝐴𝐸𝑌))
58	16, 57	eleqtrd 2871	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝐴𝐸𝑌))
59	1, 42, 37, 2, 4, 6, 10, 39, 20	footne 28958	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝐴)
60	58, 59	eldifd 3924	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ ((𝐴𝐸𝑌) ∖ 𝐴))
61	60	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑍 ∈ ((𝐴𝐸𝑌) ∖ 𝐴))
62		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍)
63	1, 2, 30, 3, 31, 24, 25, 27, 55, 61, 62	nhpmirhp 29034	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → 𝑌((hpG‘𝐺)‘𝐴)(((pInvG‘𝐺)‘𝑋)‘𝑍))
64	1, 2, 3, 24, 25, 26, 27, 28, 29, 35, 36, 51, 63	perpeqlem 29101	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑌) = (𝑋𝐿(((pInvG‘𝐺)‘𝑋)‘𝑍)))
65	49	adantr 485	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑍) = (𝑋𝐿(((pInvG‘𝐺)‘𝑋)‘𝑍)))
66	64, 65	eqtr4d 2807	. 2 ⊢ ((𝜑 ∧ ¬ 𝑌((hpG‘𝐺)‘𝐴)𝑍) → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))
67	23, 66	pm2.61dan 824	1 ⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑋𝐿𝑍))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ∖ cdif 3910   ⊆ wss 3913   class class class wbr 5110  ran crn 5660  ‘cfv 6533  (class class class)co 7408  Basecbs 17265  distcds 17315  TarskiGcstrkg 28658  Itvcitv 28664  LineGclng 28665  pInvGcmir 28887  ⟂Gcperpg 28930  hpGchpg 28994  hlGcplng 29009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-oadd 8453  df-er 8690  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9883  df-card 9921  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-2 12299  df-3 12300  df-n0 12501  df-xnn0 12574  df-z 12588  df-uz 12859  df-fz 13532  df-fzo 13679  df-hash 14363  df-word 14547  df-concat 14604  df-s1 14630  df-s2 14881  df-s3 14882  df-trkgc 28679  df-trkgb 28680  df-trkgcb 28681  df-trkgld 28683  df-trkg 28684  df-cgrg 28742  df-ismt 28764  df-leg 28814  df-hlg 28832  df-mir 28888  df-rag 28929  df-perpg 28931  df-hpg 28995  df-plng 29010  df-mid 29037  df-lmi 29038  df-cgra 29072

This theorem is referenced by:  perpprlng  29149