Metamath Proof Explorer

Theorem tgcgr4

Description: Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Hypotheses tgcgrxfr.p 
|- P = ( Base ` G )
tgcgrxfr.m 
|- .- = ( dist ` G )
tgcgrxfr.i 
|- I = ( Itv ` G )
tgcgrxfr.r 
|- .~ = ( cgrG ` G )
tgcgrxfr.g 
|- ( ph -> G e. TarskiG )
tgcgr4.a 
|- ( ph -> A e. P )
tgcgr4.b 
|- ( ph -> B e. P )
tgcgr4.c 
|- ( ph -> C e. P )
tgcgr4.d 
|- ( ph -> D e. P )
tgcgr4.w 
|- ( ph -> W e. P )
tgcgr4.x 
|- ( ph -> X e. P )
tgcgr4.y 
|- ( ph -> Y e. P )
tgcgr4.z 
|- ( ph -> Z e. P )
Assertion tgcgr4 
|- ( ph -> ( <" A B C D "> .~ <" W X Y Z "> <-> ( <" A B C "> .~ <" W X Y "> /\ ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p 
 |-  P = ( Base ` G )
2 tgcgrxfr.m 
 |-  .- = ( dist ` G )
3 tgcgrxfr.i 
 |-  I = ( Itv ` G )
4 tgcgrxfr.r 
 |-  .~ = ( cgrG ` G )
5 tgcgrxfr.g 
 |-  ( ph -> G e. TarskiG )
6 tgcgr4.a 
 |-  ( ph -> A e. P )
7 tgcgr4.b 
 |-  ( ph -> B e. P )
8 tgcgr4.c 
 |-  ( ph -> C e. P )
9 tgcgr4.d 
 |-  ( ph -> D e. P )
10 tgcgr4.w 
 |-  ( ph -> W e. P )
11 tgcgr4.x 
 |-  ( ph -> X e. P )
12 tgcgr4.y 
 |-  ( ph -> Y e. P )
13 tgcgr4.z 
 |-  ( ph -> Z e. P )
14 fzo0ssnn0 
 |-  ( 0 ..^ 4 ) C_ NN0
15 nn0ssre 
 |-  NN0 C_ RR
16 14 15 sstri 
 |-  ( 0 ..^ 4 ) C_ RR
17 16 a1i 
 |-  ( ph -> ( 0 ..^ 4 ) C_ RR )
18 6 7 8 9 s4cld 
 |-  ( ph -> <" A B C D "> e. Word P )
19 wrdf 
 |-  ( <" A B C D "> e. Word P -> <" A B C D "> : ( 0 ..^ ( # ` <" A B C D "> ) ) --> P )
20 18 19 syl 
 |-  ( ph -> <" A B C D "> : ( 0 ..^ ( # ` <" A B C D "> ) ) --> P )
21 s4len 
 |-  ( # ` <" A B C D "> ) = 4
22 21 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C D "> ) ) = ( 0 ..^ 4 )
23 22 feq2i 
 |-  ( <" A B C D "> : ( 0 ..^ ( # ` <" A B C D "> ) ) --> P <-> <" A B C D "> : ( 0 ..^ 4 ) --> P )
24 20 23 sylib 
 |-  ( ph -> <" A B C D "> : ( 0 ..^ 4 ) --> P )
25 10 11 12 13 s4cld 
 |-  ( ph -> <" W X Y Z "> e. Word P )
26 wrdf 
 |-  ( <" W X Y Z "> e. Word P -> <" W X Y Z "> : ( 0 ..^ ( # ` <" W X Y Z "> ) ) --> P )
27 25 26 syl 
 |-  ( ph -> <" W X Y Z "> : ( 0 ..^ ( # ` <" W X Y Z "> ) ) --> P )
28 s4len 
 |-  ( # ` <" W X Y Z "> ) = 4
29 28 oveq2i 
 |-  ( 0 ..^ ( # ` <" W X Y Z "> ) ) = ( 0 ..^ 4 )
30 29 feq2i 
 |-  ( <" W X Y Z "> : ( 0 ..^ ( # ` <" W X Y Z "> ) ) --> P <-> <" W X Y Z "> : ( 0 ..^ 4 ) --> P )
31 27 30 sylib 
 |-  ( ph -> <" W X Y Z "> : ( 0 ..^ 4 ) --> P )
32 1 2 4 5 17 24 31 iscgrglt 
 |-  ( ph -> ( <" A B C D "> .~ <" W X Y Z "> <-> A. i e. dom <" A B C D "> A. j e. dom <" A B C D "> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) ) )
33 24 fdmd 
 |-  ( ph -> dom <" A B C D "> = ( 0 ..^ 4 ) )
34 3p1e4 
 |-  ( 3 + 1 ) = 4
35 34 oveq2i 
 |-  ( 0 ..^ ( 3 + 1 ) ) = ( 0 ..^ 4 )
36 3nn0 
 |-  3 e. NN0
37 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
38 36 37 eleqtri 
 |-  3 e. ( ZZ>= ` 0 )
39 fzosplitsn 
 |-  ( 3 e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( 3 + 1 ) ) = ( ( 0 ..^ 3 ) u. { 3 } ) )
40 38 39 ax-mp 
 |-  ( 0 ..^ ( 3 + 1 ) ) = ( ( 0 ..^ 3 ) u. { 3 } )
41 35 40 eqtr3i 
 |-  ( 0 ..^ 4 ) = ( ( 0 ..^ 3 ) u. { 3 } )
42 33 41 eqtrdi 
 |-  ( ph -> dom <" A B C D "> = ( ( 0 ..^ 3 ) u. { 3 } ) )
43 42 raleqdv 
 |-  ( ph -> ( A. j e. dom <" A B C D "> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> A. j e. ( ( 0 ..^ 3 ) u. { 3 } ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) ) )
44 breq2 
 |-  ( j = 3 -> ( i < j <-> i < 3 ) )
45 fveq2 
 |-  ( j = 3 -> ( <" A B C D "> ` j ) = ( <" A B C D "> ` 3 ) )
46 45 oveq2d 
 |-  ( j = 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) )
47 fveq2 
 |-  ( j = 3 -> ( <" W X Y Z "> ` j ) = ( <" W X Y Z "> ` 3 ) )
48 47 oveq2d 
 |-  ( j = 3 -> ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) )
49 46 48 eqeq12d 
 |-  ( j = 3 -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) <-> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) )
50 44 49 imbi12d 
 |-  ( j = 3 -> ( ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
51 50 ralunsn 
 |-  ( 3 e. NN0 -> ( A. j e. ( ( 0 ..^ 3 ) u. { 3 } ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
52 36 51 ax-mp 
 |-  ( A. j e. ( ( 0 ..^ 3 ) u. { 3 } ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
53 43 52 bitrdi 
 |-  ( ph -> ( A. j e. dom <" A B C D "> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
54 53 ralbidv 
 |-  ( ph -> ( A. i e. dom <" A B C D "> A. j e. dom <" A B C D "> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> A. i e. dom <" A B C D "> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
55 42 raleqdv 
 |-  ( ph -> ( A. i e. dom <" A B C D "> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> A. i e. ( ( 0 ..^ 3 ) u. { 3 } ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
56 fzo0ssnn0 
 |-  ( 0 ..^ 3 ) C_ NN0
57 56 15 sstri 
 |-  ( 0 ..^ 3 ) C_ RR
58 simpr 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> j e. ( 0 ..^ 3 ) )
59 57 58 sseldi 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> j e. RR )
60 simpl 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> i = 3 )
61 3re 
 |-  3 e. RR
62 60 61 eqeltrdi 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> i e. RR )
63 elfzolt2 
 |-  ( j e. ( 0 ..^ 3 ) -> j < 3 )
64 63 adantl 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> j < 3 )
65 64 60 breqtrrd 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> j < i )
66 59 62 65 ltnsymd 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> -. i < j )
67 66 pm2.21d 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) )
68 tbtru 
 |-  ( ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> T. ) )
69 67 68 sylib 
 |-  ( ( i = 3 /\ j e. ( 0 ..^ 3 ) ) -> ( ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> T. ) )
70 69 ralbidva 
 |-  ( i = 3 -> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> A. j e. ( 0 ..^ 3 ) T. ) )
71 3nn 
 |-  3 e. NN
72 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 3 ) <-> 3 e. NN )
73 71 72 mpbir 
 |-  0 e. ( 0 ..^ 3 )
74 73 ne0ii 
 |-  ( 0 ..^ 3 ) =/= (/)
75 r19.3rzv 
 |-  ( ( 0 ..^ 3 ) =/= (/) -> ( T. <-> A. j e. ( 0 ..^ 3 ) T. ) )
76 74 75 ax-mp 
 |-  ( T. <-> A. j e. ( 0 ..^ 3 ) T. )
77 70 76 bitr4di 
 |-  ( i = 3 -> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> T. ) )
78 breq1 
 |-  ( i = 3 -> ( i < 3 <-> 3 < 3 ) )
79 61 ltnri 
 |-  -. 3 < 3
80 79 bifal 
 |-  ( 3 < 3 <-> F. )
81 78 80 bitrdi 
 |-  ( i = 3 -> ( i < 3 <-> F. ) )
82 81 imbi1d 
 |-  ( i = 3 -> ( ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( F. -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
83 falim 
 |-  ( F. -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) )
84 83 bitru 
 |-  ( ( F. -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> T. )
85 82 84 bitrdi 
 |-  ( i = 3 -> ( ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> T. ) )
86 77 85 anbi12d 
 |-  ( i = 3 -> ( ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( T. /\ T. ) ) )
87 anidm 
 |-  ( ( T. /\ T. ) <-> T. )
88 86 87 bitrdi 
 |-  ( i = 3 -> ( ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> T. ) )
89 88 ralunsn 
 |-  ( 3 e. NN0 -> ( A. i e. ( ( 0 ..^ 3 ) u. { 3 } ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) /\ T. ) ) )
90 36 89 ax-mp 
 |-  ( A. i e. ( ( 0 ..^ 3 ) u. { 3 } ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) /\ T. ) )
91 ancom 
 |-  ( ( A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) /\ T. ) <-> ( T. /\ A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
92 truan 
 |-  ( ( T. /\ A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) <-> A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
93 90 91 92 3bitri 
 |-  ( A. i e. ( ( 0 ..^ 3 ) u. { 3 } ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
94 55 93 bitrdi 
 |-  ( ph -> ( A. i e. dom <" A B C D "> ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
95 54 94 bitrd 
 |-  ( ph -> ( A. i e. dom <" A B C D "> A. j e. dom <" A B C D "> ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) ) )
96 r19.26 
 |-  ( A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ A. i e. ( 0 ..^ 3 ) ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
97 6 7 8 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
98 wrdf 
 |-  ( <" A B C "> e. Word P -> <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P )
99 97 98 syl 
 |-  ( ph -> <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P )
100 s3len 
 |-  ( # ` <" A B C "> ) = 3
101 100 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = ( 0 ..^ 3 )
102 101 feq2i 
 |-  ( <" A B C "> : ( 0 ..^ ( # ` <" A B C "> ) ) --> P <-> <" A B C "> : ( 0 ..^ 3 ) --> P )
103 99 102 sylib 
 |-  ( ph -> <" A B C "> : ( 0 ..^ 3 ) --> P )
104 103 fdmd 
 |-  ( ph -> dom <" A B C "> = ( 0 ..^ 3 ) )
105 104 raleqdv 
 |-  ( ph -> ( A. j e. dom <" A B C "> ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) <-> A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) ) )
106 104 105 raleqbidv 
 |-  ( ph -> ( A. i e. dom <" A B C "> A. j e. dom <" A B C "> ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) <-> A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) ) )
107 57 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) C_ RR )
108 10 11 12 s3cld 
 |-  ( ph -> <" W X Y "> e. Word P )
109 wrdf 
 |-  ( <" W X Y "> e. Word P -> <" W X Y "> : ( 0 ..^ ( # ` <" W X Y "> ) ) --> P )
110 108 109 syl 
 |-  ( ph -> <" W X Y "> : ( 0 ..^ ( # ` <" W X Y "> ) ) --> P )
111 s3len 
 |-  ( # ` <" W X Y "> ) = 3
112 111 oveq2i 
 |-  ( 0 ..^ ( # ` <" W X Y "> ) ) = ( 0 ..^ 3 )
113 112 feq2i 
 |-  ( <" W X Y "> : ( 0 ..^ ( # ` <" W X Y "> ) ) --> P <-> <" W X Y "> : ( 0 ..^ 3 ) --> P )
114 110 113 sylib 
 |-  ( ph -> <" W X Y "> : ( 0 ..^ 3 ) --> P )
115 1 2 4 5 107 103 114 iscgrglt 
 |-  ( ph -> ( <" A B C "> .~ <" W X Y "> <-> A. i e. dom <" A B C "> A. j e. dom <" A B C "> ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) ) )
116 df-s4 
 |-  <" A B C D "> = ( <" A B C "> ++ <" D "> )
117 116 fveq1i 
 |-  ( <" A B C D "> ` i ) = ( ( <" A B C "> ++ <" D "> ) ` i )
118 6 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> A e. P )
119 7 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> B e. P )
120 8 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> C e. P )
121 118 119 120 s3cld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> <" A B C "> e. Word P )
122 9 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> D e. P )
123 122 s1cld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> <" D "> e. Word P )
124 simprl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> i e. ( 0 ..^ 3 ) )
125 124 101 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> i e. ( 0 ..^ ( # ` <" A B C "> ) ) )
126 ccatval1 
 |-  ( ( <" A B C "> e. Word P /\ <" D "> e. Word P /\ i e. ( 0 ..^ ( # ` <" A B C "> ) ) ) -> ( ( <" A B C "> ++ <" D "> ) ` i ) = ( <" A B C "> ` i ) )
127 121 123 125 126 syl3anc 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" A B C "> ++ <" D "> ) ` i ) = ( <" A B C "> ` i ) )
128 117 127 syl5eq 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( <" A B C D "> ` i ) = ( <" A B C "> ` i ) )
129 116 fveq1i 
 |-  ( <" A B C D "> ` j ) = ( ( <" A B C "> ++ <" D "> ) ` j )
130 simprr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> j e. ( 0 ..^ 3 ) )
131 130 101 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> j e. ( 0 ..^ ( # ` <" A B C "> ) ) )
132 ccatval1 
 |-  ( ( <" A B C "> e. Word P /\ <" D "> e. Word P /\ j e. ( 0 ..^ ( # ` <" A B C "> ) ) ) -> ( ( <" A B C "> ++ <" D "> ) ` j ) = ( <" A B C "> ` j ) )
133 121 123 131 132 syl3anc 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" A B C "> ++ <" D "> ) ` j ) = ( <" A B C "> ` j ) )
134 129 133 syl5eq 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( <" A B C D "> ` j ) = ( <" A B C "> ` j ) )
135 128 134 oveq12d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) )
136 df-s4 
 |-  <" W X Y Z "> = ( <" W X Y "> ++ <" Z "> )
137 136 fveq1i 
 |-  ( <" W X Y Z "> ` i ) = ( ( <" W X Y "> ++ <" Z "> ) ` i )
138 10 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> W e. P )
139 11 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> X e. P )
140 12 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> Y e. P )
141 138 139 140 s3cld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> <" W X Y "> e. Word P )
142 13 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> Z e. P )
143 142 s1cld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> <" Z "> e. Word P )
144 124 112 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> i e. ( 0 ..^ ( # ` <" W X Y "> ) ) )
145 ccatval1 
 |-  ( ( <" W X Y "> e. Word P /\ <" Z "> e. Word P /\ i e. ( 0 ..^ ( # ` <" W X Y "> ) ) ) -> ( ( <" W X Y "> ++ <" Z "> ) ` i ) = ( <" W X Y "> ` i ) )
146 141 143 144 145 syl3anc 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" W X Y "> ++ <" Z "> ) ` i ) = ( <" W X Y "> ` i ) )
147 137 146 syl5eq 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( <" W X Y Z "> ` i ) = ( <" W X Y "> ` i ) )
148 136 fveq1i 
 |-  ( <" W X Y Z "> ` j ) = ( ( <" W X Y "> ++ <" Z "> ) ` j )
149 130 112 eleqtrrdi 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> j e. ( 0 ..^ ( # ` <" W X Y "> ) ) )
150 ccatval1 
 |-  ( ( <" W X Y "> e. Word P /\ <" Z "> e. Word P /\ j e. ( 0 ..^ ( # ` <" W X Y "> ) ) ) -> ( ( <" W X Y "> ++ <" Z "> ) ` j ) = ( <" W X Y "> ` j ) )
151 141 143 149 150 syl3anc 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" W X Y "> ++ <" Z "> ) ` j ) = ( <" W X Y "> ` j ) )
152 148 151 syl5eq 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( <" W X Y Z "> ` j ) = ( <" W X Y "> ` j ) )
153 147 152 oveq12d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) )
154 135 153 eqeq12d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) <-> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) )
155 154 imbi2d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ 3 ) /\ j e. ( 0 ..^ 3 ) ) ) -> ( ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) ) )
156 155 2ralbidva 
 |-  ( ph -> ( A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C "> ` i ) .- ( <" A B C "> ` j ) ) = ( ( <" W X Y "> ` i ) .- ( <" W X Y "> ` j ) ) ) ) )
157 106 115 156 3bitr4rd 
 |-  ( ph -> ( A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) <-> <" A B C "> .~ <" W X Y "> ) )
158 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
159 158 raleqi 
 |-  ( A. i e. ( 0 ..^ 3 ) ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> A. i e. { 0 , 1 , 2 } ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) )
160 3pos 
 |-  0 < 3
161 breq1 
 |-  ( i = 0 -> ( i < 3 <-> 0 < 3 ) )
162 160 161 mpbiri 
 |-  ( i = 0 -> i < 3 )
163 162 adantl 
 |-  ( ( ph /\ i = 0 ) -> i < 3 )
164 biimt 
 |-  ( i < 3 -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
165 163 164 syl 
 |-  ( ( ph /\ i = 0 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
166 fveq2 
 |-  ( i = 0 -> ( <" A B C D "> ` i ) = ( <" A B C D "> ` 0 ) )
167 s4fv0 
 |-  ( A e. P -> ( <" A B C D "> ` 0 ) = A )
168 6 167 syl 
 |-  ( ph -> ( <" A B C D "> ` 0 ) = A )
169 166 168 sylan9eqr 
 |-  ( ( ph /\ i = 0 ) -> ( <" A B C D "> ` i ) = A )
170 s4fv3 
 |-  ( D e. P -> ( <" A B C D "> ` 3 ) = D )
171 9 170 syl 
 |-  ( ph -> ( <" A B C D "> ` 3 ) = D )
172 171 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( <" A B C D "> ` 3 ) = D )
173 169 172 oveq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( A .- D ) )
174 fveq2 
 |-  ( i = 0 -> ( <" W X Y Z "> ` i ) = ( <" W X Y Z "> ` 0 ) )
175 s4fv0 
 |-  ( W e. P -> ( <" W X Y Z "> ` 0 ) = W )
176 10 175 syl 
 |-  ( ph -> ( <" W X Y Z "> ` 0 ) = W )
177 174 176 sylan9eqr 
 |-  ( ( ph /\ i = 0 ) -> ( <" W X Y Z "> ` i ) = W )
178 s4fv3 
 |-  ( Z e. P -> ( <" W X Y Z "> ` 3 ) = Z )
179 13 178 syl 
 |-  ( ph -> ( <" W X Y Z "> ` 3 ) = Z )
180 179 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( <" W X Y Z "> ` 3 ) = Z )
181 177 180 oveq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) = ( W .- Z ) )
182 173 181 eqeq12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( A .- D ) = ( W .- Z ) ) )
183 165 182 bitr3d 
 |-  ( ( ph /\ i = 0 ) -> ( ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( A .- D ) = ( W .- Z ) ) )
184 1lt3 
 |-  1 < 3
185 breq1 
 |-  ( i = 1 -> ( i < 3 <-> 1 < 3 ) )
186 184 185 mpbiri 
 |-  ( i = 1 -> i < 3 )
187 186 adantl 
 |-  ( ( ph /\ i = 1 ) -> i < 3 )
188 187 164 syl 
 |-  ( ( ph /\ i = 1 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
189 fveq2 
 |-  ( i = 1 -> ( <" A B C D "> ` i ) = ( <" A B C D "> ` 1 ) )
190 s4fv1 
 |-  ( B e. P -> ( <" A B C D "> ` 1 ) = B )
191 7 190 syl 
 |-  ( ph -> ( <" A B C D "> ` 1 ) = B )
192 189 191 sylan9eqr 
 |-  ( ( ph /\ i = 1 ) -> ( <" A B C D "> ` i ) = B )
193 171 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( <" A B C D "> ` 3 ) = D )
194 192 193 oveq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( B .- D ) )
195 fveq2 
 |-  ( i = 1 -> ( <" W X Y Z "> ` i ) = ( <" W X Y Z "> ` 1 ) )
196 s4fv1 
 |-  ( X e. P -> ( <" W X Y Z "> ` 1 ) = X )
197 11 196 syl 
 |-  ( ph -> ( <" W X Y Z "> ` 1 ) = X )
198 195 197 sylan9eqr 
 |-  ( ( ph /\ i = 1 ) -> ( <" W X Y Z "> ` i ) = X )
199 179 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( <" W X Y Z "> ` 3 ) = Z )
200 198 199 oveq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) = ( X .- Z ) )
201 194 200 eqeq12d 
 |-  ( ( ph /\ i = 1 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( B .- D ) = ( X .- Z ) ) )
202 188 201 bitr3d 
 |-  ( ( ph /\ i = 1 ) -> ( ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( B .- D ) = ( X .- Z ) ) )
203 2lt3 
 |-  2 < 3
204 breq1 
 |-  ( i = 2 -> ( i < 3 <-> 2 < 3 ) )
205 203 204 mpbiri 
 |-  ( i = 2 -> i < 3 )
206 205 adantl 
 |-  ( ( ph /\ i = 2 ) -> i < 3 )
207 206 164 syl 
 |-  ( ( ph /\ i = 2 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) )
208 fveq2 
 |-  ( i = 2 -> ( <" A B C D "> ` i ) = ( <" A B C D "> ` 2 ) )
209 s4fv2 
 |-  ( C e. P -> ( <" A B C D "> ` 2 ) = C )
210 8 209 syl 
 |-  ( ph -> ( <" A B C D "> ` 2 ) = C )
211 208 210 sylan9eqr 
 |-  ( ( ph /\ i = 2 ) -> ( <" A B C D "> ` i ) = C )
212 171 adantr 
 |-  ( ( ph /\ i = 2 ) -> ( <" A B C D "> ` 3 ) = D )
213 211 212 oveq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( C .- D ) )
214 fveq2 
 |-  ( i = 2 -> ( <" W X Y Z "> ` i ) = ( <" W X Y Z "> ` 2 ) )
215 s4fv2 
 |-  ( Y e. P -> ( <" W X Y Z "> ` 2 ) = Y )
216 12 215 syl 
 |-  ( ph -> ( <" W X Y Z "> ` 2 ) = Y )
217 214 216 sylan9eqr 
 |-  ( ( ph /\ i = 2 ) -> ( <" W X Y Z "> ` i ) = Y )
218 179 adantr 
 |-  ( ( ph /\ i = 2 ) -> ( <" W X Y Z "> ` 3 ) = Z )
219 217 218 oveq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) = ( Y .- Z ) )
220 213 219 eqeq12d 
 |-  ( ( ph /\ i = 2 ) -> ( ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) <-> ( C .- D ) = ( Y .- Z ) ) )
221 207 220 bitr3d 
 |-  ( ( ph /\ i = 2 ) -> ( ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( C .- D ) = ( Y .- Z ) ) )
222 0red 
 |-  ( ph -> 0 e. RR )
223 1red 
 |-  ( ph -> 1 e. RR )
224 2re 
 |-  2 e. RR
225 224 a1i 
 |-  ( ph -> 2 e. RR )
226 183 202 221 222 223 225 raltpd 
 |-  ( ph -> ( A. i e. { 0 , 1 , 2 } ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) )
227 159 226 syl5bb 
 |-  ( ph -> ( A. i e. ( 0 ..^ 3 ) ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) <-> ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) )
228 157 227 anbi12d 
 |-  ( ph -> ( ( A. i e. ( 0 ..^ 3 ) A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ A. i e. ( 0 ..^ 3 ) ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( <" A B C "> .~ <" W X Y "> /\ ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) ) )
229 96 228 syl5bb 
 |-  ( ph -> ( A. i e. ( 0 ..^ 3 ) ( A. j e. ( 0 ..^ 3 ) ( i < j -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` j ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` j ) ) ) /\ ( i < 3 -> ( ( <" A B C D "> ` i ) .- ( <" A B C D "> ` 3 ) ) = ( ( <" W X Y Z "> ` i ) .- ( <" W X Y Z "> ` 3 ) ) ) ) <-> ( <" A B C "> .~ <" W X Y "> /\ ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) ) )
230 32 95 229 3bitrd 
 |-  ( ph -> ( <" A B C D "> .~ <" W X Y Z "> <-> ( <" A B C "> .~ <" W X Y "> /\ ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) ) )