Metamath Proof Explorer

Theorem iscgrglt

Description: The property for two sequences A and B of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Hypotheses trgcgrg.p 
|- P = ( Base ` G )
trgcgrg.m 
|- .- = ( dist ` G )
trgcgrg.r 
|- .~ = ( cgrG ` G )
trgcgrg.g 
|- ( ph -> G e. TarskiG )
iscgrglt.d 
|- ( ph -> D C_ RR )
iscgrglt.a 
|- ( ph -> A : D --> P )
iscgrglt.b 
|- ( ph -> B : D --> P )
Assertion iscgrglt 
|- ( ph -> ( A .~ B <-> A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 trgcgrg.p 
 |-  P = ( Base ` G )
2 trgcgrg.m 
 |-  .- = ( dist ` G )
3 trgcgrg.r 
 |-  .~ = ( cgrG ` G )
4 trgcgrg.g 
 |-  ( ph -> G e. TarskiG )
5 iscgrglt.d 
 |-  ( ph -> D C_ RR )
6 iscgrglt.a 
 |-  ( ph -> A : D --> P )
7 iscgrglt.b 
 |-  ( ph -> B : D --> P )
8 1 2 3 4 5 6 7 iscgrgd 
 |-  ( ph -> ( A .~ B <-> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
9 simp2 
 |-  ( ( ( ph /\ ( i e. dom A /\ j e. dom A ) ) /\ ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) /\ i < j ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
10 9 3exp 
 |-  ( ( ph /\ ( i e. dom A /\ j e. dom A ) ) -> ( ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) -> ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
11 10 ralimdvva 
 |-  ( ph -> ( A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) -> A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
12 breq1 
 |-  ( k = i -> ( k < l <-> i < l ) )
13 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
14 13 oveq1d 
 |-  ( k = i -> ( ( A ` k ) .- ( A ` l ) ) = ( ( A ` i ) .- ( A ` l ) ) )
15 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
16 15 oveq1d 
 |-  ( k = i -> ( ( B ` k ) .- ( B ` l ) ) = ( ( B ` i ) .- ( B ` l ) ) )
17 14 16 eqeq12d 
 |-  ( k = i -> ( ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) <-> ( ( A ` i ) .- ( A ` l ) ) = ( ( B ` i ) .- ( B ` l ) ) ) )
18 12 17 imbi12d 
 |-  ( k = i -> ( ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) <-> ( i < l -> ( ( A ` i ) .- ( A ` l ) ) = ( ( B ` i ) .- ( B ` l ) ) ) ) )
19 breq2 
 |-  ( l = j -> ( i < l <-> i < j ) )
20 fveq2 
 |-  ( l = j -> ( A ` l ) = ( A ` j ) )
21 20 oveq2d 
 |-  ( l = j -> ( ( A ` i ) .- ( A ` l ) ) = ( ( A ` i ) .- ( A ` j ) ) )
22 fveq2 
 |-  ( l = j -> ( B ` l ) = ( B ` j ) )
23 22 oveq2d 
 |-  ( l = j -> ( ( B ` i ) .- ( B ` l ) ) = ( ( B ` i ) .- ( B ` j ) ) )
24 21 23 eqeq12d 
 |-  ( l = j -> ( ( ( A ` i ) .- ( A ` l ) ) = ( ( B ` i ) .- ( B ` l ) ) <-> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
25 19 24 imbi12d 
 |-  ( l = j -> ( ( i < l -> ( ( A ` i ) .- ( A ` l ) ) = ( ( B ` i ) .- ( B ` l ) ) ) <-> ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
26 18 25 cbvral2vw 
 |-  ( A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) <-> A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
27 simpllr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> i e. dom A )
28 simplr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> j e. dom A )
29 simp-4r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) )
30 27 28 29 jca31 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> ( ( i e. dom A /\ j e. dom A ) /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) )
31 simpr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> i < j )
32 18 25 rspc2va 
 |-  ( ( ( i e. dom A /\ j e. dom A ) /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) -> ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
33 30 31 32 sylc 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i < j ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
34 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
35 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> G e. TarskiG )
36 6 ad2antrr 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> A : D --> P )
37 simplr 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> i e. dom A )
38 36 fdmd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> dom A = D )
39 37 38 eleqtrd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> i e. D )
40 36 39 ffvelcdmd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> ( A ` i ) e. P )
41 40 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( A ` i ) e. P )
42 7 ad2antrr 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> B : D --> P )
43 42 39 ffvelcdmd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> ( B ` i ) e. P )
44 43 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( B ` i ) e. P )
45 1 2 34 35 41 44 tgcgrtriv 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( ( A ` i ) .- ( A ` i ) ) = ( ( B ` i ) .- ( B ` i ) ) )
46 simpr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> i = j )
47 46 fveq2d 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( A ` i ) = ( A ` j ) )
48 47 oveq2d 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( ( A ` i ) .- ( A ` i ) ) = ( ( A ` i ) .- ( A ` j ) ) )
49 46 fveq2d 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( B ` i ) = ( B ` j ) )
50 49 oveq2d 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( ( B ` i ) .- ( B ` i ) ) = ( ( B ` i ) .- ( B ` j ) ) )
51 45 48 50 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
52 51 adantl3r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ i = j ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
53 4 ad4antr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> G e. TarskiG )
54 simpr 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> j e. dom A )
55 54 38 eleqtrd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> j e. D )
56 36 55 ffvelcdmd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> ( A ` j ) e. P )
57 56 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( A ` j ) e. P )
58 57 adantl3r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( A ` j ) e. P )
59 40 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( A ` i ) e. P )
60 59 adantl3r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( A ` i ) e. P )
61 42 55 ffvelcdmd 
 |-  ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) -> ( B ` j ) e. P )
