Metamath Proof Explorer

Theorem angmndaddeu1

Description: There exists a unique point s satisfying the conditions of angle addition. General case. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmndadd.p 
|- P = ( Base ` G )
angmndadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmndadd.i 
|- I = ( Itv ` G )
angmndadd.d 
|- .- = ( dist ` G )
angmndadd.c 
|- .~ = ( cgrA ` G )
angmndadd.l 
|- L = ( LineG ` G )
angmndadd.g 
|- ( ph -> G e. TarskiG )
angmndaddov.u 
|- ( ph -> U e. P )
angmndaddov.v 
|- ( ph -> V e. P )
angmndaddov.w 
|- ( ph -> W e. P )
angmndaddov.x 
|- ( ph -> X e. P )
angmndaddov.y 
|- ( ph -> Y e. P )
angmndaddov.z 
|- ( ph -> Z e. P )
angmndaddeu.1 
|- ( ph -> U =/= V )
angmndaddeu.2 
|- ( ph -> V =/= W )
angmndaddeu.3 
|- ( ph -> X =/= Y )
angmndaddeu.4 
|- ( ph -> Y =/= Z )
angmndaddeu1.1 
|- ( ph -> -. X e. ( Y L Z ) )
angmndaddeu1.2 
|- ( ph -> -. U e. ( V L W ) )
Assertion angmndaddeu1 
|- ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 angmndadd.p 
 |-  P = ( Base ` G )
2 angmndadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmndadd.i 
 |-  I = ( Itv ` G )
4 angmndadd.d 
 |-  .- = ( dist ` G )
5 angmndadd.c 
 |-  .~ = ( cgrA ` G )
6 angmndadd.l 
 |-  L = ( LineG ` G )
7 angmndadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmndaddov.u 
 |-  ( ph -> U e. P )
9 angmndaddov.v 
 |-  ( ph -> V e. P )
10 angmndaddov.w 
 |-  ( ph -> W e. P )
11 angmndaddov.x 
 |-  ( ph -> X e. P )
12 angmndaddov.y 
 |-  ( ph -> Y e. P )
13 angmndaddov.z 
 |-  ( ph -> Z e. P )
14 angmndaddeu.1 
 |-  ( ph -> U =/= V )
15 angmndaddeu.2 
 |-  ( ph -> V =/= W )
16 angmndaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmndaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmndaddeu1.1 
 |-  ( ph -> -. X e. ( Y L Z ) )
19 angmndaddeu1.2 
 |-  ( ph -> -. U e. ( V L W ) )
20 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
21 7 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> G e. TarskiG )
22 simpllr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> w e. P )
23 9 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> V e. P )
24 8 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> U e. P )
25 13 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> Z e. P )
26 12 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> Y e. P )
27 15 neneqd 
 |-  ( ph -> -. V = W )
28 ioran 
 |-  ( -. ( U e. ( V L W ) \/ V = W ) <-> ( -. U e. ( V L W ) /\ -. V = W ) )
29 19 27 28 sylanbrc 
 |-  ( ph -> -. ( U e. ( V L W ) \/ V = W ) )
30 1 6 3 7 9 10 8 29 ncolrot2 
 |-  ( ph -> -. ( W e. ( U L V ) \/ U = V ) )
31 1 6 3 7 8 9 10 30 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
32 eqid 
 |-  ( ( lInvG ` G ) ` ( Y L Z ) ) = ( ( lInvG ` G ) ` ( Y L Z ) )
33 1 3 6 7 12 13 17 tgelrnln 
 |-  ( ph -> ( Y L Z ) e. ran L )
34 1 4 3 7 31 32 6 33 11 lmicl 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. P )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. P )
36 30 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> -. ( W e. ( U L V ) \/ U = V ) )
37 21 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> G e. TarskiG )
38 23 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> V e. P )
39 24 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> U e. P )
40 14 neneqd 
 |-  ( ph -> -. U = V )
41 40 neqcomd 
 |-  ( ph -> -. V = U )
42 41 neqned 
 |-  ( ph -> V =/= U )
