let i, j, n be Nat; for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds
dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
let G be Go-board; ( [i,j] in Indices G & [(i + n),j] in Indices G implies dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) )
assume that
A1:
[i,j] in Indices G
and
A2:
[(i + n),j] in Indices G
; dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
set x = G * (i,j);
set y = G * ((i + n),j);
per cases
( n = 0 or n <> 0 )
;
suppose A3:
n <> 0
;
dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)A4:
i + n <= len G
by A2, MATRIX_0:32;
A5:
1
<= i
by A1, MATRIX_0:32;
A6:
1
<= i + n
by A2, MATRIX_0:32;
A7:
( 1
<= j &
j <= width G )
by A1, MATRIX_0:32;
1
<= n
by A3, NAT_1:14;
then
i < i + n
by NAT_1:19;
then
(G * (i,j)) `1 < (G * ((i + n),j)) `1
by A4, A7, A5, GOBOARD5:3;
then A8:
((G * (i,j)) `1) - ((G * (i,j)) `1) < ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
by XREAL_1:14;
i <= len G
by A1, MATRIX_0:32;
then A9:
(G * (i,j)) `2 =
(G * (1,j)) `2
by A7, A5, GOBOARD5:1
.=
(G * ((i + n),j)) `2
by A6, A4, A7, GOBOARD5:1
;
thus dist (
(G * (i,j)),
(G * ((i + n),j))) =
sqrt (((((G * (i,j)) `1) - ((G * ((i + n),j)) `1)) ^2) + ((((G * (i,j)) `2) - ((G * ((i + n),j)) `2)) ^2))
by TOPREAL6:92
.=
|.(((G * (i,j)) `1) - ((G * ((i + n),j)) `1)).|
by A9, COMPLEX1:72
.=
|.(- (((G * (i,j)) `1) - ((G * ((i + n),j)) `1))).|
by COMPLEX1:52
.=
((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
by A8, ABSVALUE:def 1
;
verum end;