:: MATRIX_2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem defines --> MATRIX_2:def 1 :
theorem Th1: :: MATRIX_2:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
definition
let a,
b,
c,
d be
set ;
func a,
b ][ c,
d -> tabular FinSequence equals :: MATRIX_2:def 2
<*<*a,b*>,<*c,d*>*>;
correctness
coherence
<*<*a,b*>,<*c,d*>*> is tabular FinSequence;
end;
:: deftheorem defines ][ MATRIX_2:def 2 :
theorem Th3: :: MATRIX_2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
for
x1,
x2,
y1,
y2 being
set holds
(
len (x1,x2 ][ y1,y2) = 2 &
width (x1,x2 ][ y1,y2) = 2 &
Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] )
theorem Th4: :: MATRIX_2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
for
x1,
x2,
y1,
y2 being
set holds
(
[1,1] in Indices (x1,x2 ][ y1,y2) &
[1,2] in Indices (x1,x2 ][ y1,y2) &
[2,1] in Indices (x1,x2 ][ y1,y2) &
[2,2] in Indices (x1,x2 ][ y1,y2) )
theorem :: MATRIX_2:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
for
D being non
empty set for
a,
b,
c,
d being
Element of
D holds
(
(a,b ][ c,d) * 1,1
= a &
(a,b ][ c,d) * 1,2
= b &
(a,b ][ c,d) * 2,1
= c &
(a,b ][ c,d) * 2,2
= d )
:: deftheorem defines Upper_Triangular_Matrix MATRIX_2:def 3 :
:: deftheorem defines Lower_Triangular_Matrix MATRIX_2:def 4 :
theorem :: MATRIX_2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem :: MATRIX_2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th10: :: MATRIX_2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
definition
let i be
Nat;
let K be
Field;
let M be
Matrix of
K;
canceled;assume A1:
i in Seg (width M)
;
func DelCol M,
i -> Matrix of
K means :: MATRIX_2:def 6
(
len it = len M & ( for
k being
Nat st
k in dom M holds
it . k = Del (Line M,k),
i ) );
existence
ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del (Line M,k),i ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del (Line M,k),i ) & len b2 = len M & ( for k being Nat st k in dom M holds
b2 . k = Del (Line M,k),i ) holds
b1 = b2
end;
:: deftheorem MATRIX_2:def 5 :
canceled;
:: deftheorem defines DelCol MATRIX_2:def 6 :
theorem Th11: :: MATRIX_2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th12: :: MATRIX_2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th14: :: MATRIX_2:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th15: :: MATRIX_2:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th16: :: MATRIX_2:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th17: :: MATRIX_2:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th18: :: MATRIX_2:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
definition
let i be
Nat;
let K be
Field;
let M be
Matrix of
K;
assume A1:
(
i in dom M &
width M > 0 )
;
func DelLine M,
i -> Matrix of
K means :: MATRIX_2:def 7
it = {} if len M = 1
otherwise (
width it = width M & ( for
k being
Nat st
k in Seg (width M) holds
Col it,
k = Del (Col M,k),
i ) );
existence
( ( len M = 1 implies ex b1 being Matrix of K st b1 = {} ) & ( not len M = 1 implies ex b1 being Matrix of K st
( width b1 = width M & ( for k being Nat st k in Seg (width M) holds
Col b1,k = Del (Col M,k),i ) ) ) )
uniqueness
for b1, b2 being Matrix of K holds
( ( len M = 1 & b1 = {} & b2 = {} implies b1 = b2 ) & ( not len M = 1 & width b1 = width M & ( for k being Nat st k in Seg (width M) holds
Col b1,k = Del (Col M,k),i ) & width b2 = width M & ( for k being Nat st k in Seg (width M) holds
Col b2,k = Del (Col M,k),i ) implies b1 = b2 ) )
consistency
for b1 being Matrix of K holds verum
;
end;
:: deftheorem defines DelLine MATRIX_2:def 7 :
:: deftheorem defines Deleting MATRIX_2:def 8 :
:: deftheorem Def9 defines permutational MATRIX_2:def 9 :
:: deftheorem Def10 defines len MATRIX_2:def 10 :
theorem :: MATRIX_2:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :
theorem :: MATRIX_2:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem Def12 defines len MATRIX_2:def 12 :
theorem :: MATRIX_2:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :
theorem Th23: :: MATRIX_2:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th24: :: MATRIX_2:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th25: :: MATRIX_2:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th26: :: MATRIX_2:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: MATRIX_2:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
canceled;
theorem Th28: :: MATRIX_2:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem defines being_transposition MATRIX_2:def 14 :
:: deftheorem Def15 defines even MATRIX_2:def 15 :
theorem :: MATRIX_2:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem defines - MATRIX_2:def 16 :
:: deftheorem defines FinOmega MATRIX_2:def 17 :
theorem :: MATRIX_2:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)