let i, j, n be Element of NAT ; :: thesis: for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
let G be Go-board; :: thesis: ( [i,j] in Indices G & [i,(j + n)] in Indices G implies dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 ) )
assume A1:
( [i,j] in Indices G & [i,(j + n)] in Indices G )
; :: thesis: dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
set x = G * i,j;
set y = G * i,(j + n);
per cases
( n = 0 or n <> 0 )
;
suppose A2:
n <> 0
;
:: thesis: dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )A3:
( 1
<= j + n &
j + n <= width 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) `1 =
(G * i,1) `1
by GOBOARD5:3
.=
(G * i,(j + n)) `1
by A3, A4, GOBOARD5:3
;
1
<= n
by A2, NAT_1:14;
then
j < j + n
by NAT_1:19;
then
(G * i,j) `2 < (G * i,(j + n)) `2
by A3, A4, GOBOARD5:5;
then A6:
((G * i,j) `2 ) - ((G * i,j) `2 ) < ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
by XREAL_1:16;
thus dist (G * i,j),
(G * i,(j + n)) =
sqrt (((((G * i,j) `1 ) - ((G * i,(j + n)) `1 )) ^2 ) + ((((G * i,j) `2 ) - ((G * i,(j + n)) `2 )) ^2 ))
by TOPREAL6:101
.=
abs (((G * i,j) `2 ) - ((G * i,(j + n)) `2 ))
by A5, COMPLEX1:158
.=
abs (- (((G * i,j) `2 ) - ((G * i,(j + n)) `2 )))
by COMPLEX1:138
.=
((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
by A6, ABSVALUE:def 1
;
:: thesis: verum end;