Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( 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 perpeq ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 𝐿 𝑍 ) )

Proof

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