Metamath Proof Explorer

Theorem perpeqlem

Description: Lemma for perpeq . (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 )
perpeqlem.1 
|- ( ph -> Y ( ( hpG ` G ) ` A ) Z )
Assertion perpeqlem 
|- ( 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 perpeqlem.1 
 |-  ( ph -> Y ( ( hpG ` G ) ` A ) Z )
14 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
15 4 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> G e. TarskiG )
16 1 2 14 4 5 7 tglnpt 
 |-  ( ph -> X e. P )
17 16 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X e. P )
18 1 14 2 3 4 6 9 plngrnssp 
 |-  ( ph -> Y e. P )
19 18 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y e. P )
20 2 4 11 perpln1 
 |-  ( ph -> ( X L Y ) e. ran L )
21 1 14 2 4 16 18 20 tglnne 
 |-  ( ph -> X =/= Y )
22 21 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X =/= Y )
23 2 4 12 perpln1 
 |-  ( ph -> ( X L Z ) e. ran L )
24 23 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Z ) e. ran L )
25 1 14 2 3 4 6 10 plngrnssp 
 |-  ( ph -> Z e. P )
26 1 14 2 4 16 25 23 tglnne 
 |-  ( ph -> X =/= Z )
27 26 necomd 
 |-  ( ph -> Z =/= X )
28 1 14 2 4 25 16 27 tglinerflx2 
 |-  ( ph -> X e. ( Z L X ) )
29 1 14 2 4 16 25 26 tglinecom 
 |-  ( ph -> ( X L Z ) = ( Z L X ) )
30 28 29 eleqtrrd 
 |-  ( ph -> X e. ( X L Z ) )
31 30 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X e. ( X L Z ) )
32 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
33 25 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Z e. P )
34 5 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> A e. ran L )
35 simplr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> t e. ( A \ ( X L Y ) ) )
36 35 eldifad 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> t e. A )
37 1 2 14 15 34 36 tglnpt 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> t e. P )
38 simpr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> t =/= X )
39 38 necomd 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X =/= t )
40 eqid 
 |-  ( dist ` G ) = ( dist ` G )
41 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
42 21 necomd 
 |-  ( ph -> Y =/= X )
43 1 14 2 4 18 16 42 tglinerflx2 
 |-  ( ph -> X e. ( Y L X ) )
44 43 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X e. ( Y L X ) )
45 11 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Y ) ( perpG ` G ) A )
46 1 14 2 15 17 19 22 tglinecom 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Y ) = ( Y L X ) )
47 7 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X e. A )
48 1 14 2 15 17 37 39 39 34 47 36 tglinethru 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> A = ( X L t ) )
49 45 46 48 3brtr3d 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( Y L X ) ( perpG ` G ) ( X L t ) )
50 1 40 14 2 15 19 17 44 37 49 perprag 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> <" Y X t "> e. ( raG ` G ) )
51 1 40 14 2 41 15 19 17 37 50 ragcom 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> <" t X Y "> e. ( raG ` G ) )
52 28 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> X e. ( Z L X ) )
53 29 12 eqbrtrrd 
 |-  ( ph -> ( Z L X ) ( perpG ` G ) A )
54 53 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( Z L X ) ( perpG ` G ) A )
55 54 48 breqtrd 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( Z L X ) ( perpG ` G ) ( X L t ) )
56 1 40 14 2 15 33 17 52 37 55 perprag 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> <" Z X t "> e. ( raG ` G ) )
57 1 40 14 2 41 15 33 17 37 56 ragcom 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> <" t X Z "> e. ( raG ` G ) )
58 1 14 2 15 37 17 38 38 34 36 47 tglinethru 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> A = ( t L X ) )
59 58 fveq2d 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( ( hpG ` G ) ` A ) = ( ( hpG ` G ) ` ( t L X ) ) )
60 13 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y ( ( hpG ` G ) ` A ) Z )
61 59 60 breqdi 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y ( ( hpG ` G ) ` ( t L X ) ) Z )
62 1 2 15 17 37 19 33 39 51 57 61 ragraghl 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y ( ( hlG ` G ) ` X ) Z )
63 1 14 32 19 33 17 15 2 62 hlln 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y e. ( Z L X ) )
64 29 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Z ) = ( Z L X ) )
65 63 64 eleqtrrd 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> Y e. ( X L Z ) )
66 1 14 2 15 17 19 22 22 24 31 65 tglinethru 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Z ) = ( X L Y ) )
67 66 eqcomd 
 |-  ( ( ( ph /\ t e. ( A \ ( X L Y ) ) ) /\ t =/= X ) -> ( X L Y ) = ( X L Z ) )
68 1 40 14 2 4 20 5 11 perpneq 
 |-  ( ph -> ( X L Y ) =/= A )
69 68 necomd 
 |-  ( ph -> A =/= ( X L Y ) )
70 1 14 2 4 5 20 7 69 tglnpt4 
 |-  ( ph -> E. t e. ( A \ ( X L Y ) ) t =/= X )
71 67 70 r19.29a 
 |-  ( ph -> ( X L Y ) = ( X L Z ) )