:: MATRIX_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let f be FinSequence;
attr f is tabular means :Def1: :: MATRIX_1:def 1
ex n being Nat st
for x being set st x in rng f holds
ex s being FinSequence st
( s = x & len s = n );
end;

:: deftheorem Def1 defines tabular MATRIX_1:def 1 :
for f being FinSequence holds
( f is tabular iff ex n being Nat st
for x being set st x in rng f holds
ex s being FinSequence st
( s = x & len s = n ) );

registration
cluster tabular set ;
existence
ex b1 being FinSequence st b1 is tabular
proof end;
end;

theorem Th1: :: MATRIX_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D holds <*<*d*>*> is tabular
proof end;

theorem Th2: :: MATRIX_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for m, n being Nat holds m |-> (n |-> x) is tabular
proof end;

theorem Th3: :: MATRIX_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being FinSequence holds <*s*> is tabular
proof end;

theorem Th4: :: MATRIX_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular
proof end;

theorem Th5: :: MATRIX_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is tabular
proof end;

theorem :: MATRIX_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<*{} ,{} *> is tabular
proof end;

theorem :: MATRIX_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is tabular
proof end;

theorem :: MATRIX_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is tabular
proof end;

registration
let D be set ;
cluster tabular FinSequence of D * ;
existence
ex b1 being FinSequence of D * st b1 is tabular
proof end;
end;

definition
let D be set ;
mode Matrix of D is tabular FinSequence of D * ;
end;

registration
let D be non empty set ;
cluster non empty-yielding FinSequence of D * ;
existence
not for b1 being Matrix of D holds b1 is empty-yielding
proof end;
end;

theorem Th9: :: MATRIX_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) )
proof end;

definition
let D be non empty set ;
let m, n be Nat;
canceled;
mode Matrix of m,n,D -> Matrix of D means :Def3: :: MATRIX_1:def 3
( len it = m & ( for p being FinSequence of D st p in rng it holds
len p = n ) );
existence
ex b1 being Matrix of D st
( len b1 = m & ( for p being FinSequence of D st p in rng b1 holds
len p = n ) )
proof end;
end;

:: deftheorem MATRIX_1:def 2 :
canceled;

:: deftheorem Def3 defines Matrix MATRIX_1:def 3 :
for D being non empty set
for m, n being Nat
for b4 being Matrix of D holds
( b4 is Matrix of m,n,D iff ( len b4 = m & ( for p being FinSequence of D st p in rng b4 holds
len p = n ) ) );

definition
let D be non empty set ;
let n be Nat;
mode Matrix of n,D is Matrix of n,n,D;
end;

definition
let K be non empty 1-sorted ;
mode Matrix of K is Matrix of the carrier of K;
let n be Nat;
mode Matrix of n,K is Matrix of n,n,the carrier of K;
let m be Nat;
mode Matrix of n,m,K is Matrix of n,m,the carrier of K;
end;

theorem Th10: :: MATRIX_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
proof end;

theorem Th11: :: MATRIX_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being FinSequence of D holds <*p*> is Matrix of 1, len p,D
proof end;

theorem Th12: :: MATRIX_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for p1, p2 being FinSequence of D st len p1 = n & len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
proof end;

theorem Th13: :: MATRIX_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for D being non empty set holds {} is Matrix of 0,m,D
proof end;

theorem :: MATRIX_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds <*{} *> is Matrix of 1,0,D
proof end;

theorem :: MATRIX_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a being Element of D holds <*<*a*>*> is Matrix of 1,D
proof end;

theorem :: MATRIX_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds <*{} ,{} *> is Matrix of 2,0,D
proof end;

theorem :: MATRIX_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D
proof end;

theorem :: MATRIX_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
proof end;

theorem :: MATRIX_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
proof end;

