Metamath Proof Explorer

Theorem tgaaddcpbllem1

Description: Lemma for tgaaddcpbl . (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 "> )
tgaaddcpbllem3.1 
|- ( ph -> -. Y e. ( X I Z ) )
tgaaddcpbllem1.1 
|- K = ( hlG ` G )
tgaaddcpbllem1.2 
|- ( ph -> R e. ( Y L S ) )
tgaaddcpbllem1.3 
|- ( ph -> R e. ( X I Z ) )
tgaaddcpbllem1.4 
|- ( ph -> R ( K ` Y ) S )
Assertion tgaaddcpbllem1 
|- ( 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 tgaaddcpbllem3.1 
 |-  ( ph -> -. Y e. ( X I Z ) )
23 tgaaddcpbllem1.1 
 |-  K = ( hlG ` G )
24 tgaaddcpbllem1.2 
 |-  ( ph -> R e. ( Y L S ) )
25 tgaaddcpbllem1.3 
 |-  ( ph -> R e. ( X I Z ) )
26 tgaaddcpbllem1.4 
 |-  ( ph -> R ( K ` Y ) S )
27 4 eqcomi 
 |-  ( cgrA ` G ) = .~
28 27 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( cgrA ` G ) = .~ )
29 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> G e. TarskiG )
30 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> G e. TarskiG )
31 13 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> X e. P )
32 14 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> Y e. P )
33 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> Z e. P )
34 33 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> Z e. P )
35 10 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> U e. P )
36 11 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V e. P )
37 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w e. P )
38 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> u e. P )
39 38 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u e. P )
40 1 2 3 7 14 8 16 tglinerflx1 
 |-  ( ph -> Y e. ( Y L S ) )
41 eqid 
 |-  ( dist ` G ) = ( dist ` G )
42 1 2 3 7 14 8 16 tgelrnln 
 |-  ( ph -> ( Y L S ) e. ran L )
43 1 41 2 5 3 42 7 13 15 18 oppne1 
 |-  ( ph -> -. X e. ( Y L S ) )
44 nelne2 
 |-  ( ( Y e. ( Y L S ) /\ -. X e. ( Y L S ) ) -> Y =/= X )
45 40 43 44 syl2anc 
 |-  ( ph -> Y =/= X )
46 45 necomd 
 |-  ( ph -> X =/= Y )
47 46 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> X =/= Y )
48 1 41 2 5 3 42 7 13 15 18 oppne2 
 |-  ( ph -> -. Z e. ( Y L S ) )
49 nelne2 
 |-  ( ( Y e. ( Y L S ) /\ -. Z e. ( Y L S ) ) -> Y =/= Z )
50 40 48 49 syl2anc 
 |-  ( ph -> Y =/= Z )
