Metamath Proof Explorer

Theorem tgaaddcpbl

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Theorem 11.22 of Schwabhauser p. 99. The angles <" X Y S "> and <" S Y Z "> are added to result in <" X Y Z "> , and <" U V T "> and <" T V W "> are added to result in <" U V W "> . (Contributed by Thierry Arnoux, 2-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl.p 
|- P = ( Base ` G )
tgaaddcpbl.i 
|- I = ( Itv ` G )
tgaaddcpbl.l 
|- L = ( LineG ` G )
tgaaddcpbl.c 
|- .~ = ( cgrA ` G )
tgaaddcpbl.o 
|- O = { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) }
tgaaddcpbl.q 
|- Q = { <. c , d >. | ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) /\ E. t e. ( V L T ) t e. ( c I d ) ) }
tgaaddcpbl.1 
|- ( ph -> G e. TarskiG )
tgaaddcpbl.s 
|- ( ph -> S e. P )
tgaaddcpbl.t 
|- ( ph -> T e. P )
tgaaddcpbl.u 
|- ( ph -> U e. P )
tgaaddcpbl.v 
|- ( ph -> V e. P )
tgaaddcpbl.w 
|- ( ph -> W e. P )
tgaaddcpbl.x 
|- ( ph -> X e. P )
tgaaddcpbl.y 
|- ( ph -> Y e. P )
tgaaddcpbl.z 
|- ( ph -> Z e. P )
tgaaddcpbl.2 
|- ( ph -> Y =/= S )
tgaaddcpbl.3 
|- ( ph -> V =/= T )
tgaaddcpbl.4 
|- ( ph -> X O Z )
tgaaddcpbl.5 
|- ( ph -> U Q W )
tgaaddcpbl.6 
|- ( ph -> <" X Y S "> .~ <" U V T "> )
tgaaddcpbl.7 
|- ( ph -> <" S Y Z "> .~ <" T V W "> )
Assertion tgaaddcpbl 
|- ( ph -> <" X Y Z "> .~ <" U V W "> )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl.p 
 |-  P = ( Base ` G )
2 tgaaddcpbl.i 
 |-  I = ( Itv ` G )
3 tgaaddcpbl.l 
 |-  L = ( LineG ` G )
4 tgaaddcpbl.c 
 |-  .~ = ( cgrA ` G )
5 tgaaddcpbl.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( Y L S ) ) /\ b e. ( P \ ( Y L S ) ) ) /\ E. s e. ( Y L S ) s e. ( a I b ) ) }
6 tgaaddcpbl.q 
 |-  Q = { <. c , d >. | ( ( c e. ( P \ ( V L T ) ) /\ d e. ( P \ ( V L T ) ) ) /\ E. t e. ( V L T ) t e. ( c I d ) ) }
7 tgaaddcpbl.1 
 |-  ( ph -> G e. TarskiG )
8 tgaaddcpbl.s 
 |-  ( ph -> S e. P )
9 tgaaddcpbl.t 
 |-  ( ph -> T e. P )
10 tgaaddcpbl.u 
 |-  ( ph -> U e. P )
11 tgaaddcpbl.v 
 |-  ( ph -> V e. P )
12 tgaaddcpbl.w 
 |-  ( ph -> W e. P )
13 tgaaddcpbl.x 
 |-  ( ph -> X e. P )
14 tgaaddcpbl.y 
 |-  ( ph -> Y e. P )
15 tgaaddcpbl.z 
 |-  ( ph -> Z e. P )
16 tgaaddcpbl.2 
 |-  ( ph -> Y =/= S )
17 tgaaddcpbl.3 
 |-  ( ph -> V =/= T )
18 tgaaddcpbl.4 
 |-  ( ph -> X O Z )
19 tgaaddcpbl.5 
 |-  ( ph -> U Q W )
20 tgaaddcpbl.6 
 |-  ( ph -> <" X Y S "> .~ <" U V T "> )
21 tgaaddcpbl.7 
 |-  ( ph -> <" S Y Z "> .~ <" T V W "> )
22 4 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> .~ = ( cgrA ` G ) )
23 22 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( cgrA ` G ) = .~ )
24 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
25 7 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> G e. TarskiG )
26 25 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> G e. TarskiG )
27 13 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> X e. P )
28 14 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> Y e. P )
29 28 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> Y e. P )
30 15 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> Z e. P )
31 30 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> Z e. P )
32 10 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> U e. P )
33 11 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> V e. P )
34 33 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> V e. P )
35 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> w e. P )
36 eqid 
 |-  ( dist ` G ) = ( dist ` G )
