:: Some Basic Properties of Some Special Matrices, Part {III}
:: by Xiquan Liang and Tao Wang
::
:: Received October 23, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


Lm1: for n, i being Nat st i in Seg n holds
(n + 1) - i in Seg n

proof end;

Lm2: for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
( (n + 1) - j in Seg n & (n + 1) - i in Seg n )

proof end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attr M is subsymmetric means :Def1: :: MATRIX17:def 1
for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = M * (k,l);
end;

:: deftheorem Def1 defines subsymmetric MATRIX17:def 1 :
for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = M * (k,l) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster (n,n) --> a -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) subsymmetric for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
cluster - M -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = - M holds
b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
cluster M1 + M2 -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be subsymmetric Matrix of n,K;
cluster a * M -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = a * M holds
b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be subsymmetric Matrix of n,K;
cluster M1 - M2 -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is subsymmetric
;
end;

registration
let n be Nat;
let K be Field;
let M be subsymmetric Matrix of n,K;
cluster M @ -> subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M @ holds
b1 is subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster tabular V110( the carrier of K,n,n) line_circulant -> subsymmetric for FinSequence of the carrier of K * ;
coherence
for b1 being Matrix of n,K st b1 is line_circulant holds
b1 is subsymmetric
proof end;
cluster tabular V110( the carrier of K,n,n) col_circulant -> subsymmetric for FinSequence of the carrier of K * ;
coherence
for b1 being Matrix of n,K st b1 is col_circulant holds
b1 is subsymmetric
proof end;
end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attr M is Anti-subsymmetric means :Def2: :: MATRIX17:def 2
for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = - (M * (k,l));
end;

:: deftheorem Def2 defines Anti-subsymmetric MATRIX17:def 2 :
for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is Anti-subsymmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i holds
M * (i,j) = - (M * (k,l)) );

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) Anti-subsymmetric for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st b1 is Anti-subsymmetric
proof end;
end;

theorem :: MATRIX17:1
for K being Fanoian Field
for n, i, j, k, l being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds
M1 * (i,j) = 0. K
proof end;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
cluster - M -> Anti-subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = - M holds
b1 is Anti-subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
cluster M1 + M2 -> Anti-subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is Anti-subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be Anti-subsymmetric Matrix of n,K;
cluster a * M -> Anti-subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = a * M holds
b1 is Anti-subsymmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Anti-subsymmetric Matrix of n,K;
cluster M1 - M2 -> Anti-subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is Anti-subsymmetric
;
end;

registration
let n be Nat;
let K be Field;
let M be Anti-subsymmetric Matrix of n,K;
cluster M @ -> Anti-subsymmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M @ holds
b1 is Anti-subsymmetric
proof end;
end;

definition
let K be Field;
let n be Nat;
let M be Matrix of n,K;
attr M is central_symmetric means :Def3: :: MATRIX17:def 3
for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds
M * (i,j) = M * (k,l);
end;

:: deftheorem Def3 defines central_symmetric MATRIX17:def 3 :
for K being Field
for n being Nat
for M being Matrix of n,K holds
( M is central_symmetric iff for i, j, k, l being Nat st [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j holds
M * (i,j) = M * (k,l) );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster (n,n) --> a -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) central_symmetric for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
cluster - M -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = - M holds
b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
cluster M1 + M2 -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M be central_symmetric Matrix of n,K;
cluster a * M -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = a * M holds
b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be central_symmetric Matrix of n,K;
cluster M1 - M2 -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is central_symmetric
;
end;

registration
let n be Nat;
let K be Field;
let M be central_symmetric Matrix of n,K;
cluster M @ -> central_symmetric for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M @ holds
b1 is central_symmetric
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster tabular V110( the carrier of K,n,n) symmetric subsymmetric -> central_symmetric for FinSequence of the carrier of K * ;
coherence
for b1 being Matrix of n,K st b1 is symmetric & b1 is subsymmetric holds
b1 is central_symmetric
proof end;
end;

Lm3: for n, i, j being Nat st i in Seg n & j in Seg n & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n

proof end;

Lm4: for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n

proof end;

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
pred M is_symmetry_circulant_about p means :: MATRIX17:def 4
( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) );
end;

:: deftheorem defines is_symmetry_circulant_about MATRIX17:def 4 :
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_symmetry_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) ) );

theorem Th2: :: MATRIX17:2
for n being Nat
for K being Field
for a being Element of K holds (n,n) --> a is_symmetry_circulant_about n |-> a
proof end;

theorem Th3: :: MATRIX17:3
for n being Nat
for K being Field
for a being Element of K
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
a * M1 is_symmetry_circulant_about a * p
proof end;

theorem Th4: :: MATRIX17:4
for n being Nat
for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_symmetry_circulant_about p holds
- M1 is_symmetry_circulant_about - p
proof end;

theorem Th5: :: MATRIX17:5
for n being Nat
for K being Field
for p, q being FinSequence of K
for M1, M2 being Matrix of n,K st M1 is_symmetry_circulant_about p & M2 is_symmetry_circulant_about q holds
M1 + M2 is_symmetry_circulant_about p + q
proof end;

definition
let K be set ;
let M be Matrix of K;
attr M is symmetry_circulant means :Def5: :: MATRIX17:def 5
ex p being FinSequence of K st
( len p = width M & M is_symmetry_circulant_about p );
end;

:: deftheorem Def5 defines symmetry_circulant MATRIX17:def 5 :
for K being set
for M being Matrix of K holds
( M is symmetry_circulant iff ex p being FinSequence of K st
( len p = width M & M is_symmetry_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attr p is first-symmetry-of-circulant means :: MATRIX17:def 6
ex M being Matrix of len p,K st M is_symmetry_circulant_about p;
end;

:: deftheorem defines first-symmetry-of-circulant MATRIX17:def 6 :
for K being non empty set
for p being FinSequence of K holds
( p is first-symmetry-of-circulant iff ex M being Matrix of len p,K st M is_symmetry_circulant_about p );

definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-symmetry-of-circulant ;
func SCirc p -> Matrix of len p,K means :Def7: :: MATRIX17:def 7
it is_symmetry_circulant_about p;
existence
ex b1 being Matrix of len p,K st b1 is_symmetry_circulant_about p
by A1;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_symmetry_circulant_about p & b2 is_symmetry_circulant_about p holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines SCirc MATRIX17:def 7 :
for K being non empty set
for p being FinSequence of K st p is first-symmetry-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = SCirc p iff b3 is_symmetry_circulant_about p );

registration
let n be Nat;
let K be Field;
let a be Element of K;
cluster (n,n) --> a -> symmetry_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is symmetry_circulant
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular V110( the carrier of K,n,n) symmetry_circulant for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st b1 is symmetry_circulant
proof end;
end;

theorem Th6: :: MATRIX17:6
for n being Nat
for D being non empty set
for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
proof end;

registration
let n be Nat;
let K be Field;
let a be Element of K;
let M1 be symmetry_circulant Matrix of n,K;
cluster a * M1 -> symmetry_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = a * M1 holds
b1 is symmetry_circulant
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
cluster M1 + M2 -> symmetry_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 + M2 holds
b1 is symmetry_circulant
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1 be symmetry_circulant Matrix of n,K;
cluster - M1 -> symmetry_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = - M1 holds
b1 is symmetry_circulant
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be symmetry_circulant Matrix of n,K;
cluster M1 - M2 -> symmetry_circulant for Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = M1 - M2 holds
b1 is symmetry_circulant
;
end;

theorem :: MATRIX17:7
for n being Nat
for D being non empty set
for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
proof end;

theorem Th8: :: MATRIX17:8
for K being Field
for p being FinSequence of K st p is first-symmetry-of-circulant holds
- p is first-symmetry-of-circulant
proof end;

theorem :: MATRIX17:9
for K being Field
for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (- p) = - (SCirc p)
proof end;

theorem Th10: :: MATRIX17:10
for K being Field
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
p + q is first-symmetry-of-circulant
proof end;

theorem Th11: :: MATRIX17:11
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
proof end;

theorem Th12: :: MATRIX17:12
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
a * p is first-symmetry-of-circulant
proof end;

theorem Th13: :: MATRIX17:13
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
SCirc (a * p) = a * (SCirc p)
proof end;

theorem :: MATRIX17:14
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
(a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)
proof end;

theorem :: MATRIX17:15
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (a * (SCirc q)) = SCirc (a * (p + q))
proof end;

theorem :: MATRIX17:16
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds
(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))
proof end;

theorem Th17: :: MATRIX17:17
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
proof end;

registration
let n be Nat;
let K be Field;
cluster tabular V110( the carrier of K,n,n) symmetry_circulant -> symmetric for FinSequence of the carrier of K * ;
coherence
for b1 being Matrix of n,K st b1 is symmetry_circulant holds
b1 is symmetric
by Th17;
end;