set M = GoB (v1,v2);
A1:
len (GoB (v1,v2)) = len v1
by Def1;
then A2:
dom (GoB (v1,v2)) = dom v1
by FINSEQ_3:29;
A3:
width (GoB (v1,v2)) = len v2
by Def1;
hence
GoB (v1,v2) is V3()
by A1, MATRIX_0:def 10; ( GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column )
A4:
Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):]
by A3, A2, MATRIX_0:def 4;
thus
GoB (v1,v2) is X_equal-in-line
GoB (v1,v2) is Y_equal-in-column proof
let n be
Nat;
GOBOARD1:def 4 ( not n in dom (GoB (v1,v2)) or X_axis (Line ((GoB (v1,v2)),n)) is constant )
reconsider l =
Line (
(GoB (v1,v2)),
n) as
FinSequence of
(TOP-REAL 2) ;
set x =
X_axis l;
assume A5:
n in dom (GoB (v1,v2))
;
X_axis (Line ((GoB (v1,v2)),n)) is constant
A6:
(
len l = width (GoB (v1,v2)) &
dom (X_axis l) = Seg (len (X_axis l)) )
by FINSEQ_1:def 3, MATRIX_0:def 7;
A7:
len (X_axis l) = len l
by GOBOARD1:def 1;
then A8:
dom (X_axis l) = dom l
by FINSEQ_3:29;
now for i, j being Nat st i in dom (X_axis l) & j in dom (X_axis l) holds
(X_axis l) . i = (X_axis l) . jlet i,
j be
Nat;
( i in dom (X_axis l) & j in dom (X_axis l) implies (X_axis l) . i = (X_axis l) . j )assume that A9:
i in dom (X_axis l)
and A10:
j in dom (X_axis l)
;
(X_axis l) . i = (X_axis l) . jreconsider r =
v1 . n,
s1 =
v2 . i,
s2 =
v2 . j as
Real ;
[n,i] in Indices (GoB (v1,v2))
by A3, A2, A4, A5, A7, A6, A9, ZFMISC_1:87;
then
(GoB (v1,v2)) * (
n,
i)
= |[r,s1]|
by Def1;
then A11:
((GoB (v1,v2)) * (n,i)) `1 = r
by EUCLID:52;
l /. i = l . i
by A8, A9, PARTFUN1:def 6;
then
l /. i = (GoB (v1,v2)) * (
n,
i)
by A7, A6, A9, MATRIX_0:def 7;
then A12:
(X_axis l) . i = r
by A9, A11, GOBOARD1:def 1;
[n,j] in Indices (GoB (v1,v2))
by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:87;
then
(GoB (v1,v2)) * (
n,
j)
= |[r,s2]|
by Def1;
then A13:
((GoB (v1,v2)) * (n,j)) `1 = r
by EUCLID:52;
l /. j = l . j
by A8, A10, PARTFUN1:def 6;
then
l /. j = (GoB (v1,v2)) * (
n,
j)
by A7, A6, A10, MATRIX_0:def 7;
hence
(X_axis l) . i = (X_axis l) . j
by A10, A13, A12, GOBOARD1:def 1;
verum end;
hence
X_axis (Line ((GoB (v1,v2)),n)) is
constant
by SEQM_3:def 10;
verum
end;
thus
GoB (v1,v2) is Y_equal-in-column
verumproof
let n be
Nat;
GOBOARD1:def 5 ( not n in Seg (width (GoB (v1,v2))) or Y_axis (Col ((GoB (v1,v2)),n)) is constant )
reconsider c =
Col (
(GoB (v1,v2)),
n) as
FinSequence of
(TOP-REAL 2) ;
set y =
Y_axis c;
len (Y_axis c) = len c
by GOBOARD1:def 2;
then A14:
dom (Y_axis c) = dom c
by FINSEQ_3:29;
len c = len (GoB (v1,v2))
by MATRIX_0:def 8;
then A15:
dom c = dom (GoB (v1,v2))
by FINSEQ_3:29;
assume A16:
n in Seg (width (GoB (v1,v2)))
;
Y_axis (Col ((GoB (v1,v2)),n)) is constant
now for i, j being Nat st i in dom (Y_axis c) & j in dom (Y_axis c) holds
(Y_axis c) . i = (Y_axis c) . jlet i,
j be
Nat;
( i in dom (Y_axis c) & j in dom (Y_axis c) implies (Y_axis c) . i = (Y_axis c) . j )assume that A17:
i in dom (Y_axis c)
and A18:
j in dom (Y_axis c)
;
(Y_axis c) . i = (Y_axis c) . jreconsider r =
v2 . n,
s1 =
v1 . i,
s2 =
v1 . j as
Real ;
[i,n] in Indices (GoB (v1,v2))
by A3, A2, A4, A16, A14, A15, A17, ZFMISC_1:87;
then
(GoB (v1,v2)) * (
i,
n)
= |[s1,r]|
by Def1;
then A19:
((GoB (v1,v2)) * (i,n)) `2 = r
by EUCLID:52;
c /. i = c . i
by A14, A17, PARTFUN1:def 6;
then
c /. i = (GoB (v1,v2)) * (
i,
n)
by A14, A15, A17, MATRIX_0:def 8;
then A20:
(Y_axis c) . i = r
by A17, A19, GOBOARD1:def 2;
[j,n] in Indices (GoB (v1,v2))
by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:87;
then
(GoB (v1,v2)) * (
j,
n)
= |[s2,r]|
by Def1;
then A21:
((GoB (v1,v2)) * (j,n)) `2 = r
by EUCLID:52;
c /. j = c . j
by A14, A18, PARTFUN1:def 6;
then
c /. j = (GoB (v1,v2)) * (
j,
n)
by A14, A15, A18, MATRIX_0:def 8;
hence
(Y_axis c) . i = (Y_axis c) . j
by A18, A21, A20, GOBOARD1:def 2;
verum end;
hence
Y_axis (Col ((GoB (v1,v2)),n)) is
constant
by SEQM_3:def 10;
verum
end;