43 42 ad4antr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> V =/= U )
44 22 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> w e. P )
45 simpr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> ( V .- w ) = ( Y .- Z ) )
46 45 eqcomd 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> ( Y .- Z ) = ( V .- w ) )
47 17 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> Y =/= Z )
48 1 4 3 21 26 25 23 22 46 47 tgcgrneq 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> V =/= w )
49 48 necomd 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> w =/= V )
50 49 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> w =/= V )
51 simpr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> ( w e. ( V L U ) \/ V = U ) )
52 41 ad4antr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> -. V = U )
53 51 52 olcnd 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> w e. ( V L U ) )
54 10 ad4antr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> W e. P )
55 10 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> W e. P )
56 simplr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> w ( ( hlG ` G ) ` V ) W )
57 1 3 20 22 55 23 21 56 hlcomd 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> W ( ( hlG ` G ) ` V ) w )
58 1 3 20 55 22 23 21 6 57 hlln 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> W e. ( w L V ) )
59 1 3 6 21 23 22 55 48 58 lncom 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> W e. ( V L w ) )
60 59 adantr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> W e. ( V L w ) )
61 1 3 6 37 38 39 43 44 50 53 54 60 tglineeltr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> W e. ( V L U ) )
62 1 3 6 7 9 8 42 tglinecom 
 |-  ( ph -> ( V L U ) = ( U L V ) )
63 62 ad4antr 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> ( V L U ) = ( U L V ) )
64 61 63 eleqtrd 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> W e. ( U L V ) )
65 64 orcd 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ ( w e. ( V L U ) \/ V = U ) ) -> ( W e. ( U L V ) \/ U = V ) )
66 36 65 mtand 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> -. ( w e. ( V L U ) \/ V = U ) )
67 eleq1 
 |-  ( a = c -> ( a e. ( P \ ( Y L Z ) ) <-> c e. ( P \ ( Y L Z ) ) ) )
68 67 adantr 
 |-  ( ( a = c /\ b = d ) -> ( a e. ( P \ ( Y L Z ) ) <-> c e. ( P \ ( Y L Z ) ) ) )
69 eleq1 
 |-  ( b = d -> ( b e. ( P \ ( Y L Z ) ) <-> d e. ( P \ ( Y L Z ) ) ) )
70 69 adantl 
 |-  ( ( a = c /\ b = d ) -> ( b e. ( P \ ( Y L Z ) ) <-> d e. ( P \ ( Y L Z ) ) ) )
71 68 70 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) <-> ( c e. ( P \ ( Y L Z ) ) /\ d e. ( P \ ( Y L Z ) ) ) ) )
72 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
73 72 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a I b ) <-> s e. ( c I d ) ) )
74 73 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L Z ) s e. ( a I b ) <-> E. s e. ( Y L Z ) s e. ( c I d ) ) )
75 eleq1 
 |-  ( s = t -> ( s e. ( c I d ) <-> t e. ( c I d ) ) )
76 75 cbvrexvw 
 |-  ( E. s e. ( Y L Z ) s e. ( c I d ) <-> E. t e. ( Y L Z ) t e. ( c I d ) )
77 74 76 bitrdi 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L Z ) s e. ( a I b ) <-> E. t e. ( Y L Z ) t e. ( c I d ) ) )
78 71 77 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) <-> ( ( c e. ( P \ ( Y L Z ) ) /\ d e. ( P \ ( Y L Z ) ) ) /\ E. t e. ( Y L Z ) t e. ( c I d ) ) ) )
79 78 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( Y L Z ) ) /\ d e. ( P \ ( Y L Z ) ) ) /\ E. t e. ( Y L Z ) t e. ( c I d ) ) }
80 1 4 3 6 7 31 33 79 32 11 18 lmiopp 
 |-  ( ph -> X { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
81 1 4 3 79 6 33 7 11 34 80 oppne2 
 |-  ( ph -> -. ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. ( Y L Z ) )
82 1 3 6 7 12 13 17 tglinecom 
 |-  ( ph -> ( Y L Z ) = ( Z L Y ) )
83 81 82 neleqtrd 
 |-  ( ph -> -. ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. ( Z L Y ) )
84 17 necomd 
 |-  ( ph -> Z =/= Y )
85 84 neneqd 
 |-  ( ph -> -. Z = Y )
86 ioran 
 |-  ( -. ( ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. ( Z L Y ) \/ Z = Y ) <-> ( -. ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. ( Z L Y ) /\ -. Z = Y ) )
87 83 85 86 sylanbrc 
 |-  ( ph -> -. ( ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. ( Z L Y ) \/ Z = Y ) )
88 1 6 3 7 13 12 34 87 ncolrot1 
 |-  ( ph -> -. ( Z e. ( Y L ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) \/ Y = ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) )
89 88 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> -. ( Z e. ( Y L ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) \/ Y = ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) )
90 1 4 3 21 23 22 26 25 45 tgcgrcomlr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> ( w .- V ) = ( Z .- Y ) )
91 1 4 3 6 20 21 22 23 24 25 26 35 66 89 90 trgcopyeu 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> E! s e. P ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) )
92 5 eqcomi 
 |-  ( cgrA ` G ) = .~
93 92 a1i 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( cgrA ` G ) = .~ )
94 21 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> G e. TarskiG )
95 25 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> Z e. P )
96 26 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> Y e. P )
97 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> s e. P )
98 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> U e. P )
99 23 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> V e. P )
100 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> w e. P )
101 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> U =/= V )
102 48 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> V =/= w )
103 1 3 94 20 98 99 100 101 102 cgraswap 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" U V w "> ( cgrA ` G ) <" w V U "> )
104 49 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> w =/= V )
105 42 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> V =/= U )
106 simplr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" w V U "> ( cgrG ` G ) <" Z Y s "> )
107 1 3 94 20 100 99 98 95 96 97 104 105 106 cgrcgra 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" w V U "> ( cgrA ` G ) <" Z Y s "> )
108 1 3 94 20 98 99 100 100 99 98 103 95 96 97 107 cgratr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" U V w "> ( cgrA ` G ) <" Z Y s "> )
109 1 3 94 20 98 99 100 95 96 97 108 cgracom 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V w "> )
110 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> W e. P )
111 57 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> W ( ( hlG ` G ) ` V ) w )
112 1 3 20 94 95 96 97 98 99 100 109 110 111 cgrahl2 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
113 93 112 breqdi 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> <" Z Y s "> .~ <" U V W "> )
114 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
115 1 4 3 114 94 100 99 98 95 96 97 106 cgr3simp2 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( V .- U ) = ( Y .- s ) )
116 115 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( Y .- s ) = ( V .- U ) )
117 33 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( Y L Z ) e. ran L )
118 11 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> X e. P )
119 118 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> X e. P )
120 35 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. P )
121 eqidd 
 |-  ( ph -> ( hpG ` G ) = ( hpG ` G ) )
122 121 82 fveq12d 
 |-  ( ph -> ( ( hpG ` G ) ` ( Y L Z ) ) = ( ( hpG ` G ) ` ( Z L Y ) ) )
123 122 eqcomd 
 |-  ( ph -> ( ( hpG ` G ) ` ( Z L Y ) ) = ( ( hpG ` G ) ` ( Y L Z ) ) )
124 123 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( ( hpG ` G ) ` ( Z L Y ) ) = ( ( hpG ` G ) ` ( Y L Z ) ) )
125 simpr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
126 124 125 breqdi 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> s ( ( hpG ` G ) ` ( Y L Z ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
127 1 3 6 94 117 97 79 120 126 hpgcom 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ( ( hpG ` G ) ` ( Y L Z ) ) s )
128 21 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> G e. TarskiG )
129 33 ad5antr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> ( Y L Z ) e. ran L )
130 35 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. P )
131 simplr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> s e. P )
132 118 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> X e. P )
133 80 ad5antr 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> X { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
134 1 4 3 79 6 129 128 132 130 133 oppcom 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X )
135 1 3 6 79 128 129 130 131 132 134 lnopp2hpgb 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) -> ( s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X <-> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ( ( hpG ` G ) ` ( Y L Z ) ) s ) )
136 135 adantr 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X <-> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ( ( hpG ` G ) ` ( Y L Z ) ) s ) )
137 127 136 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X )
138 1 3 6 79 94 117 97 119 137 lnoppinn0 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( ( Y L Z ) i^i ( s I X ) ) =/= (/) )
139 113 116 138 3jca 
 |-  ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" w V U "> ( cgrG ` G ) <" Z Y s "> ) /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
140 139 anasss 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
141 21 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> G e. TarskiG )
142 22 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> w e. P )
143 23 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> V e. P )
144 24 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U e. P )
145 25 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Z e. P )
146 26 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y e. P )
147 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s e. P )
148 90 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( w .- V ) = ( Z .- Y ) )
149 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( Y .- s ) = ( V .- U ) )
150 149 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( V .- U ) = ( Y .- s ) )
151 55 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> W e. P )
152 42 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> V =/= U )
153 1 4 3 141 143 144 146 147 150 152 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y =/= s )
154 153 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s =/= Y )
155 47 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y =/= Z )
156 1 3 141 20 147 146 145 154 155 cgraswap 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" s Y Z "> ( cgrA ` G ) <" Z Y s "> )
157 5 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> .~ = ( cgrA ` G ) )
158 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> .~ <" U V W "> )
159 157 158 breqdi 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
160 1 3 141 20 147 146 145 145 146 147 156 144 143 151 159 cgratr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" s Y Z "> ( cgrA ` G ) <" U V W "> )
161 1 3 141 20 147 146 145 144 143 151 160 cgracom 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" U V W "> ( cgrA ` G ) <" s Y Z "> )
162 118 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> X e. P )
163 14 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U =/= V )
164 1 3 20 144 162 143 141 163 hlid 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U ( ( hlG ` G ) ` V ) U )
165 56 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> w ( ( hlG ` G ) ` V ) W )
166 45 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( V .- w ) = ( Y .- Z ) )
167 1 3 20 141 144 143 151 147 146 145 161 144 4 142 164 165 150 166 cgracgr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( U .- w ) = ( s .- Z ) )
168 1 4 114 141 142 143 144 145 146 147 148 150 167 trgcgr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" w V U "> ( cgrG ` G ) <" Z Y s "> )
169 122 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( ( hpG ` G ) ` ( Y L Z ) ) = ( ( hpG ` G ) ` ( Z L Y ) ) )
170 33 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( Y L Z ) e. ran L )
171 35 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) e. P )
172 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( ( Y L Z ) i^i ( s I X ) ) =/= (/) )
173 147 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> s e. P )
174 162 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> X e. P )
175 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> r e. ( ( Y L Z ) i^i ( s I X ) ) )
176 175 elin1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> r e. ( Y L Z ) )
177 36 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> -. ( W e. ( U L V ) \/ U = V ) )
178 1 3 4 141 144 143 151 147 146 145 161 6 177 cgrancol 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> -. ( Z e. ( s L Y ) \/ s = Y ) )
179 1 6 3 141 147 146 145 178 ncolrot1 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> -. ( s e. ( Y L Z ) \/ Y = Z ) )
180 179 orsild 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> -. s e. ( Y L Z ) )
181 180 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> -. s e. ( Y L Z ) )
182 18 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> -. X e. ( Y L Z ) )
183 175 elin2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> r e. ( s I X ) )
184 1 4 3 79 173 174 176 181 182 183 islnoppd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) /\ r e. ( ( Y L Z ) i^i ( s I X ) ) ) -> s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X )
185 172 184 n0limd 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X )
186 80 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> X { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
187 1 4 3 79 6 170 141 162 171 186 oppcom 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X )
188 1 3 6 79 141 170 171 147 162 187 lnopp2hpgb 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( s { <. a , b >. | ( ( a e. ( P \ ( Y L Z ) ) /\ b e. ( P \ ( Y L Z ) ) ) /\ E. s e. ( Y L Z ) s e. ( a I b ) ) } X <-> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ( ( hpG ` G ) ` ( Y L Z ) ) s ) )
189 185 188 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ( ( hpG ` G ) ` ( Y L Z ) ) s )
190 1 3 6 141 170 171 79 147 189 hpgcom 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s ( ( hpG ` G ) ` ( Y L Z ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
191 169 190 breqdi 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) )
192 168 191 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) )
193 192 3anasss 
 |-  ( ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) -> ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) )
194 140 193 impbida 
 |-  ( ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) /\ s e. P ) -> ( ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
195 194 reubidva 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> ( E! s e. P ( <" w V U "> ( cgrG ` G ) <" Z Y s "> /\ s ( ( hpG ` G ) ` ( Z L Y ) ) ( ( ( lInvG ` G ) ` ( Y L Z ) ) ` X ) ) <-> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
196 91 195 mpbid 
 |-  ( ( ( ( ph /\ w e. P ) /\ w ( ( hlG ` G ) ` V ) W ) /\ ( V .- w ) = ( Y .- Z ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
197 196 anasss 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( ( hlG ` G ) ` V ) W /\ ( V .- w ) = ( Y .- Z ) ) ) -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
198 15 necomd 
 |-  ( ph -> W =/= V )
199 1 3 20 9 12 13 7 10 4 198 17 hlcgrex 
 |-  ( ph -> E. w e. P ( w ( ( hlG ` G ) ` V ) W /\ ( V .- w ) = ( Y .- Z ) ) )
200 197 199 r19.29a 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )