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
|
ffvelrnd |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
syl5bir |
|- ( 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 ) ) ) ) ) |