Metamath Proof Explorer

Theorem angmndaddov2lem

Description: Lemma for angmndaddov2 . (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 )
angmndaddov2lem.1 
|- ( ph -> X e. ( Y L Z ) )
Assertion angmndaddov2lem 
|- ( ph -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- 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 angmndaddov2lem.1 
 |-  ( ph -> X e. ( Y L Z ) )
19 7 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> G e. TarskiG )
20 11 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> X e. P )
21 12 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y e. P )
22 13 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> Z e. P )
23 8 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> U e. P )
24 9 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> V e. P )
25 10 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> W e. P )
26 16 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> X =/= Y )
27 17 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y =/= Z )
28 14 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> U =/= V )
29 15 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> V =/= W )
30 simpr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> U ( ( hlG ` G ) ` V ) W )
31 simplr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> X ( ( hlG ` G ) ` Y ) Z )
32 1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31 angmndaddeu4 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
33 32 adantlr 
 |-  ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
34 7 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> G e. TarskiG )
35 11 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> X e. P )
36 12 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> Y e. P )
37 13 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> Z e. P )
38 8 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> U e. P )
39 9 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> V e. P )
40 10 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> W e. P )
41 16 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> X =/= Y )
42 17 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> Y =/= Z )
43 14 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> U =/= V )
44 15 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> V =/= W )
45 simpr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> V e. ( W I U ) )
46 1 4 3 34 40 39 38 45 tgbtwncom 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> V e. ( U I W ) )
47 simplr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> X ( ( hlG ` G ) ` Y ) Z )
48 1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 46 47 angmndaddeu6 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ V e. ( W I U ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
49 48 adantlr 
 |-  ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) /\ V e. ( W I U ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
50 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
51 10 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> W e. P )
52 9 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> V e. P )
53 8 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> U e. P )
54 7 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> G e. TarskiG )
55 11 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> X e. P )
56 15 necomd 
 |-  ( ph -> W =/= V )
57 56 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> W =/= V )
58 simpr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> U e. ( V L W ) )
59 1 3 6 54 51 52 53 57 58 lncom 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> U e. ( W L V ) )
60 1 3 50 51 52 53 54 55 6 59 lnhl 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> ( U ( ( hlG ` G ) ` V ) W \/ V e. ( W I U ) ) )
61 33 49 60 mpjaodan 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
62 7 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> G e. TarskiG )
63 11 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> X e. P )
64 12 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> Y e. P )
65 13 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> Z e. P )
66 8 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> U e. P )
67 9 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> V e. P )
68 10 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> W e. P )
69 16 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> X =/= Y )
70 17 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> Y =/= Z )
71 14 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> U =/= V )
72 15 ad2antrr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> V =/= W )
73 simpr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> -. U e. ( V L W ) )
74 simplr 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> X ( ( hlG ` G ) ` Y ) Z )
75 1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74 angmndaddeu2 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
76 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> <" W V s "> .~ <" X Y Z "> )
77 simplr 
 |-  ( ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> ( V .- s ) = ( Y .- X ) )
