let n be Nat; for K being Field
for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let K be Field; for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
let a be Element of K; (n,n) --> a is_symmetry_circulant_about n |-> a
set p = n |-> a;
set M = (n,n) --> a;
A1:
( width ((n,n) --> a) = n & len (n |-> a) = n )
by CARD_1:def 7, MATRIX_0:24;
hence
len (n |-> a) = width ((n,n) --> a)
; MATRIX17:def 4 ( ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) ) & ( for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) ) )
A2:
Indices ((n,n) --> a) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
thus
for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a)))
for i, j being Nat st [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 holds
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))proof
let i,
j be
Nat;
( [i,j] in Indices ((n,n) --> a) & i + j <> (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a))) )
assume that A3:
[i,j] in Indices ((n,n) --> a)
and A4:
i + j <> (len (n |-> a)) + 1
;
((n,n) --> a) * (i,j) = (n |-> a) . (((i + j) - 1) mod (len (n |-> a)))
((Seg n) --> a) . (((i + j) - 1) mod (len (n |-> a))) = a
by A1, A2, A3, A4, Lm4, FUNCOP_1:7;
hence
((n,n) --> a) * (
i,
j)
= (n |-> a) . (((i + j) - 1) mod (len (n |-> a)))
by A3, MATRIX_0:46;
verum
end;
let i, j be Nat; ( [i,j] in Indices ((n,n) --> a) & i + j = (len (n |-> a)) + 1 implies ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a)) )
assume that
A5:
[i,j] in Indices ((n,n) --> a)
and
A6:
i + j = (len (n |-> a)) + 1
; ((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))
( i in Seg n & j in Seg n )
by A2, A5, ZFMISC_1:87;
then
( 1 <= i & 1 <= j )
by FINSEQ_1:1;
then
1 + 1 <= i + j
by XREAL_1:7;
then
((len (n |-> a)) + 1) - 1 >= (1 + 1) - 1
by A6, XREAL_1:9;
then A7:
len (n |-> a) in Seg (len (n |-> a))
;
((Seg n) --> a) . (len (n |-> a)) = a
by A1, A7, FUNCOP_1:7;
hence
((n,n) --> a) * (i,j) = (n |-> a) . (len (n |-> a))
by A5, MATRIX_0:46; verum