set p = n |-> (0. K);
A1:
len (0. (K,n)) = n
by MATRIX_0:24;
A2:
0. (K,n,n) = n |-> (n |-> (0. K))
;
set M1 = 0. (K,n);
A3:
len (n |-> (0. K)) = n
by CARD_1:def 7;
A4:
Indices (0. (K,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) )
assume A5:
[i,j] in Indices (0. (K,n))
;
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
then
((i - j) mod n) + 1
in Seg n
by A4, Lm3;
then
((i - j) mod (len (n |-> (0. K)))) + 1
in Seg n
by CARD_1:def 7;
then
((Seg n) --> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) = 0. K
by FUNCOP_1:7;
hence
(0. (K,n)) * (
i,
j)
= (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
by A2, A5, MATRIX_3:1;
verum
end;
then A6:
0. (K,n) is_col_circulant_about n |-> (0. K)
by A1, A3;
A7:
width (0. (K,n)) = n
by MATRIX_0:24;
thus
0. (K,n) is line_circulant
0. (K,n) is col_circulant proof
for
i,
j being
Nat st
[i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (
i,
j)
= (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume A8:
[i,j] in Indices (0. (K,n))
;
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
then
((j - i) mod n) + 1
in Seg n
by A4, Lm3;
then
((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K
by FUNCOP_1:7;
hence
(0. (K,n)) * (
i,
j)
= (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
by A3, A2, A8, MATRIX_3:1;
verum
end;
then
0. (
K,
n)
is_line_circulant_about n |-> (0. K)
by A7, A3;
then consider p being
FinSequence of
K such that A9:
(
len p = width (0. (K,n)) &
0. (
K,
n)
is_line_circulant_about p )
;
take
p
;
MATRIX16:def 2 ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p )
thus
(
len p = width (0. (K,n)) &
0. (
K,
n)
is_line_circulant_about p )
by A9;
verum
end;
consider p being FinSequence of K such that
A10:
( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p )
by A6;
take
p
; MATRIX16:def 5 ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p )
thus
( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p )
by A10; verum