78 76 77 jca 
 |-  ( ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
79 78 3anasss 
 |-  ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
80 simplr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" W V s "> .~ <" X Y Z "> )
81 simpr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( V .- s ) = ( Y .- X ) )
82 62 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> G e. TarskiG )
83 67 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V e. P )
84 68 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> W e. P )
85 simpllr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. P )
86 72 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V =/= W )
87 63 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> X e. P )
88 64 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Y e. P )
89 65 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Z e. P )
90 5 a1i 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> .~ = ( cgrA ` G ) )
91 90 80 breqdi 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" W V s "> ( cgrA ` G ) <" X Y Z "> )
92 1 3 82 50 84 83 85 87 88 89 91 cgracom 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" X Y Z "> ( cgrA ` G ) <" W V s "> )
93 74 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> X ( ( hlG ` G ) ` Y ) Z )
94 1 3 4 82 87 88 89 84 83 85 92 50 93 cgrahl 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> W ( ( hlG ` G ) ` V ) s )
95 1 3 50 84 85 83 82 6 94 hlln 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> W e. ( s L V ) )
96 81 eqcomd 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( Y .- X ) = ( V .- s ) )
97 16 necomd 
 |-  ( ph -> Y =/= X )
98 97 ad5antr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Y =/= X )
99 1 4 3 82 88 87 83 85 96 98 tgcgrneq 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V =/= s )
100 99 necomd 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s =/= V )
101 1 3 6 82 83 84 85 86 95 100 lnrot1 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( V L W ) )
102 66 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> U e. P )
103 1 4 3 82 85 102 tgbtwntriv1 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( s I U ) )
104 101 103 elind 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( ( V L W ) i^i ( s I U ) ) )
105 104 ne0d 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( ( V L W ) i^i ( s I U ) ) =/= (/) )
106 80 81 105 3jca 
 |-  ( ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
107 106 anasss 
 |-  ( ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
108 79 107 impbida 
 |-  ( ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) /\ s e. P ) -> ( ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) <-> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) )
109 108 reubidva 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> ( E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) <-> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) )
110 75 109 mpbid 
 |-  ( ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) /\ -. U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
111 exmidd 
 |-  ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) -> ( U e. ( V L W ) \/ -. U e. ( V L W ) ) )
112 61 110 111 mpjaodan 
 |-  ( ( ph /\ X ( ( hlG ` G ) ` Y ) Z ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
113 7 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> G e. TarskiG )
114 11 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> X e. P )
115 12 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y e. P )
116 13 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> Z e. P )
117 8 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> U e. P )
118 9 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> V e. P )
119 10 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> W e. P )
120 16 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> X =/= Y )
121 17 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y =/= Z )
122 14 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> U =/= V )
123 15 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> V =/= W )
124 simpr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> U ( ( hlG ` G ) ` V ) W )
125 simplr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y e. ( Z I X ) )
126 1 4 3 113 116 115 114 125 tgbtwncom 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> Y e. ( X I Z ) )
127 1 2 3 4 5 6 113 114 115 116 117 118 119 120 121 122 123 124 126 angmndaddeu5 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
128 127 adantlr 
 |-  ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) /\ U ( ( hlG ` G ) ` V ) W ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
129 7 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> G e. TarskiG )
130 11 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> X e. P )
131 12 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> Y e. P )
132 13 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> Z e. P )
133 8 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> U e. P )
134 9 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> V e. P )
135 10 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> W e. P )
136 16 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> X =/= Y )
137 17 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> Y =/= Z )
138 14 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> U =/= V )
139 15 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> V =/= W )
140 simpr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> V e. ( W I U ) )
141 1 4 3 129 135 134 133 140 tgbtwncom 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> V e. ( U I W ) )
142 simplr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> Y e. ( Z I X ) )
143 1 4 3 129 132 131 130 142 tgbtwncom 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> Y e. ( X I Z ) )
144 1 2 3 4 5 6 129 130 131 132 133 134 135 136 137 138 139 141 143 angmndaddeu7 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ V e. ( W I U ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
145 144 adantlr 
 |-  ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) /\ V e. ( W I U ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
146 10 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> W e. P )
147 9 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> V e. P )
148 8 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> U e. P )
149 7 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> G e. TarskiG )
150 11 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> X e. P )
151 56 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> W =/= V )
152 simpr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> U e. ( V L W ) )
153 1 3 6 149 146 147 148 151 152 lncom 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> U e. ( W L V ) )
154 1 3 50 146 147 148 149 150 6 153 lnhl 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> ( U ( ( hlG ` G ) ` V ) W \/ V e. ( W I U ) ) )
155 128 145 154 mpjaodan 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
156 7 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> G e. TarskiG )
157 11 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> X e. P )
158 12 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> Y e. P )
159 13 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> Z e. P )
160 8 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> U e. P )
161 9 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> V e. P )
162 10 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> W e. P )
163 16 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> X =/= Y )
164 17 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> Y =/= Z )
165 14 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> U =/= V )
166 15 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> V =/= W )
167 simpr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> -. U e. ( V L W ) )
168 simplr 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> Y e. ( Z I X ) )
169 1 4 3 156 159 158 157 168 tgbtwncom 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> Y e. ( X I Z ) )
170 1 2 3 4 5 6 156 157 158 159 160 161 162 163 164 165 166 167 169 angmndaddeu3 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
171 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> <" W V s "> .~ <" X Y Z "> )
172 simplr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> ( V .- s ) = ( Y .- X ) )
173 171 172 jca 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
174 173 3anasss 
 |-  ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
175 simplr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" W V s "> .~ <" X Y Z "> )
176 simpr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( V .- s ) = ( Y .- X ) )
177 156 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> G e. TarskiG )
178 161 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V e. P )
179 162 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> W e. P )
180 simpllr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. P )
181 166 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V =/= W )
182 56 neneqd 
 |-  ( ph -> -. W = V )
183 182 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> -. W = V )
184 177 adantr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> G e. TarskiG )
185 179 adantr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> W e. P )
186 178 adantr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> V e. P )
187 157 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> X e. P )
188 158 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Y e. P )
189 159 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Z e. P )
190 5 a1i 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> .~ = ( cgrA ` G ) )
191 190 175 breqdi 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" W V s "> ( cgrA ` G ) <" X Y Z "> )
192 1 3 177 50 179 178 180 187 188 189 191 cgracom 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> <" X Y Z "> ( cgrA ` G ) <" W V s "> )
193 169 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> Y e. ( X I Z ) )
194 1 3 4 177 187 188 189 179 178 180 192 193 cgrabtwn 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V e. ( W I s ) )
195 194 adantr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> V e. ( W I s ) )
196 simpr 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> W = s )
197 196 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> ( W I W ) = ( W I s ) )
198 195 197 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> V e. ( W I W ) )
199 1 4 3 184 185 186 198 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) /\ W = s ) -> W = V )
200 183 199 mtand 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> -. W = s )
201 200 neqned 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> W =/= s )
202 1 3 6 177 179 180 178 201 194 btwnlng1 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> V e. ( W L s ) )
203 1 3 6 177 178 179 180 181 202 201 lnrot2 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( V L W ) )
204 160 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> U e. P )
205 1 4 3 177 180 204 tgbtwntriv1 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( s I U ) )
206 203 205 elind 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> s e. ( ( V L W ) i^i ( s I U ) ) )
207 206 ne0d 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( ( V L W ) i^i ( s I U ) ) =/= (/) )
208 175 176 207 3jca 
 |-  ( ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ <" W V s "> .~ <" X Y Z "> ) /\ ( V .- s ) = ( Y .- X ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
209 208 anasss 
 |-  ( ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) /\ ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) -> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) )
210 174 209 impbida 
 |-  ( ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) /\ s e. P ) -> ( ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) <-> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) )
211 210 reubidva 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> ( E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) /\ ( ( V L W ) i^i ( s I U ) ) =/= (/) ) <-> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) )
212 170 211 mpbid 
 |-  ( ( ( ph /\ Y e. ( Z I X ) ) /\ -. U e. ( V L W ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
213 exmidd 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> ( U e. ( V L W ) \/ -. U e. ( V L W ) ) )
214 155 212 213 mpjaodan 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
215 17 necomd 
 |-  ( ph -> Z =/= Y )
216 1 3 6 7 13 12 11 215 18 lncom 
 |-  ( ph -> X e. ( Z L Y ) )
217 1 3 50 13 12 11 7 11 6 216 lnhl 
 |-  ( ph -> ( X ( ( hlG ` G ) ` Y ) Z \/ Y e. ( Z I X ) ) )
218 112 214 217 mpjaodan 
 |-  ( ph -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )