:: 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 b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ 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 b₁ being Matrix of n,K st b₁ 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 b₁ being Matrix of n,K st b₁ = - M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 + M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = a * M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 - M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M @ holds
b₁ 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 b₁ being Matrix of n,K st b₁ is line_circulant holds
b₁ 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 b₁ being Matrix of n,K st b₁ is col_circulant holds
b₁ 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 b₁ being Matrix of n,K st b₁ 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 b₁ being Matrix of n,K st b₁ = - M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 + M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = a * M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 - M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M @ holds
b₁ 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 b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ 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 b₁ being Matrix of n,K st b₁ 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 b₁ being Matrix of n,K st b₁ = - M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 + M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = a * M holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 - M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M @ holds
b₁ 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 b₁ being Matrix of n,K st b₁ is symmetric & b₁ is subsymmetric holds
b₁ 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 b₁ being Matrix of len p,K st b₁ is_symmetry_circulant_about p by A1;
uniqueness
for b₁, b₂ being Matrix of len p,K st b₁ is_symmetry_circulant_about p & b₂ is_symmetry_circulant_about p holds
b₁ = b₂

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 b₃ being Matrix of len p,K holds
( b₃ = SCirc p iff b₃ 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 b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ 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 b₁ being Matrix of n,K st b₁ 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 b₁ being Matrix of n,K st b₁ = a * M1 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 + M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = - M1 holds
b₁ 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 b₁ being Matrix of n,K st b₁ = M1 - M2 holds
b₁ 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 b₁ being Matrix of n,K st b₁ is symmetry_circulant holds
b₁ is symmetric by Th17;

end;