definition
let M be tabular FinSequence;
func width M -> Nat means :Def4: :: MATRIX_1:def 4
ex s being FinSequence st
( s in rng M & len s = it ) if len M > 0
otherwise it = 0;
existence
( ( len M > 0 implies ex b1 being Nat ex s being FinSequence st
( s in rng M & len s = b1 ) ) & ( not len M > 0 implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = b1 ) & ex s being FinSequence st
( s in rng M & len s = b2 ) implies b1 = b2 ) & ( not len M > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum
;
end;

:: deftheorem Def4 defines width MATRIX_1:def 4 :
for M being tabular FinSequence
for b2 being Nat holds
( ( len M > 0 implies ( b2 = width M iff ex s being FinSequence st
( s in rng M & len s = b2 ) ) ) & ( not len M > 0 implies ( b2 = width M iff b2 = 0 ) ) );

theorem Th20: :: MATRIX_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
proof end;

definition
let M be tabular FinSequence;
func Indices M -> set equals :: MATRIX_1:def 5
[:(dom M),(Seg (width M)):];
coherence
[:(dom M),(Seg (width M)):] is set
;
end;

:: deftheorem defines Indices MATRIX_1:def 5 :
for M being tabular FinSequence holds Indices M = [:(dom M),(Seg (width M)):];

definition
let D be set ;
let M be Matrix of D;
let i, j be Nat;
assume A1: [i,j] in Indices M ;
func M * i,j -> Element of D means :Def6: :: MATRIX_1:def 6
ex p being FinSequence of D st
( p = M . i & it = p . j );
existence
ex b1 being Element of D ex p being FinSequence of D st
( p = M . i & b1 = p . j )
proof end;
uniqueness
for b1, b2 being Element of D st ex p being FinSequence of D st
( p = M . i & b1 = p . j ) & ex p being FinSequence of D st
( p = M . i & b2 = p . j ) holds
b1 = b2
;
end;

:: deftheorem Def6 defines * MATRIX_1:def 6 :
for D being set
for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
for b5 being Element of D holds
( b5 = M * i,j iff ex p being FinSequence of D st
( p = M . i & b5 = p . j ) );

theorem Th21: :: MATRIX_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M1, M2 being Matrix of D st len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = M2 * i,j ) holds
M1 = M2
proof end;

scheme :: MATRIX_1:sch 1
MatrixLambda{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, F4( set , set ) -> Element of F1() } :
ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
M * i,j = F4(i,j)
proof end;

scheme :: MATRIX_1:sch 2
MatrixEx{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, P1[ set , set , set ] } :
ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
P1[i,j,M * i,j]
provided
for i, j being Nat st [i,j] in [:(Seg F2()),(Seg F3()):] holds
for x1, x2 being Element of F1() st P1[i,j,x1] & P1[i,j,x2] holds
x1 = x2 and
A1: for i, j being Nat st [i,j] in [:(Seg F2()),(Seg F3()):] holds
ex x being Element of F1() st P1[i,j,x]
proof end;

theorem :: MATRIX_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MATRIX_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for D being non empty set
for M being Matrix of 0,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
proof end;

theorem Th24: :: MATRIX_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set st n > 0 holds
for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
proof end;

theorem Th25: :: MATRIX_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
proof end;

theorem Th26: :: MATRIX_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds
( len M = n & Indices M = [:(Seg n),(Seg (width M)):] )
proof end;

theorem Th27: :: MATRIX_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D holds Indices M1 = Indices M2
proof end;

theorem Th28: :: MATRIX_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = M2 * i,j ) holds
M1 = M2
proof end;

theorem :: MATRIX_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for M1 being Matrix of n,D
for i, j being Nat st [i,j] in Indices M1 holds
[j,i] in Indices M1
proof end;

definition
let D be non empty set ;
let M be Matrix of D;
func M @ -> Matrix of D means :: MATRIX_1:def 7
( len it = width M & ( for i, j being Nat holds
( [i,j] in Indices it iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
it * i,j = M * j,i ) );
existence
ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * i,j = M * j,i ) )
proof end;
uniqueness
for b1, b2 being Matrix of D st len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * i,j = M * j,i ) & len b2 = width M & ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b2 * i,j = M * j,i ) holds
b1 = b2
proof end;
end;

