set M = Gauge C,n;
( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) )
by Def1;
hence
not Gauge C,n is empty-yielding
by GOBOARD1:def 5; :: thesis: ( Gauge C,n is X_equal-in-line & Gauge C,n is Y_equal-in-column )
A1:
Indices (Gauge C,n) = [:(dom (Gauge C,n)),(Seg (width (Gauge C,n))):]
by MATRIX_1:def 5;
thus
Gauge C,n is X_equal-in-line
:: thesis: Gauge C,n is Y_equal-in-column proof
let i be
Element of
NAT ;
:: according to GOBOARD1:def 6 :: thesis: ( not i in dom (Gauge C,n) or X_axis (Line (Gauge C,n),i) is constant )
assume A2:
i in dom (Gauge C,n)
;
:: thesis: X_axis (Line (Gauge C,n),i) is constant
set l =
Line (Gauge C,n),
i;
set f =
X_axis (Line (Gauge C,n),i);
let j1 be
Element of
NAT ;
:: according to GOBOARD1:def 2 :: thesis: for b1 being Element of NAT holds
( not j1 in dom (X_axis (Line (Gauge C,n),i)) or not b1 in dom (X_axis (Line (Gauge C,n),i)) or (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . b1 )let j2 be
Element of
NAT ;
:: thesis: ( not j1 in dom (X_axis (Line (Gauge C,n),i)) or not j2 in dom (X_axis (Line (Gauge C,n),i)) or (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . j2 )
assume that A3:
j1 in dom (X_axis (Line (Gauge C,n),i))
and A4:
j2 in dom (X_axis (Line (Gauge C,n),i))
;
:: thesis: (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . j2
len (Line (Gauge C,n),i) = width (Gauge C,n)
by MATRIX_1:def 8;
then A5:
dom (Line (Gauge C,n),i) = Seg (width (Gauge C,n))
by FINSEQ_1:def 3;
A6:
dom (X_axis (Line (Gauge C,n),i)) = dom (Line (Gauge C,n),i)
by SPRECT_2:19;
then A7:
(Line (Gauge C,n),i) /. j1 =
(Line (Gauge C,n),i) . j1
by A3, PARTFUN1:def 8
.=
(Gauge C,n) * i,
j1
by A3, A5, A6, MATRIX_1:def 8
;
A8:
[i,j1] in Indices (Gauge C,n)
by A1, A2, A3, A5, A6, ZFMISC_1:106;
A9:
(Line (Gauge C,n),i) /. j2 =
(Line (Gauge C,n),i) . j2
by A4, A6, PARTFUN1:def 8
.=
(Gauge C,n) * i,
j2
by A4, A5, A6, MATRIX_1:def 8
;
A10:
[i,j2] in Indices (Gauge C,n)
by A1, A2, A4, A5, A6, ZFMISC_1:106;
set x =
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2));
set d =
((N-bound C) - (S-bound C)) / (2 |^ n);
thus (X_axis (Line (Gauge C,n),i)) . j1 =
((Line (Gauge C,n),i) /. j1) `1
by A3, GOBOARD1:def 3
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)))]| `1
by A7, A8, Def1
.=
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))
by EUCLID:56
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)))]| `1
by EUCLID:56
.=
((Line (Gauge C,n),i) /. j2) `1
by A9, A10, Def1
.=
(X_axis (Line (Gauge C,n),i)) . j2
by A4, GOBOARD1:def 3
;
:: thesis: verum
end;
thus
Gauge C,n is Y_equal-in-column
:: thesis: verumproof
let j be
Element of
NAT ;
:: according to GOBOARD1:def 7 :: thesis: ( not j in Seg (width (Gauge C,n)) or Y_axis (Col (Gauge C,n),j) is constant )
assume A11:
j in Seg (width (Gauge C,n))
;
:: thesis: Y_axis (Col (Gauge C,n),j) is constant
set c =
Col (Gauge C,n),
j;
set f =
Y_axis (Col (Gauge C,n),j);
let i1 be
Element of
NAT ;
:: according to GOBOARD1:def 2 :: thesis: for b1 being Element of NAT holds
( not i1 in dom (Y_axis (Col (Gauge C,n),j)) or not b1 in dom (Y_axis (Col (Gauge C,n),j)) or (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . b1 )let i2 be
Element of
NAT ;
:: thesis: ( not i1 in dom (Y_axis (Col (Gauge C,n),j)) or not i2 in dom (Y_axis (Col (Gauge C,n),j)) or (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . i2 )
assume that A12:
i1 in dom (Y_axis (Col (Gauge C,n),j))
and A13:
i2 in dom (Y_axis (Col (Gauge C,n),j))
;
:: thesis: (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . i2
len (Col (Gauge C,n),j) = len (Gauge C,n)
by MATRIX_1:def 9;
then A14:
dom (Col (Gauge C,n),j) = dom (Gauge C,n)
by FINSEQ_3:31;
A15:
dom (Y_axis (Col (Gauge C,n),j)) = dom (Col (Gauge C,n),j)
by SPRECT_2:20;
then A16:
(Col (Gauge C,n),j) /. i1 =
(Col (Gauge C,n),j) . i1
by A12, PARTFUN1:def 8
.=
(Gauge C,n) * i1,
j
by A12, A14, A15, MATRIX_1:def 9
;
A17:
[i1,j] in Indices (Gauge C,n)
by A1, A11, A12, A14, A15, ZFMISC_1:106;
A18:
(Col (Gauge C,n),j) /. i2 =
(Col (Gauge C,n),j) . i2
by A13, A15, PARTFUN1:def 8
.=
(Gauge C,n) * i2,
j
by A13, A14, A15, MATRIX_1:def 9
;
A19:
[i2,j] in Indices (Gauge C,n)
by A1, A11, A13, A14, A15, ZFMISC_1:106;
set y =
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2));
set d =
((E-bound C) - (W-bound C)) / (2 |^ n);
thus (Y_axis (Col (Gauge C,n),j)) . i1 =
((Col (Gauge C,n),j) /. i1) `2
by A12, GOBOARD1:def 4
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2
by A16, A17, Def1
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))
by EUCLID:56
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2
by EUCLID:56
.=
((Col (Gauge C,n),j) /. i2) `2
by A18, A19, Def1
.=
(Y_axis (Col (Gauge C,n),j)) . i2
by A13, GOBOARD1:def 4
;
:: thesis: verum
end;