37 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> Y e. ( X I Z ) )
38 simpllr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> u e. P )
39 38 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> u e. P )
40 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> u ( ( hlG ` G ) ` V ) U )
41 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> V e. ( u I w ) )
42 1 2 24 39 32 35 26 34 40 41 btwnhl 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> V e. ( U I w ) )
43 1 2 3 7 14 8 16 tglinerflx1 
 |-  ( ph -> Y e. ( Y L S ) )
44 1 2 3 7 14 8 16 tgelrnln 
 |-  ( ph -> ( Y L S ) e. ran L )
45 1 36 2 5 3 44 7 13 15 18 oppne1 
 |-  ( ph -> -. X e. ( Y L S ) )
46 nelne2 
 |-  ( ( Y e. ( Y L S ) /\ -. X e. ( Y L S ) ) -> Y =/= X )
47 43 45 46 syl2anc 
 |-  ( ph -> Y =/= X )
48 47 necomd 
 |-  ( ph -> X =/= Y )
49 48 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> X =/= Y )
50 1 36 2 5 3 44 7 13 15 18 oppne2 
 |-  ( ph -> -. Z e. ( Y L S ) )
51 nelne2 
 |-  ( ( Y e. ( Y L S ) /\ -. Z e. ( Y L S ) ) -> Y =/= Z )
52 43 50 51 syl2anc 
 |-  ( ph -> Y =/= Z )
53 52 necomd 
 |-  ( ph -> Z =/= Y )
54 53 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> Z =/= Y )
55 1 2 3 7 11 9 17 tglinerflx1 
 |-  ( ph -> V e. ( V L T ) )
56 1 36 2 6 10 12 islnopp 
 |-  ( ph -> ( U Q W <-> ( ( -. U e. ( V L T ) /\ -. W e. ( V L T ) ) /\ E. t e. ( V L T ) t e. ( U I W ) ) ) )
57 19 56 mpbid 
 |-  ( ph -> ( ( -. U e. ( V L T ) /\ -. W e. ( V L T ) ) /\ E. t e. ( V L T ) t e. ( U I W ) ) )
58 57 simplld 
 |-  ( ph -> -. U e. ( V L T ) )
59 nelne2 
 |-  ( ( V e. ( V L T ) /\ -. U e. ( V L T ) ) -> V =/= U )
60 55 58 59 syl2anc 
 |-  ( ph -> V =/= U )
61 60 necomd 
 |-  ( ph -> U =/= V )
62 61 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> U =/= V )
63 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) )
64 63 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) Z ) = ( V ( dist ` G ) w ) )
65 52 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> Y =/= Z )
66 1 36 2 26 29 31 34 35 64 65 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> V =/= w )
67 66 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> w =/= V )
68 1 2 36 26 27 29 31 32 34 35 37 42 49 54 62 67 flatcgra 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V w "> )
69 12 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> W e. P )
70 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> S e. P )
71 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> T e. P )
72 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
73 eqid 
 |-  ( ( pInvG ` G ) ` T ) = ( ( pInvG ` G ) ` T )
74 1 36 2 3 72 7 9 73 10 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
75 74 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
76 7 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> G e. TarskiG )
77 14 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y e. P )
78 8 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. P )
79 15 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z e. P )
80 16 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y =/= S )
81 simpr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. ( Y L Z ) )
82 52 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y =/= Z )
83 1 2 3 76 77 79 82 tglinecom 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> ( Y L Z ) = ( Z L Y ) )
84 81 83 eleqtrd 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. ( Z L Y ) )
85 53 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z =/= Y )
86 1 2 3 76 77 78 79 80 84 85 lnrot1 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z e. ( Y L S ) )
87 50 86 mtand 
 |-  ( ph -> -. S e. ( Y L Z ) )
88 52 neneqd 
 |-  ( ph -> -. Y = Z )
89 ioran 
 |-  ( -. ( S e. ( Y L Z ) \/ Y = Z ) <-> ( -. S e. ( Y L Z ) /\ -. Y = Z ) )
90 87 88 89 sylanbrc 
 |-  ( ph -> -. ( S e. ( Y L Z ) \/ Y = Z ) )
91 90 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> -. ( S e. ( Y L Z ) \/ Y = Z ) )
92 7 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> G e. TarskiG )
93 9 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> T e. P )
94 10 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> U e. P )
95 1 36 2 3 72 92 93 73 94 mirmir 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` ( ( ( pInvG ` G ) ` T ) ` U ) ) = U )
96 1 2 3 7 11 9 17 tgelrnln 
 |-  ( ph -> ( V L T ) e. ran L )
97 96 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( V L T ) e. ran L )
98 1 2 3 7 11 9 17 tglinerflx2 
 |-  ( ph -> T e. ( V L T ) )
99 98 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> T e. ( V L T ) )
100 74 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
101 11 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> V e. P )
102 simpr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) )
103 1 3 2 92 101 100 93 102 colcom 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( T e. ( ( ( ( pInvG ` G ) ` T ) ` U ) L V ) \/ ( ( ( pInvG ` G ) ` T ) ` U ) = V ) )
104 1 3 2 92 100 101 93 103 colrot1 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( ( pInvG ` G ) ` T ) ` U ) e. ( V L T ) \/ V = T ) )
105 17 neneqd 
 |-  ( ph -> -. V = T )