:: deftheorem defines @ MATRIX_1:def 7 :
for D being non empty set
for M, b3 being Matrix of D holds
( b3 = M @ iff ( len b3 = width M & ( for i, j being Nat holds
( [i,j] in Indices b3 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b3 * i,j = M * j,i ) ) );

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
func Line M,i -> FinSequence of D means :Def8: :: MATRIX_1:def 8
( len it = width M & ( for j being Nat st j in Seg (width M) holds
it . j = M * i,j ) );
existence
ex b1 being FinSequence of D st
( len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = M * i,j ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = M * i,j ) & len b2 = width M & ( for j being Nat st j in Seg (width M) holds
b2 . j = M * i,j ) holds
b1 = b2
proof end;
func Col M,i -> FinSequence of D means :Def9: :: MATRIX_1:def 9
( len it = len M & ( for j being Nat st j in dom M holds
it . j = M * j,i ) );
existence
ex b1 being FinSequence of D st
( len b1 = len M & ( for j being Nat st j in dom M holds
b1 . j = M * j,i ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = len M & ( for j being Nat st j in dom M holds
b1 . j = M * j,i ) & len b2 = len M & ( for j being Nat st j in dom M holds
b2 . j = M * j,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Line MATRIX_1:def 8 :
for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Line M,i iff ( len b4 = width M & ( for j being Nat st j in Seg (width M) holds
b4 . j = M * i,j ) ) );

:: deftheorem Def9 defines Col MATRIX_1:def 9 :
for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Col M,i iff ( len b4 = len M & ( for j being Nat st j in dom M holds
b4 . j = M * j,i ) ) );

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
:: original: Line
redefine func Line M,i -> Element of (width M) -tuples_on D;
coherence
Line M,i is Element of (width M) -tuples_on D
proof end;
:: original: Col
redefine func Col M,i -> Element of (len M) -tuples_on D;
coherence
Col M,i is Element of (len M) -tuples_on D
proof end;
end;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
func n -Matrices_over K -> set equals :: MATRIX_1:def 10
n -tuples_on (n -tuples_on the carrier of K);
coherence
n -tuples_on (n -tuples_on the carrier of K) is set
;
func 0. K,n -> Matrix of n,K equals :: MATRIX_1:def 11
n |-> (n |-> (0. K));
coherence
n |-> (n |-> (0. K)) is Matrix of n,K
by Th10;
func 1. K,n -> Matrix of n,K means :Def12: :: MATRIX_1:def 12
( ( for i being Nat st [i,i] in Indices it holds
it * i,i = 1. K ) & ( for i, j being Nat st [i,j] in Indices it & i <> j holds
it * i,j = 0. K ) );
existence
ex b1 being Matrix of n,K st
( ( for i being Nat st [i,i] in Indices b1 holds
b1 * i,i = 1. K ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * i,j = 0. K ) )
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i being Nat st [i,i] in Indices b1 holds
b1 * i,i = 1. K ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * i,j = 0. K ) & ( for i being Nat st [i,i] in Indices b2 holds
b2 * i,i = 1. K ) & ( for i, j being Nat st [i,j] in Indices b2 & i <> j holds
b2 * i,j = 0. K ) holds
b1 = b2
proof end;
let A be Matrix of n,K;
func - A -> Matrix of n,K means :Def13: :: MATRIX_1:def 13
for i, j being Nat st [i,j] in Indices A holds
it * i,j = - (A * i,j);
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j)
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j) ) & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = - (A * i,j) ) holds
b1 = b2
proof end;
let B be Matrix of n,K;
func A + B -> Matrix of n,K means :Def14: :: MATRIX_1:def 14
for i, j being Nat st [i,j] in Indices A holds
it * i,j = (A * i,j) + (B * i,j);
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j)
proof end;
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j) ) & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = (A * i,j) + (B * i,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines -Matrices_over MATRIX_1:def 10 :
for K being non empty doubleLoopStr
for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

:: deftheorem defines 0. MATRIX_1:def 11 :
for K being non empty doubleLoopStr
for n being Nat holds 0. K,n = n |-> (n |-> (0. K));

:: deftheorem Def12 defines 1. MATRIX_1:def 12 :
for K being non empty doubleLoopStr
for n being Nat
for b3 being Matrix of n,K holds
( b3 = 1. K,n iff ( ( for i being Nat st [i,i] in Indices b3 holds
b3 * i,i = 1. K ) & ( for i, j being Nat st [i,j] in Indices b3 & i <> j holds
b3 * i,j = 0. K ) ) );

:: deftheorem Def13 defines - MATRIX_1:def 13 :
for K being non empty doubleLoopStr
for n being Nat
for A, b4 being Matrix of n,K holds
( b4 = - A iff for i, j being Nat st [i,j] in Indices A holds
b4 * i,j = - (A * i,j) );

:: deftheorem Def14 defines + MATRIX_1:def 14 :
for K being non empty doubleLoopStr
for n being Nat
for A, B, b5 being Matrix of n,K holds
( b5 = A + B iff for i, j being Nat st [i,j] in Indices A holds
b5 * i,j = (A * i,j) + (B * i,j) );

registration
let K be non empty doubleLoopStr ;
let n be Nat;
cluster n -Matrices_over K -> non empty ;
coherence
not n -Matrices_over K is empty
;
end;

theorem Th30: :: MATRIX_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat
for K being non empty doubleLoopStr st [i,j] in Indices (0. K,n) holds
(0. K,n) * i,j = 0. K
proof end;

theorem Th31: :: MATRIX_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
proof end;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
mode Diagonal of n,K -> Matrix of n,K means :: MATRIX_1:def 15
for i, j being Nat st [i,j] in Indices it & it * i,j <> 0. K holds
i = j;
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices b1 & b1 * i,j <> 0. K holds
i = j
proof end;
end;

:: deftheorem defines Diagonal MATRIX_1:def 15 :
for K being non empty doubleLoopStr
for n being Nat
for b3 being Matrix of n,K holds
( b3 is Diagonal of n,K iff for i, j being Nat st [i,j] in Indices b3 & b3 * i,j <> 0. K holds
i = j );

theorem Th32: :: MATRIX_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for F being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for A, B being Matrix of n,F holds A + B = B + A
proof end;

theorem Th33: :: MATRIX_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for F being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
proof end;

theorem Th34: :: MATRIX_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for F being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for A being Matrix of n,F holds A + (0. F,n) = A
proof end;

theorem Th35: :: MATRIX_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for F being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for A being Matrix of n,F holds A + (- A) = 0. F,n
proof end;

definition
let F be non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr ;
let n be Nat;
func n -G_Matrix_over F -> strict AbGroup means :: MATRIX_1:def 16
( the carrier of it = n -Matrices_over F & ( for A, B being Matrix of n,F holds the add of it . A,B = A + B ) & the Zero of it = 0. F,n );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the add of b1 . A,B = A + B ) & the Zero of b1 = 0. F,n )
proof end;
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the add of b1 . A,B = A + B ) & the Zero of b1 = 0. F,n & the carrier of b2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the add of b2 . A,B = A + B ) & the Zero of b2 = 0. F,n holds
b1 = b2
proof end;
end;

:: deftheorem defines -G_Matrix_over MATRIX_1:def 16 :
for F being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for n being Nat
for b3 being strict AbGroup holds
( b3 = n -G_Matrix_over F iff ( the carrier of b3 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the add of b3 . A,B = A + B ) & the Zero of b3 = 0. F,n ) );