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 
|- P = ( Base ` G )
perpeq.2 
|- L = ( LineG ` G )
perpeq.3 
|- E = ( PlnG ` G )
perpeq.4 
|- ( ph -> G e. TarskiG )
perpeq.5 
|- ( ph -> A e. ran L )
perpeq.6 
|- ( ph -> H e. ran E )
perpeq.7 
|- ( ph -> X e. A )
perpeq.8 
|- ( ph -> A C_ H )
perpeq.9 
|- ( ph -> Y e. H )
perpeq.10 
|- ( ph -> Z e. H )
perpeq.11 
|- ( ph -> ( X L Y ) ( perpG ` G ) A )
perpeq.12 
|- ( ph -> ( X L Z ) ( perpG ` G ) A )
Assertion perpeq 
|- ( ph -> ( X L Y ) = ( X L Z ) )

Proof

Step Hyp Ref Expression
1 perpeq.1 
 |-  P = ( Base ` G )
2 perpeq.2 
 |-  L = ( LineG ` G )
3 perpeq.3 
 |-  E = ( PlnG ` G )
4 perpeq.4 
 |-  ( ph -> G e. TarskiG )
5 perpeq.5 
 |-  ( ph -> A e. ran L )
6 perpeq.6 
 |-  ( ph -> H e. ran E )
7 perpeq.7 
 |-  ( ph -> X e. A )
8 perpeq.8 
 |-  ( ph -> A C_ H )
9 perpeq.9 
 |-  ( ph -> Y e. H )
10 perpeq.10 
 |-  ( ph -> Z e. H )
11 perpeq.11 
 |-  ( ph -> ( X L Y ) ( perpG ` G ) A )
12 perpeq.12 
 |-  ( ph -> ( X L Z ) ( perpG ` G ) A )
13 4 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> G e. TarskiG )
14 5 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> A e. ran L )
15 6 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> H e. ran E )
16 7 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> X e. A )
17 8 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> A C_ H )
18 9 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> Y e. H )
19 10 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> Z e. H )
20 11 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Y ) ( perpG ` G ) A )
21 12 adantr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Z ) ( perpG ` G ) A )
22 simpr 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> Y ( ( hpG ` G ) ` A ) Z )
23 1 2 3 13 14 15 16 17 18 19 20 21 22 perpeqlem 
 |-  ( ( ph /\ Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Y ) = ( X L Z ) )
24 4 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> G e. TarskiG )
25 5 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> A e. ran L )
26 6 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> H e. ran E )
27 7 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> X e. A )
28 8 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> A C_ H )
29 9 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> Y e. H )
30 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
31 eqid 
 |-  ( ( pInvG ` G ) ` X ) = ( ( pInvG ` G ) ` X )
32 8 7 sseldd 
 |-  ( ph -> X e. H )
33 32 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> X e. H )
34 10 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> Z e. H )
35 1 3 30 31 24 26 33 34 mirplncl 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( ( ( pInvG ` G ) ` X ) ` Z ) e. H )
36 11 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Y ) ( perpG ` G ) A )
37 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
38 1 2 37 4 5 7 tglnpt 
 |-  ( ph -> X e. P )
39 1 37 2 3 4 6 10 plngrnssp 
 |-  ( ph -> Z e. P )
40 2 4 12 perpln1 
 |-  ( ph -> ( X L Z ) e. ran L )
41 1 37 2 4 38 39 40 tglnne 
 |-  ( ph -> X =/= Z )
42 eqid 
 |-  ( dist ` G ) = ( dist ` G )
43 1 37 2 4 38 39 41 tglinerflx1 
 |-  ( ph -> X e. ( X L Z ) )
44 1 37 2 4 38 39 41 tglinerflx2 
 |-  ( ph -> Z e. ( X L Z ) )
45 1 42 37 2 30 4 31 40 43 44 mirln 
 |-  ( ph -> ( ( ( pInvG ` G ) ` X ) ` Z ) e. ( X L Z ) )
46 1 2 37 4 40 45 tglnpt 
 |-  ( ph -> ( ( ( pInvG ` G ) ` X ) ` Z ) e. P )
47 41 necomd 
 |-  ( ph -> Z =/= X )
48 1 42 37 2 30 4 38 31 39 47 mirne 
 |-  ( ph -> ( ( ( pInvG ` G ) ` X ) ` Z ) =/= X )
49 1 37 2 4 38 39 41 46 48 45 tglineelsb2 
 |-  ( ph -> ( X L Z ) = ( X L ( ( ( pInvG ` G ) ` X ) ` Z ) ) )
50 49 12 breq1dd 
 |-  ( ph -> ( X L ( ( ( pInvG ` G ) ` X ) ` Z ) ) ( perpG ` G ) A )
51 50 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( X L ( ( ( pInvG ` G ) ` X ) ` Z ) ) ( perpG ` G ) A )
52 1 37 2 3 4 6 9 plngrnssp 
 |-  ( ph -> Y e. P )
53 1 42 37 2 4 5 7 52 11 footne 
 |-  ( ph -> -. Y e. A )
54 52 53 eldifd 
 |-  ( ph -> Y e. ( P \ A ) )
55 54 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> Y e. ( P \ A ) )
56 9 53 eldifd 
 |-  ( ph -> Y e. ( H \ A ) )
57 1 2 3 4 6 5 56 8 plng3p 
 |-  ( ph -> H = ( A E Y ) )
58 10 57 eleqtrd 
 |-  ( ph -> Z e. ( A E Y ) )
59 1 42 37 2 4 5 7 39 12 footne 
 |-  ( ph -> -. Z e. A )
60 58 59 eldifd 
 |-  ( ph -> Z e. ( ( A E Y ) \ A ) )
61 60 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> Z e. ( ( A E Y ) \ A ) )
62 simpr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> -. Y ( ( hpG ` G ) ` A ) Z )
63 1 2 30 3 31 24 25 27 55 61 62 nhpmirhp 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> Y ( ( hpG ` G ) ` A ) ( ( ( pInvG ` G ) ` X ) ` Z ) )
64 1 2 3 24 25 26 27 28 29 35 36 51 63 perpeqlem 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Y ) = ( X L ( ( ( pInvG ` G ) ` X ) ` Z ) ) )
65 49 adantr 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Z ) = ( X L ( ( ( pInvG ` G ) ` X ) ` Z ) ) )
66 64 65 eqtr4d 
 |-  ( ( ph /\ -. Y ( ( hpG ` G ) ` A ) Z ) -> ( X L Y ) = ( X L Z ) )
67 23 66 pm2.61dan 
 |-  ( ph -> ( X L Y ) = ( X L Z ) )