106 105 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> -. V = T )
107 104 106 olcnd 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. ( V L T ) )
108 1 36 2 3 72 92 73 97 99 107 mirln 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` ( ( ( pInvG ` G ) ` T ) ` U ) ) e. ( V L T ) )
109 95 108 eqeltrrd 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> U e. ( V L T ) )
110 58 109 mtand 
 |-  ( ph -> -. ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) )
111 110 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> -. ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) )
112 4 a1i 
 |-  ( ph -> .~ = ( cgrA ` G ) )
113 112 21 breqdi 
 |-  ( ph -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
114 113 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
115 112 20 breqdi 
 |-  ( ph -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
116 1 2 7 24 13 14 8 10 11 9 115 cgracom 
 |-  ( ph -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
117 116 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
118 1 2 36 26 32 34 71 27 29 70 35 31 117 42 37 66 65 sacgr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" w V T "> ( cgrA ` G ) <" Z Y S "> )
119 1 2 36 26 35 34 71 31 29 70 118 cgraswaplr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" T V w "> ( cgrA ` G ) <" S Y Z "> )
120 1 2 26 24 71 34 35 70 29 31 119 cgracom 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V w "> )
121 1 2 3 7 11 9 17 tglinecom 
 |-  ( ph -> ( V L T ) = ( T L V ) )
122 121 fveq2d 
 |-  ( ph -> ( ( hpG ` G ) ` ( V L T ) ) = ( ( hpG ` G ) ` ( T L V ) ) )
123 10 58 eldifd 
 |-  ( ph -> U e. ( P \ ( V L T ) ) )
124 1 2 72 73 6 7 96 98 123 3 oppmir 
 |-  ( ph -> U Q ( ( ( pInvG ` G ) ` T ) ` U ) )