62 61 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( B ` j ) e. P )
63 62 adantl3r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( B ` j ) e. P )
64 43 adantr 
 |-  ( ( ( ( ph /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( B ` i ) e. P )
65 64 adantl3r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( B ` i ) e. P )
66 simplr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> j e. dom A )
67 simpllr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> i e. dom A )
68 simp-4r 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) )
69 66 67 68 jca31 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( ( j e. dom A /\ i e. dom A ) /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) )
70 simpr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> j < i )
71 breq1 
 |-  ( k = j -> ( k < l <-> j < l ) )
72 fveq2 
 |-  ( k = j -> ( A ` k ) = ( A ` j ) )
73 72 oveq1d 
 |-  ( k = j -> ( ( A ` k ) .- ( A ` l ) ) = ( ( A ` j ) .- ( A ` l ) ) )
74 fveq2 
 |-  ( k = j -> ( B ` k ) = ( B ` j ) )
75 74 oveq1d 
 |-  ( k = j -> ( ( B ` k ) .- ( B ` l ) ) = ( ( B ` j ) .- ( B ` l ) ) )
76 73 75 eqeq12d 
 |-  ( k = j -> ( ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) <-> ( ( A ` j ) .- ( A ` l ) ) = ( ( B ` j ) .- ( B ` l ) ) ) )
77 71 76 imbi12d 
 |-  ( k = j -> ( ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) <-> ( j < l -> ( ( A ` j ) .- ( A ` l ) ) = ( ( B ` j ) .- ( B ` l ) ) ) ) )
78 breq2 
 |-  ( l = i -> ( j < l <-> j < i ) )
79 fveq2 
 |-  ( l = i -> ( A ` l ) = ( A ` i ) )
80 79 oveq2d 
 |-  ( l = i -> ( ( A ` j ) .- ( A ` l ) ) = ( ( A ` j ) .- ( A ` i ) ) )
81 fveq2 
 |-  ( l = i -> ( B ` l ) = ( B ` i ) )
82 81 oveq2d 
 |-  ( l = i -> ( ( B ` j ) .- ( B ` l ) ) = ( ( B ` j ) .- ( B ` i ) ) )
83 80 82 eqeq12d 
 |-  ( l = i -> ( ( ( A ` j ) .- ( A ` l ) ) = ( ( B ` j ) .- ( B ` l ) ) <-> ( ( A ` j ) .- ( A ` i ) ) = ( ( B ` j ) .- ( B ` i ) ) ) )
84 78 83 imbi12d 
 |-  ( l = i -> ( ( j < l -> ( ( A ` j ) .- ( A ` l ) ) = ( ( B ` j ) .- ( B ` l ) ) ) <-> ( j < i -> ( ( A ` j ) .- ( A ` i ) ) = ( ( B ` j ) .- ( B ` i ) ) ) ) )
85 77 84 rspc2va 
 |-  ( ( ( j e. dom A /\ i e. dom A ) /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) -> ( j < i -> ( ( A ` j ) .- ( A ` i ) ) = ( ( B ` j ) .- ( B ` i ) ) ) )
86 69 70 85 sylc 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( ( A ` j ) .- ( A ` i ) ) = ( ( B ` j ) .- ( B ` i ) ) )
87 1 2 34 53 58 60 63 65 86 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) /\ j < i ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
88 6 fdmd 
 |-  ( ph -> dom A = D )
89 88 5 eqsstrd 
 |-  ( ph -> dom A C_ RR )
90 89 ad3antrrr 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> dom A C_ RR )
91 simplr 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> i e. dom A )
92 90 91 sseldd 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> i e. RR )
93 simpr 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> j e. dom A )
94 90 93 sseldd 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> j e. RR )
95 92 94 lttri4d 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> ( i < j \/ i = j \/ j < i ) )
96 33 52 87 95 mpjao3dan 
 |-  ( ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ i e. dom A ) /\ j e. dom A ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
97 96 anasss 
 |-  ( ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) /\ ( i e. dom A /\ j e. dom A ) ) -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
98 97 ralrimivva 
 |-  ( ( ph /\ A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) ) -> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) )
99 98 ex 
 |-  ( ph -> ( A. k e. dom A A. l e. dom A ( k < l -> ( ( A ` k ) .- ( A ` l ) ) = ( ( B ` k ) .- ( B ` l ) ) ) -> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
100 26 99 biimtrrid 
 |-  ( ph -> ( A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) -> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
101 11 100 impbid 
 |-  ( ph -> ( A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) <-> A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
102 8 101 bitrd 
 |-  ( ph -> ( A .~ B <-> A. i e. dom A A. j e. dom A ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )