let i, j, n be Element of NAT ; :: thesis: 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; :: thesis: ( [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 A1:
( [i,j] in Indices G & [(i + n),j] in Indices G )
; :: thesis: 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 A2:
n <> 0
;
:: thesis: dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )A3:
( 1
<= i + n &
i + n <= len G )
by A1, MATRIX_1:39;
A4:
( 1
<= j &
j <= width G & 1
<= i &
i <= len G )
by A1, MATRIX_1:39;
then A5:
(G * i,j) `2 =
(G * 1,j) `2
by GOBOARD5:2
.=
(G * (i + n),j) `2
by A3, A4, GOBOARD5:2
;
1
<= n
by A2, NAT_1:14;
then
i < i + n
by NAT_1:19;
then
(G * i,j) `1 < (G * (i + n),j) `1
by A3, A4, GOBOARD5:4;
then A6:
((G * i,j) `1 ) - ((G * i,j) `1 ) < ((G * (i + n),j) `1 ) - ((G * i,j) `1 )
by XREAL_1:16;
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:101
.=
abs (((G * i,j) `1 ) - ((G * (i + n),j) `1 ))
by A5, COMPLEX1:158
.=
abs (- (((G * i,j) `1 ) - ((G * (i + n),j) `1 )))
by COMPLEX1:138
.=
((G * (i + n),j) `1 ) - ((G * i,j) `1 )
by A6, ABSVALUE:def 1
;
:: thesis: verum end;