let i, n, j, m be Element of NAT ; :: thesis: for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge D,n) & 1 <= j & j <= len (Gauge D,m) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds
((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge D,n) & 1 <= j & j <= len (Gauge D,m) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) implies ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2 )
set a = N-bound D;
set s = S-bound D;
set w = W-bound D;
set e = E-bound D;
set G = Gauge D,n;
set M = Gauge D,m;
assume A1:
( 1 <= i & i <= len (Gauge D,n) )
; :: thesis: ( not 1 <= j or not j <= len (Gauge D,m) or ( not ( n > 0 & m > 0 ) & not ( n = 0 & m = 0 ) ) or ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2 )
assume
( 1 <= j & j <= len (Gauge D,m) )
; :: thesis: ( ( not ( n > 0 & m > 0 ) & not ( n = 0 & m = 0 ) ) or ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2 )
then A2:
[j,(Center (Gauge D,m))] in Indices (Gauge D,m)
by Lm5;
A3:
[i,(Center (Gauge D,n))] in Indices (Gauge D,n)
by A1, Lm5;
assume A4:
( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) )
; :: thesis: ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2
per cases
( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) )
by A4;
suppose that A5:
n > 0
and A6:
m > 0
;
:: thesis: ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2 thus ((Gauge D,n) * i,(Center (Gauge D,n))) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((Center (Gauge D,n)) - 2)))]| `2
by A3, JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((Center (Gauge D,n)) - 2))
by EUCLID:56
.=
(S-bound D) + (((N-bound D) - (S-bound D)) / 2)
by A5, Lm6
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * ((Center (Gauge D,m)) - 2))
by A6, Lm6
.=
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * (j - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * ((Center (Gauge D,m)) - 2)))]| `2
by EUCLID:56
.=
((Gauge D,m) * j,(Center (Gauge D,m))) `2
by A2, JORDAN8:def 1
;
:: thesis: verum end; suppose A7:
(
n = 0 &
m = 0 )
;
:: thesis: ((Gauge D,n) * i,(Center (Gauge D,n))) `2 = ((Gauge D,m) * j,(Center (Gauge D,m))) `2 thus ((Gauge D,n) * i,(Center (Gauge D,n))) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((Center (Gauge D,n)) - 2)))]| `2
by A3, JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * ((Center (Gauge D,m)) - 2))
by A7, EUCLID:56
.=
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * (j - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * ((Center (Gauge D,m)) - 2)))]| `2
by EUCLID:56
.=
((Gauge D,m) * j,(Center (Gauge D,m))) `2
by A2, JORDAN8:def 1
;
:: thesis: verum end;