51 50 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> Y =/= Z )
52 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
53 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) )
54 53 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) X ) = ( V ( dist ` G ) u ) )
55 1 41 2 30 32 31 36 39 54 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( X ( dist ` G ) Y ) = ( u ( dist ` G ) V ) )
56 55 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( u ( dist ` G ) V ) = ( X ( dist ` G ) Y ) )
57 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> r e. P )
58 57 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. P )
59 1 3 2 7 42 24 tglnpt 
 |-  ( ph -> R e. P )
60 59 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> R e. P )
61 60 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> R e. P )
62 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r ( K ` V ) T )
63 30 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> G e. TarskiG )
64 31 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> X e. P )
65 61 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> R e. P )
66 39 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> u e. P )
67 58 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> r e. P )
68 32 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> Y e. P )
69 36 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> V e. P )
70 9 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> T e. P )
71 70 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> T e. P )
72 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> U e. P )
73 8 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> S e. P )
74 73 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> S e. P )
75 4 a1i 
 |-  ( ph -> .~ = ( cgrA ` G ) )
76 75 20 breqdi 
 |-  ( ph -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
77 76 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y S "> ( cgrA ` G ) <" U V T "> )
78 1 2 30 23 31 32 73 35 36 70 77 cgracom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
79 78 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> <" U V T "> ( cgrA ` G ) <" X Y S "> )
80 26 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> R ( K ` Y ) S )
81 1 2 23 63 72 69 71 64 68 74 79 65 80 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> <" U V T "> ( cgrA ` G ) <" X Y R "> )
82 1 2 63 23 72 69 71 64 68 65 81 cgracom 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> <" X Y R "> ( cgrA ` G ) <" U V T "> )
83 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> u ( K ` V ) U )
84 1 2 23 63 64 68 65 72 69 71 82 66 83 cgrahl1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> <" X Y R "> ( cgrA ` G ) <" u V T "> )
85 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> r ( K ` V ) T )
86 1 2 23 63 64 68 65 66 69 71 84 67 85 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> <" X Y R "> ( cgrA ` G ) <" u V r "> )
87 1 2 23 13 13 14 7 46 hlid 
 |-  ( ph -> X ( K ` Y ) X )
88 87 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> X ( K ` Y ) X )
89 88 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> X ( K ` Y ) X )
90 simpr 
 |-  ( ( ph /\ R = Y ) -> R = Y )
91 25 adantr 
 |-  ( ( ph /\ R = Y ) -> R e. ( X I Z ) )
92 90 91 eqeltrrd 
 |-  ( ( ph /\ R = Y ) -> Y e. ( X I Z ) )
93 22 92 mtand 
 |-  ( ph -> -. R = Y )
94 93 neqned 
 |-  ( ph -> R =/= Y )
95 94 necomd 
 |-  ( ph -> Y =/= R )
96 95 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> Y =/= R )
97 96 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> R =/= Y )
98 1 2 23 65 64 68 63 97 hlid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> R ( K ` Y ) R )
99 54 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> ( Y ( dist ` G ) X ) = ( V ( dist ` G ) u ) )
100 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) )
101 100 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) R ) = ( V ( dist ` G ) r ) )
102 101 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> ( Y ( dist ` G ) R ) = ( V ( dist ` G ) r ) )
103 1 2 23 63 64 68 65 66 69 67 86 64 41 65 89 98 99 102 cgracgr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> ( X ( dist ` G ) R ) = ( u ( dist ` G ) r ) )
104 1 41 2 63 64 65 66 67 103 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> ( R ( dist ` G ) X ) = ( r ( dist ` G ) u ) )
105 62 104 mpdan 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( R ( dist ` G ) X ) = ( r ( dist ` G ) u ) )
106 24 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ r ( K ` V ) T ) -> R e. ( Y L S ) )
107 62 106 mpdan 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> R e. ( Y L S ) )
108 43 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. X e. ( Y L S ) )
109 nelne2 
 |-  ( ( R e. ( Y L S ) /\ -. X e. ( Y L S ) ) -> R =/= X )
110 107 108 109 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> R =/= X )
111 1 41 2 30 61 31 58 39 105 110 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r =/= u )
112 111 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u =/= r )
113 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. ( u I w ) )
114 25 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> R e. ( X I Z ) )
115 105 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( r ( dist ` G ) u ) = ( R ( dist ` G ) X ) )
116 1 41 2 30 58 39 61 31 115 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( u ( dist ` G ) r ) = ( X ( dist ` G ) R ) )
117 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) )
118 1 41 2 30 36 58 32 61 100 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( r ( dist ` G ) V ) = ( R ( dist ` G ) Y ) )
119 1 41 2 30 39 58 37 31 61 34 36 32 112 113 114 116 117 56 118 axtg5seg 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( w ( dist ` G ) V ) = ( Z ( dist ` G ) Y ) )
120 1 41 2 30 37 36 34 32 119 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( V ( dist ` G ) w ) = ( Y ( dist ` G ) Z ) )
121 1 41 2 30 39 58 37 31 61 34 113 114 116 117 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( u ( dist ` G ) w ) = ( X ( dist ` G ) Z ) )
122 1 41 2 30 39 37 31 34 121 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( w ( dist ` G ) u ) = ( Z ( dist ` G ) X ) )
123 1 41 52 30 39 36 37 31 32 34 56 120 122 trgcgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" u V w "> ( cgrG ` G ) <" X Y Z "> )
124 1 41 2 52 30 39 36 37 31 32 34 123 trgcgrcom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrG ` G ) <" u V w "> )
125 1 2 30 23 31 32 34 39 36 37 47 51 124 cgrcgra 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" u V w "> )
126 62 83 mpdan 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u ( K ` V ) U )
127 1 2 23 39 35 36 30 126 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> U ( K ` V ) u )
128 1 2 23 30 31 32 34 39 36 37 125 35 127 cgrahl1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V w "> )
129 12 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> W e. P )
130 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
131 eqid 
 |-  ( ( pInvG ` G ) ` T ) = ( ( pInvG ` G ) ` T )
132 1 41 2 3 130 7 9 131 10 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
133 132 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
134 7 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> G e. TarskiG )
135 14 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y e. P )
136 8 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. P )
137 15 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z e. P )
138 16 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y =/= S )
139 simpr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. ( Y L Z ) )
140 50 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Y =/= Z )
141 1 2 3 134 135 137 140 tglinecom 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> ( Y L Z ) = ( Z L Y ) )
142 139 141 eleqtrd 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> S e. ( Z L Y ) )
143 50 necomd 
 |-  ( ph -> Z =/= Y )
144 143 adantr 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z =/= Y )
145 1 2 3 134 135 136 137 138 142 144 lnrot1 
 |-  ( ( ph /\ S e. ( Y L Z ) ) -> Z e. ( Y L S ) )
146 48 145 mtand 
 |-  ( ph -> -. S e. ( Y L Z ) )
147 50 neneqd 
 |-  ( ph -> -. Y = Z )
148 146 147 jca 
 |-  ( ph -> ( -. S e. ( Y L Z ) /\ -. Y = Z ) )
149 ioran 
 |-  ( -. ( S e. ( Y L Z ) \/ Y = Z ) <-> ( -. S e. ( Y L Z ) /\ -. Y = Z ) )
150 148 149 sylibr 
 |-  ( ph -> -. ( S e. ( Y L Z ) \/ Y = Z ) )
151 150 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. ( S e. ( Y L Z ) \/ Y = Z ) )
152 1 41 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 ) ) ) )
153 19 152 mpbid 
 |-  ( ph -> ( ( -. U e. ( V L T ) /\ -. W e. ( V L T ) ) /\ E. t e. ( V L T ) t e. ( U I W ) ) )
154 153 simplld 
 |-  ( ph -> -. U e. ( V L T ) )
155 7 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> G e. TarskiG )
156 9 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> T e. P )
157 10 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> U e. P )
158 1 41 2 3 130 155 156 131 157 mirmir 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` ( ( ( pInvG ` G ) ` T ) ` U ) ) = U )
159 1 2 3 7 11 9 17 tgelrnln 
 |-  ( ph -> ( V L T ) e. ran L )
160 159 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( V L T ) e. ran L )
161 1 2 3 7 11 9 17 tglinerflx2 
 |-  ( ph -> T e. ( V L T ) )
162 161 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> T e. ( V L T ) )
163 132 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. P )
164 11 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> V e. P )
165 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 ) ) )
166 1 3 2 155 164 163 156 165 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 ) )
167 1 3 2 155 163 164 156 166 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 ) )
168 17 neneqd 
 |-  ( ph -> -. V = T )
169 168 adantr 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> -. V = T )
170 167 169 olcnd 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) e. ( V L T ) )
171 1 41 2 3 130 155 131 160 162 170 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 ) )
172 158 171 eqeltrrd 
 |-  ( ( ph /\ ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) ) -> U e. ( V L T ) )
173 154 172 mtand 
 |-  ( ph -> -. ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) )
174 173 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. ( T e. ( V L ( ( ( pInvG ` G ) ` T ) ` U ) ) \/ V = ( ( ( pInvG ` G ) ` T ) ` U ) ) )
175 75 21 breqdi 
 |-  ( ph -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
176 175 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V W "> )
177 62 97 mpdan 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> R =/= Y )
178 177 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> Y =/= R )
179 1 41 2 30 32 61 36 58 101 178 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V =/= r )
180 179 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r =/= V )
181 120 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) Z ) = ( V ( dist ` G ) w ) )
182 1 41 2 30 32 34 36 37 181 51 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V =/= w )
183 1 41 2 30 58 37 61 34 117 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( w ( dist ` G ) r ) = ( Z ( dist ` G ) R ) )
184 1 41 52 30 58 36 37 61 32 34 118 120 183 trgcgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" r V w "> ( cgrG ` G ) <" R Y Z "> )
185 1 2 30 23 58 36 37 61 32 34 180 182 184 cgrcgra 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" r V w "> ( cgrA ` G ) <" R Y Z "> )
186 1 2 23 59 8 14 7 26 hlcomd 
 |-  ( ph -> S ( K ` Y ) R )
187 186 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> S ( K ` Y ) R )
188 1 2 23 30 58 36 37 61 32 34 185 73 187 cgrahl1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" r V w "> ( cgrA ` G ) <" S Y Z "> )
189 1 2 30 23 58 36 37 73 32 34 188 cgracom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" S Y Z "> ( cgrA ` G ) <" r V w "> )
190 1 2 23 58 70 36 30 62 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> T ( K ` V ) r )
191 1 2 23 30 73 32 34 58 36 37 189 70 190 cgrahl1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" S Y Z "> ( cgrA ` G ) <" T V w "> )
192 1 2 3 7 11 9 17 tglinecom 
 |-  ( ph -> ( V L T ) = ( T L V ) )
193 192 fveq2d 
 |-  ( ph -> ( ( hpG ` G ) ` ( V L T ) ) = ( ( hpG ` G ) ` ( T L V ) ) )
194 10 154 eldifd 
 |-  ( ph -> U e. ( P \ ( V L T ) ) )
195 1 2 130 131 6 7 159 161 194 3 oppmir 
 |-  ( ph -> U Q ( ( ( pInvG ` G ) ` T ) ` U ) )
196 1 41 2 6 3 159 7 10 132 195 oppcom 
 |-  ( ph -> ( ( ( pInvG ` G ) ` T ) ` U ) Q U )
197 1 41 2 6 3 159 7 10 12 19 oppcom 
 |-  ( ph -> W Q U )
198 1 2 3 6 7 159 12 132 10 197 lnopp2hpgb 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` T ) ` U ) Q U <-> W ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) ) )
199 196 198 mpbid 
 |-  ( ph -> W ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
200 193 199 breqdi 
 |-  ( ph -> W ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
201 200 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> W ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
202 193 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( ( hpG ` G ) ` ( V L T ) ) = ( ( hpG ` G ) ` ( T L V ) ) )
203 196 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( ( ( pInvG ` G ) ` T ) ` U ) Q U )
204 159 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( V L T ) e. ran L )
205 1 2 23 58 70 36 30 3 62 hlln 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. ( T L V ) )
206 192 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( V L T ) = ( T L V ) )
207 205 206 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. ( V L T ) )
208 nelne2 
 |-  ( ( R e. ( Y L S ) /\ -. Z e. ( Y L S ) ) -> R =/= Z )
209 24 48 208 syl2anc 
 |-  ( ph -> R =/= Z )
210 209 neneqd 
 |-  ( ph -> -. R = Z )
211 210 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. R = Z )
212 30 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> G e. TarskiG )
213 58 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> r e. P )
214 37 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. P )
215 61 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> R e. P )
216 34 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> Z e. P )
217 117 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) )
218 121 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( X ( dist ` G ) Z ) = ( u ( dist ` G ) w ) )
219 1 41 2 5 3 42 7 13 15 18 oppne3 
 |-  ( ph -> X =/= Z )
220 219 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> X =/= Z )
221 1 41 2 30 31 34 39 37 218 220 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u =/= w )
222 1 2 3 30 39 37 221 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( u L w ) e. ran L )
223 222 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( u L w ) e. ran L )
224 204 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( V L T ) e. ran L )
225 1 2 3 30 39 37 221 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u e. ( u L w ) )
226 30 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> G e. TarskiG )
227 36 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> V e. P )
228 70 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> T e. P )
229 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> U e. P )
230 17 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> V =/= T )
231 39 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> u e. P )
232 45 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> Y =/= X )
233 1 41 2 30 32 31 36 39 54 232 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V =/= u )
234 233 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u =/= V )
235 234 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> u =/= V )
236 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> u e. ( V L T ) )
237 1 2 3 226 231 227 228 235 236 230 lnrot2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> T e. ( u L V ) )
238 1 2 3 7 11 9 17 tglinerflx1 
 |-  ( ph -> V e. ( V L T ) )
239 nelne2 
 |-  ( ( V e. ( V L T ) /\ -. U e. ( V L T ) ) -> V =/= U )
240 238 154 239 syl2anc 
 |-  ( ph -> V =/= U )
241 240 necomd 
 |-  ( ph -> U =/= V )
242 241 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> U =/= V )
243 1 2 3 226 231 227 235 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> ( u L V ) e. ran L )
244 1 2 23 39 35 36 30 3 126 hlln 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u e. ( U L V ) )
245 241 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> U =/= V )
246 1 2 3 30 35 36 245 tglinecom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( U L V ) = ( V L U ) )
247 244 246 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u e. ( V L U ) )
248 240 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V =/= U )
249 1 2 3 30 39 36 35 234 247 248 lnrot2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> U e. ( u L V ) )
250 249 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> U e. ( u L V ) )
251 1 2 3 226 231 227 235 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> V e. ( u L V ) )
252 1 2 3 226 229 227 242 242 243 250 251 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> ( u L V ) = ( U L V ) )
253 237 252 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> T e. ( U L V ) )
254 1 2 3 226 227 228 229 230 253 242 lnrot1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> U e. ( V L T ) )
255 154 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ u e. ( V L T ) ) -> -. U e. ( V L T ) )
256 254 255 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. u e. ( V L T ) )
257 nelne1 
 |-  ( ( u e. ( u L w ) /\ -. u e. ( V L T ) ) -> ( u L w ) =/= ( V L T ) )
258 225 256 257 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( u L w ) =/= ( V L T ) )
259 258 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> ( u L w ) =/= ( V L T ) )
260 1 2 3 30 39 37 58 221 113 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. ( u L w ) )
261 260 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> r e. ( u L w ) )
262 207 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> r e. ( V L T ) )
263 261 262 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> r e. ( ( u L w ) i^i ( V L T ) ) )
264 1 2 3 30 39 37 221 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w e. ( u L w ) )
265 264 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( u L w ) )
266 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( V L T ) )
267 265 266 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> w e. ( ( u L w ) i^i ( V L T ) ) )
268 1 2 3 212 223 224 259 263 267 tglineineq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> r = w )
269 1 41 2 212 213 214 215 216 217 268 tgcgreq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) /\ w e. ( V L T ) ) -> R = Z )
270 211 269 mtand 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> -. w e. ( V L T ) )
271 1 41 2 30 39 58 37 113 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> r e. ( w I u ) )
272 1 41 2 6 37 39 207 270 256 271 islnoppd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w Q u )
273 1 41 2 6 3 204 30 37 39 272 oppcom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> u Q w )
274 238 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> V e. ( V L T ) )
275 1 41 2 6 3 204 30 23 39 35 37 273 274 126 opphl 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> U Q w )
276 1 41 2 6 3 204 30 35 37 275 oppcom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w Q U )
277 1 2 3 6 30 204 37 133 35 276 lnopp2hpgb 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> ( ( ( ( pInvG ` G ) ` T ) ` U ) Q U <-> w ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) ) )
278 203 277 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w ( ( hpG ` G ) ` ( V L T ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
279 202 278 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> w ( ( hpG ` G ) ` ( T L V ) ) ( ( ( pInvG ` G ) ` T ) ` U ) )
280 1 2 41 30 73 32 34 70 36 133 3 151 174 129 37 23 176 191 201 279 acopyeu 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> W ( K ` V ) w )
281 1 2 23 30 31 32 34 35 36 37 128 129 280 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" U V W "> )
282 28 281 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ r e. ( u I w ) ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) -> <" X Y Z "> .~ <" U V W "> )
283 282 anasss 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) /\ w e. P ) /\ ( r e. ( u I w ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) ) -> <" X Y Z "> .~ <" U V W "> )
284 1 41 2 29 38 57 60 33 axtgsegcon 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> E. w e. P ( r e. ( u I w ) /\ ( r ( dist ` G ) w ) = ( R ( dist ` G ) Z ) ) )
285 283 284 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ r ( K ` V ) T ) /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) -> <" X Y Z "> .~ <" U V W "> )
286 285 anasss 
 |-  ( ( ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) /\ r e. P ) /\ ( r ( K ` V ) T /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) ) -> <" X Y Z "> .~ <" U V W "> )
287 17 necomd 
 |-  ( ph -> T =/= V )
288 1 2 23 11 14 59 7 9 41 287 95 hlcgrex 
 |-  ( ph -> E. r e. P ( r ( K ` V ) T /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) )
289 288 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> E. r e. P ( r ( K ` V ) T /\ ( V ( dist ` G ) r ) = ( Y ( dist ` G ) R ) ) )
290 286 289 r19.29a 
 |-  ( ( ( ( ph /\ u e. P ) /\ u ( K ` V ) U ) /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) -> <" X Y Z "> .~ <" U V W "> )
291 290 anasss 
 |-  ( ( ( ph /\ u e. P ) /\ ( u ( K ` V ) U /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) ) -> <" X Y Z "> .~ <" U V W "> )
292 1 2 23 11 14 13 7 10 41 241 45 hlcgrex 
 |-  ( ph -> E. u e. P ( u ( K ` V ) U /\ ( V ( dist ` G ) u ) = ( Y ( dist ` G ) X ) ) )
293 291 292 r19.29a 
 |-  ( ph -> <" X Y Z "> .~ <" U V W "> )