125 1 36 2 6 3 96 7 10 74 124 oppcom 
 |-  ( ph -> ( ( ( pInvG ` G ) ` T ) ` U ) Q U )
126 1 36 2 6 3 96 7 10 12 19 oppcom 
 |-  ( ph -> W Q U )
127 1 2 3 6 7 96 12 74 10 126 lnopp2hpgb 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` T ) ` U ) Q U <-> W ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) ) )
128 125 127 mpbid 
 |-  ( ph -> W ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
129 122 128 breqdi 
 |-  ( ph -> W ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
130 129 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> W ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
131 122 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( ( hpG ` G ) ` ( V L T ) ) = ( ( hpG ` G ) ` ( T L V ) ) )
132 125 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) Q U )
133 96 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( V L T ) e. ran L )
134 55 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> V e. ( V L T ) )
135 25 adantr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> G e. TarskiG )
136 33 adantr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> V e. P )
137 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> T e. P )
138 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> U e. P )
139 17 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> V =/= T )
140 38 adantr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> u e. P )
141 13 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> X e. P )
142 simpr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) )
143 142 eqcomd 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> ( Y ( dist ` G ) X ) = ( V ( dist ` G ) u ) )
144 47 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> Y =/= X )
145 1 36 2 25 28 141 33 38 143 144 tgcgrneq 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> V =/= u )
146 145 necomd 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> u =/= V )
147 146 adantr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> u =/= V )
148 simpr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> u e. ( V L T ) )
149 1 2 3 135 140 136 137 147 148 139 lnrot2 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> T e. ( u L V ) )
150 61 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> U =/= V )
151 1 2 3 135 140 136 147 tgelrnln 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> ( u L V ) e. ran L )
152 10 ad4antr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> U e. P )
153 simplr 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> u ( ( hlG ` G ) ` V ) U )
154 1 2 24 38 152 33 25 153 hlcomd 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> U ( ( hlG ` G ) ` V ) u )
155 1 2 24 152 38 33 25 3 154 hlln 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> U e. ( u L V ) )
156 155 adantr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> U e. ( u L V ) )
157 1 2 3 135 140 136 147 tglinerflx2 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> V e. ( u L V ) )
158 1 2 3 135 138 136 150 150 151 156 157 tglinethru 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> ( u L V ) = ( U L V ) )
159 149 158 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> T e. ( U L V ) )
160 1 2 3 135 136 137 138 139 159 150 lnrot1 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> U e. ( V L T ) )
161 58 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ u e. ( V L T ) ) -> -. U e. ( V L T ) )
162 160 161 pm2.65da 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> -. u e. ( V L T ) )
163 162 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> -. u e. ( V L T ) )
164 66 neneqd 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> -. V = w )
165 26 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> G e. TarskiG )
166 39 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> u e. P )
167 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. P )
168 26 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> G e. TarskiG )
169 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> w e. P )
170 34 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> V e. P )
171 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> V e. ( u I w ) )
172 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> u = w )
173 172 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> ( u I w ) = ( w I w ) )
174 171 173 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> V e. ( w I w ) )
175 1 36 2 168 169 170 174 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> w = V )
176 175 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ u = w ) -> V = w )
177 66 176 mteqand 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> u =/= w )
178 177 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> u =/= w )
179 1 2 3 165 166 167 178 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( u L w ) e. ran L )
180 133 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( V L T ) e. ran L )
181 1 2 3 165 166 167 178 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> u e. ( u L w ) )
182 163 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> -. u e. ( V L T ) )
183 nelne1 
 |-  ( ( u e. ( u L w ) /\ -. u e. ( V L T ) ) -> ( u L w ) =/= ( V L T ) )
184 181 182 183 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( u L w ) =/= ( V L T ) )
185 34 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V e. P )
186 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V e. ( u I w ) )
187 1 2 3 165 166 167 185 178 186 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V e. ( u L w ) )
188 134 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V e. ( V L T ) )
189 187 188 elind 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V e. ( ( u L w ) i^i ( V L T ) ) )
190 1 2 3 165 166 167 178 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( u L w ) )
191 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( V L T ) )
192 190 191 elind 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( ( u L w ) i^i ( V L T ) ) )
193 1 2 3 165 179 180 184 189 192 tglineineq 
 |-  ( ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> V = w )
194 164 193 mtand 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> -. w e. ( V L T ) )
195 1 36 2 6 39 35 134 163 194 41 islnoppd 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> u Q w )
196 1 36 2 6 3 133 26 24 39 32 35 195 134 40 opphl 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> U Q w )
197 1 36 2 6 3 133 26 32 35 196 oppcom 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> w Q U )
198 1 2 3 6 26 133 35 75 32 197 lnopp2hpgb 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> ( ( ( ( pInvG ` G ) ` T ) ` U ) Q U <-> w ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) ) )
199 132 198 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> w ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
200 131 199 breqdi 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> w ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
201 1 2 36 26 70 29 31 71 34 75 3 91 111 69 35 24 114 120 130 200 acopyeu 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> W ( ( hlG ` G ) ` V ) w )
202 1 2 24 26 27 29 31 32 34 35 68 69 201 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
203 23 202 breqdi 
 |-  ( ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ V e. ( u I w ) ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> .~ <" U V W "> )
204 203 anasss 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ w e. P ) /\ ( V e. ( u I w ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) ) -> <" X Y Z "> .~ <" U V W "> )
205 1 36 2 25 38 33 28 30 axtgsegcon 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> E. w e. P ( V e. ( u I w ) /\ ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) ) )
206 204 205 r19.29a 
 |-  ( ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ u ( ( hlG ` G ) ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> <" X Y Z "> .~ <" U V W "> )
207 206 anasss 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ u e. P ) /\ ( u ( ( hlG ` G ) ` V ) U /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) ) -> <" X Y Z "> .~ <" U V W "> )
208 1 2 24 11 14 13 7 10 36 61 47 hlcgrex 
 |-  ( ph -> E. u e. P ( u ( ( hlG ` G ) ` V ) U /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) )
209 208 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> E. u e. P ( u ( ( hlG ` G ) ` V ) U /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) )
210 207 209 r19.29a 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> <" X Y Z "> .~ <" U V W "> )
211 7 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> G e. TarskiG )
212 8 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> S e. P )
213 9 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> T e. P )
214 10 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> U e. P )
215 11 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> V e. P )
216 12 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> W e. P )
217 13 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> X e. P )
218 14 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> Y e. P )
219 15 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> Z e. P )
220 16 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> Y =/= S )
221 17 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> V =/= T )
222 18 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> X O Z )
223 19 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> U Q W )
224 20 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> <" X Y S "> .~ <" U V T "> )
225 21 adantr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> <" S Y Z "> .~ <" T V W "> )
226 simpr 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> -. Y e. ( X I Z ) )
227 1 2 3 4 5 6 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 tgaaddcpbllem3 
 |-  ( ( ph /\ -. Y e. ( X I Z ) ) -> <" X Y Z "> .~ <" U V W "> )
228 210 227 pm2.61dan 
 |-  ( ph -> <" X Y Z "> .~ <" U V W "> )