:: MATRIX_2 semantic presentation begin definition let n, m be Nat; let a be set ; func(n,m) --> a -> tabular FinSequence equals :: MATRIX_2:def 1 n |-> (m |-> a); coherence n |-> (m |-> a) is tabular FinSequence by MATRIX_1:2; end; :: deftheorem defines --> MATRIX_2:def_1_:_ for n, m being Nat for a being set holds (n,m) --> a = n |-> (m |-> a); definition let D be non empty set ; let n, m be Nat; let d be Element of D; :: original: --> redefine func(n,m) --> d -> Matrix of n,m,D; coherence (n,m) --> d is Matrix of n,m,D by MATRIX_1:10; end; theorem Th1: :: MATRIX_2:1 for i, j, n, m being Nat for D being non empty set for a being Element of D st [i,j] in Indices ((n,m) --> a) holds ((n,m) --> a) * (i,j) = a proof let i, j, n, m be Nat; ::_thesis: for D being non empty set for a being Element of D st [i,j] in Indices ((n,m) --> a) holds ((n,m) --> a) * (i,j) = a let D be non empty set ; ::_thesis: for a being Element of D st [i,j] in Indices ((n,m) --> a) holds ((n,m) --> a) * (i,j) = a let a be Element of D; ::_thesis: ( [i,j] in Indices ((n,m) --> a) implies ((n,m) --> a) * (i,j) = a ) reconsider m1 = m as Element of NAT by ORDINAL1:def_12; set M = (n,m) --> a; assume A1: [i,j] in Indices ((n,m) --> a) ; ::_thesis: ((n,m) --> a) * (i,j) = a then i in dom ((n,m) --> a) by ZFMISC_1:87; then i in Seg (len ((n,m) --> a)) by FINSEQ_1:def_3; then A2: i in Seg n by MATRIX_1:def_2; then A3: n > 0 ; j in Seg (width ((n,m) --> a)) by A1, ZFMISC_1:87; then j in Seg m by A3, MATRIX_1:23; then A4: (m1 |-> a) . j = a by FUNCOP_1:7; ((n,m) --> a) . i = m1 |-> a by A2, FUNCOP_1:7; hence ((n,m) --> a) * (i,j) = a by A1, A4, MATRIX_1:def_5; ::_thesis: verum end; theorem :: MATRIX_2:2 for n being Nat for K being Field for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) proof let n be Nat; ::_thesis: for K being Field for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) let K be Field; ::_thesis: for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) let a9, b9 be Element of K; ::_thesis: ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) A1: Indices ((n,n) --> a9) = Indices ((n,n) --> (a9 + b9)) by MATRIX_1:26; A2: Indices ((n,n) --> a9) = Indices ((n,n) --> b9) by MATRIX_1:26; now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((n,n)_-->_(a9_+_b9))_holds_ (((n,n)_-->_a9)_*_(i,j))_+_(((n,n)_-->_b9)_*_(i,j))_=_((n,n)_-->_(a9_+_b9))_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> (a9 + b9)) implies (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) ) assume A3: [i,j] in Indices ((n,n) --> (a9 + b9)) ; ::_thesis: (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) then ((n,n) --> a9) * (i,j) = a9 by A1, Th1; then (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = a9 + b9 by A2, A1, A3, Th1; hence (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) by A3, Th1; ::_thesis: verum end; hence ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) by A1, MATRIX_1:def_13; ::_thesis: verum end; 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; proof ( len <*a,b*> = 2 & len <*c,d*> = 2 ) by FINSEQ_1:44; hence <*<*a,b*>,<*c,d*>*> is tabular FinSequence by MATRIX_1:4; ::_thesis: verum end; end; :: deftheorem defines ][ MATRIX_2:def_2_:_ for a, b, c, d being set holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>; theorem Th3: :: MATRIX_2:3 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):] ) proof let x1, x2, y1, y2 be set ; ::_thesis: ( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] ) set M = (x1,x2) ][ (y1,y2); thus A1: len ((x1,x2) ][ (y1,y2)) = 2 by FINSEQ_1:44; ::_thesis: ( width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] ) rng ((x1,x2) ][ (y1,y2)) = {<*x1,x2*>,<*y1,y2*>} by FINSEQ_2:127; then A2: <*x1,x2*> in rng ((x1,x2) ][ (y1,y2)) by TARSKI:def_2; len <*x1,x2*> = 2 by FINSEQ_1:44; hence width ((x1,x2) ][ (y1,y2)) = 2 by A1, A2, MATRIX_1:def_3; ::_thesis: Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] hence Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] by A1, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th4: :: MATRIX_2:4 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)) ) proof let x1, x2, y1, y2 be set ; ::_thesis: ( [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)) ) A1: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; ( Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] & 1 in Seg 2 ) by Th3, FINSEQ_1:2, TARSKI:def_2; hence ( [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)) ) by A1, ZFMISC_1:87; ::_thesis: verum end; definition let D be non empty set ; let a be Element of D; :: original: <* redefine func<*a*> -> Element of 1 -tuples_on D; coherence <*a*> is Element of 1 -tuples_on D by FINSEQ_2:98; end; definition let D be non empty set ; let n be Nat; let p be Element of n -tuples_on D; :: original: <* redefine func<*p*> -> Matrix of 1,n,D; coherence <*p*> is Matrix of 1,n,D proof len p = n by CARD_1:def_7; hence <*p*> is Matrix of 1,n,D by MATRIX_1:11; ::_thesis: verum end; end; theorem :: MATRIX_2:5 for D being non empty set for a being Element of D holds ( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a ) proof let D be non empty set ; ::_thesis: for a being Element of D holds ( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a ) let a be Element of D; ::_thesis: ( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a ) set M = <*<*a*>*>; ( Indices <*<*a*>*> = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:2, MATRIX_1:24, TARSKI:def_1; hence A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:87; ::_thesis: <*<*a*>*> * (1,1) = a ( <*<*a*>*> . 1 = <*a*> & <*a*> . 1 = a ) by FINSEQ_1:40; hence <*<*a*>*> * (1,1) = a by A1, MATRIX_1:def_5; ::_thesis: verum end; definition let D be non empty set ; let a, b, c, d be Element of D; :: original: ][ redefine func(a,b) ][ (c,d) -> Matrix of 2,D; coherence (a,b) ][ (c,d) is Matrix of 2,D by MATRIX_1:19; end; theorem :: MATRIX_2:6 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 ) proof let D be non empty set ; ::_thesis: 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 ) let a, b, c, d be Element of D; ::_thesis: ( ((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 ) set M = (a,b) ][ (c,d); A1: ( ((a,b) ][ (c,d)) . 1 = <*a,b*> & ((a,b) ][ (c,d)) . 2 = <*c,d*> ) by FINSEQ_1:44; A2: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:44; A3: ( [2,1] in Indices ((a,b) ][ (c,d)) & [2,2] in Indices ((a,b) ][ (c,d)) ) by Th4; A4: ( <*c,d*> . 1 = c & <*c,d*> . 2 = d ) by FINSEQ_1:44; ( [1,1] in Indices ((a,b) ][ (c,d)) & [1,2] in Indices ((a,b) ][ (c,d)) ) by Th4; hence ( ((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 ) by A1, A2, A4, A3, MATRIX_1:def_5; ::_thesis: verum end; definition let n be Nat; let K be Field; let M be Matrix of n,K; attrM is upper_triangular means :Def3: :: MATRIX_2:def 3 for i, j being Nat st [i,j] in Indices M & i > j holds M * (i,j) = 0. K; attrM is lower_triangular means :: MATRIX_2:def 4 for i, j being Nat st [i,j] in Indices M & i < j holds M * (i,j) = 0. K; end; :: deftheorem Def3 defines upper_triangular MATRIX_2:def_3_:_ for n being Nat for K being Field for M being Matrix of n,K holds ( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds M * (i,j) = 0. K ); :: deftheorem defines lower_triangular MATRIX_2:def_4_:_ for n being Nat for K being Field for M being Matrix of n,K holds ( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds M * (i,j) = 0. K ); registration let n be Nat; let K be Field; cluster diagonal -> upper_triangular lower_triangular for Matrix of n,n, the carrier of K; coherence for b1 being Diagonal of n,K holds ( b1 is upper_triangular & b1 is lower_triangular ) proof let M be Diagonal of n,K; ::_thesis: ( M is upper_triangular & M is lower_triangular ) for i, j being Nat st [i,j] in Indices M & i > j holds M * (i,j) = 0. K by MATRIX_1:def_14; hence M is upper_triangular by Def3; ::_thesis: M is lower_triangular thus for i, j being Nat st [i,j] in Indices M & i < j holds M * (i,j) = 0. K by MATRIX_1:def_14; :: according to MATRIX_2:def_4 ::_thesis: verum end; end; registration let n be Nat; let K be Field; cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular upper_triangular lower_triangular for Matrix of n,n, the carrier of K; existence ex b1 being Matrix of n,K st ( b1 is lower_triangular & b1 is upper_triangular ) proof set M = the Diagonal of n,K; take the Diagonal of n,K ; ::_thesis: ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular ) thus ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular ) ; ::_thesis: verum end; end; definition let n be Nat; let K be Field; mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K; mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K; end; theorem :: MATRIX_2:7 for n being Nat for D being non empty set for M being Matrix of D st len M = n holds M is Matrix of n, width M,D proof let n be Nat; ::_thesis: for D being non empty set for M being Matrix of D st len M = n holds M is Matrix of n, width M,D let D be non empty set ; ::_thesis: for M being Matrix of D st len M = n holds M is Matrix of n, width M,D let M be Matrix of D; ::_thesis: ( len M = n implies M is Matrix of n, width M,D ) assume that A1: len M = n and A2: M is not Matrix of n, width M,D ; ::_thesis: contradiction set m = width M; percases ( len M <> n or ex p being FinSequence of D st ( p in rng M & not len p = width M ) ) by A2, MATRIX_1:def_2; suppose len M <> n ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; supposeA3: ex p being FinSequence of D st ( p in rng M & not len p = width M ) ; ::_thesis: contradiction consider k being Nat such that A4: for x being set st x in rng M holds ex q being FinSequence of D st ( x = q & len q = k ) by MATRIX_1:9; consider p being FinSequence of D such that A5: p in rng M and A6: len p <> width M by A3; reconsider x = p as set ; A7: ex q being FinSequence of D st ( x = q & len q = k ) by A5, A4; now__::_thesis:_len_p_=_width_M percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: len p = width M then M = {} by A1; hence len p = width M by A5, RELAT_1:38; ::_thesis: verum end; suppose n > 0 ; ::_thesis: len p = width M then consider s being FinSequence such that A8: s in rng M and A9: len s = width M by A1, MATRIX_1:def_3; reconsider y = s as set ; ex r being FinSequence of D st ( y = r & len r = k ) by A4, A8; hence len p = width M by A7, A9; ::_thesis: verum end; end; end; hence contradiction by A6; ::_thesis: verum end; end; end; begin theorem Th8: :: MATRIX_2:8 for n, m being Nat for D being non empty set for M being Matrix of n,m,D for k being Nat st k in Seg n holds M . k = Line (M,k) proof let n, m be Nat; ::_thesis: for D being non empty set for M being Matrix of n,m,D for k being Nat st k in Seg n holds M . k = Line (M,k) let D be non empty set ; ::_thesis: for M being Matrix of n,m,D for k being Nat st k in Seg n holds M . k = Line (M,k) let M be Matrix of n,m,D; ::_thesis: for k being Nat st k in Seg n holds M . k = Line (M,k) let k be Nat; ::_thesis: ( k in Seg n implies M . k = Line (M,k) ) assume A1: k in Seg n ; ::_thesis: M . k = Line (M,k) ( len M = n & dom M = Seg (len M) ) by FINSEQ_1:def_3, MATRIX_1:25; then A2: M . k in rng M by A1, FUNCT_1:def_3; percases ( n = 0 or 0 < n ) ; suppose n = 0 ; ::_thesis: M . k = Line (M,k) hence M . k = Line (M,k) by A1; ::_thesis: verum end; supposeA3: 0 < n ; ::_thesis: M . k = Line (M,k) consider l being Nat such that A4: for x being set st x in rng M holds ex p being FinSequence of D st ( x = p & len p = l ) by MATRIX_1:9; consider p being FinSequence of D such that A5: M . k = p and len p = l by A2, A4; A6: width M = m by A3, MATRIX_1:23; A7: for j being Nat st j in Seg (width M) holds p . j = M * (k,j) proof let j be Nat; ::_thesis: ( j in Seg (width M) implies p . j = M * (k,j) ) assume j in Seg (width M) ; ::_thesis: p . j = M * (k,j) then [k,j] in [:(Seg n),(Seg m):] by A1, A6, ZFMISC_1:87; then [k,j] in Indices M by A3, MATRIX_1:23; then ex q being FinSequence of D st ( q = M . k & M * (k,j) = q . j ) by MATRIX_1:def_5; hence p . j = M * (k,j) by A5; ::_thesis: verum end; len p = width M by A2, A6, A5, MATRIX_1:def_2; hence M . k = Line (M,k) by A5, A7, MATRIX_1:def_7; ::_thesis: verum end; end; end; Lm1: for K being Field for M being Matrix of K for k being Nat st k in dom M holds M . k = Line (M,k) proof let K be Field; ::_thesis: for M being Matrix of K for k being Nat st k in dom M holds M . k = Line (M,k) let M be Matrix of K; ::_thesis: for k being Nat st k in dom M holds M . k = Line (M,k) let k be Nat; ::_thesis: ( k in dom M implies M . k = Line (M,k) ) assume A1: k in dom M ; ::_thesis: M . k = Line (M,k) then ( 1 <= k & k <= len M ) by FINSEQ_3:25; then reconsider N = M as Matrix of len M, width M,K by MATRIX_1:20; k in Seg (len N) by A1, FINSEQ_1:def_3; hence M . k = Line (M,k) by Th8; ::_thesis: verum end; definition let i be Nat; let K be Field; let M be Matrix of K; func DelCol (M,i) -> Matrix of K means :: MATRIX_2:def 5 ( 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) ) ) proof percases ( not i in Seg (width M) or i in Seg (width M) ) ; supposeA1: not i in Seg (width M) ; ::_thesis: 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) ) ) take M ; ::_thesis: ( len M = len M & ( for k being Nat st k in dom M holds M . k = Del ((Line (M,k)),i) ) ) thus len M = len M ; ::_thesis: for k being Nat st k in dom M holds M . k = Del ((Line (M,k)),i) let k be Nat; ::_thesis: ( k in dom M implies M . k = Del ((Line (M,k)),i) ) assume A2: k in dom M ; ::_thesis: M . k = Del ((Line (M,k)),i) len (Line (M,k)) = width M by MATRIX_1:def_7; then A3: not i in dom (Line (M,k)) by A1, FINSEQ_1:def_3; thus M . k = Line (M,k) by A2, Lm1 .= Del ((Line (M,k)),i) by A3, FINSEQ_3:104 ; ::_thesis: verum end; supposeA4: i in Seg (width M) ; ::_thesis: 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) ) ) defpred S1[ Nat, Nat, Element of K] means \$3 = (Del ((Line (M,\$1)),i)) . \$2; percases ( len M = 0 or len M > 0 ) ; supposeA5: len M = 0 ; ::_thesis: 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) ) ) then Seg (len M) = {} ; hence 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) ) ) by A4, A5, MATRIX_1:def_3; ::_thesis: verum end; supposeA6: len M > 0 ; ::_thesis: 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) ) ) set n1 = width M; percases ( width M = 0 or width M > 0 ) ; suppose width M = 0 ; ::_thesis: 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) ) ) hence 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) ) ) by A4; ::_thesis: verum end; suppose width M > 0 ; ::_thesis: 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) ) ) then consider m being Nat such that A7: width M = m + 1 by NAT_1:6; reconsider m = m as Element of NAT by ORDINAL1:def_12; A8: for k being Nat st k in dom M holds len (Del ((Line (M,k)),i)) = m proof let k be Nat; ::_thesis: ( k in dom M implies len (Del ((Line (M,k)),i)) = m ) assume k in dom M ; ::_thesis: len (Del ((Line (M,k)),i)) = m A9: len (Line (M,k)) = width M by MATRIX_1:def_7; then i in dom (Line (M,k)) by A4, FINSEQ_1:def_3; then ex l being Nat st ( len (Line (M,k)) = l + 1 & len (Del ((Line (M,k)),i)) = l ) by FINSEQ_3:104; hence len (Del ((Line (M,k)),i)) = m by A7, A9; ::_thesis: verum end; A10: for k, l being Nat st [k,l] in [:(Seg (len M)),(Seg m):] holds ex x being Element of K st S1[k,l,x] proof let k, l be Nat; ::_thesis: ( [k,l] in [:(Seg (len M)),(Seg m):] implies ex x being Element of K st S1[k,l,x] ) assume A11: [k,l] in [:(Seg (len M)),(Seg m):] ; ::_thesis: ex x being Element of K st S1[k,l,x] reconsider p = Del ((Line (M,k)),i) as FinSequence of K by FINSEQ_3:105; dom M = Seg (len M) by FINSEQ_1:def_3; then k in dom M by A11, ZFMISC_1:87; then A12: len p = m by A8; A13: dom p = Seg (len p) by FINSEQ_1:def_3; l in Seg m by A11, ZFMISC_1:87; then reconsider x = p . l as Element of the carrier of K by A12, A13, FINSEQ_2:11; take x ; ::_thesis: S1[k,l,x] thus S1[k,l,x] ; ::_thesis: verum end; consider N being Matrix of len M,m,K such that A14: for k, l being Nat st [k,l] in Indices N holds S1[k,l,N * (k,l)] from MATRIX_1:sch_2(A10); dom M = Seg (len M) by FINSEQ_1:def_3; then A15: Indices N = [:(dom M),(Seg m):] by A6, MATRIX_1:23; A16: for k, l being Nat st k in dom M & l in Seg m holds N * (k,l) = (Del ((Line (M,k)),i)) . l proof let k, l be Nat; ::_thesis: ( k in dom M & l in Seg m implies N * (k,l) = (Del ((Line (M,k)),i)) . l ) assume ( k in dom M & l in Seg m ) ; ::_thesis: N * (k,l) = (Del ((Line (M,k)),i)) . l then [k,l] in Indices N by A15, ZFMISC_1:87; hence N * (k,l) = (Del ((Line (M,k)),i)) . l by A14; ::_thesis: verum end; A17: width N = m by A6, MATRIX_1:23; reconsider N = N as Matrix of K ; take N ; ::_thesis: ( len N = len M & ( for k being Nat st k in dom M holds N . k = Del ((Line (M,k)),i) ) ) for k being Nat st k in dom M holds N . k = Del ((Line (M,k)),i) proof let k be Nat; ::_thesis: ( k in dom M implies N . k = Del ((Line (M,k)),i) ) assume A18: k in dom M ; ::_thesis: N . k = Del ((Line (M,k)),i) then k in Seg (len M) by FINSEQ_1:def_3; then A19: N . k = Line (N,k) by Th8; reconsider s = N . k as FinSequence ; A20: len s = m by A17, A19, MATRIX_1:def_7; then A21: dom s = Seg m by FINSEQ_1:def_3; A22: now__::_thesis:_for_j_being_Nat_st_j_in_dom_s_holds_ s_._j_=_(Del_((Line_(M,k)),i))_._j let j be Nat; ::_thesis: ( j in dom s implies s . j = (Del ((Line (M,k)),i)) . j ) assume A23: j in dom s ; ::_thesis: s . j = (Del ((Line (M,k)),i)) . j then (Line (N,k)) . j = N * (k,j) by A17, A21, MATRIX_1:def_7; hence s . j = (Del ((Line (M,k)),i)) . j by A16, A18, A19, A21, A23; ::_thesis: verum end; len (Del ((Line (M,k)),i)) = m by A8, A18; hence N . k = Del ((Line (M,k)),i) by A20, A22, FINSEQ_2:9; ::_thesis: verum end; hence ( len N = len M & ( for k being Nat st k in dom M holds N . k = Del ((Line (M,k)),i) ) ) by A6, MATRIX_1:23; ::_thesis: verum end; end; end; end; end; end; end; 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 proof let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M & ( for k being Nat st k in dom M holds M1 . k = Del ((Line (M,k)),i) ) & len M2 = len M & ( for k being Nat st k in dom M holds M2 . k = Del ((Line (M,k)),i) ) implies M1 = M2 ) assume that A24: len M1 = len M and A25: for k being Nat st k in dom M holds M1 . k = Del ((Line (M,k)),i) and A26: len M2 = len M and A27: for k being Nat st k in dom M holds M2 . k = Del ((Line (M,k)),i) ; ::_thesis: M1 = M2 A28: dom M1 = dom M by A24, FINSEQ_3:29; now__::_thesis:_for_k_being_Nat_st_k_in_dom_M1_holds_ M1_._k_=_M2_._k let k be Nat; ::_thesis: ( k in dom M1 implies M1 . k = M2 . k ) assume A29: k in dom M1 ; ::_thesis: M1 . k = M2 . k hence M1 . k = Del ((Line (M,k)),i) by A25, A28 .= M2 . k by A27, A28, A29 ; ::_thesis: verum end; hence M1 = M2 by A24, A26, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem defines DelCol MATRIX_2:def_5_:_ for i being Nat for K being Field for M, b4 being Matrix of K holds ( b4 = DelCol (M,i) iff ( len b4 = len M & ( for k being Nat st k in dom M holds b4 . k = Del ((Line (M,k)),i) ) ) ); theorem Th9: :: MATRIX_2:9 for D being non empty set for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds M1 = M2 proof let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds M1 = M2 let M1, M2 be Matrix of D; ::_thesis: ( M1 @ = M2 @ & len M1 = len M2 implies M1 = M2 ) assume that A1: M1 @ = M2 @ and A2: len M1 = len M2 ; ::_thesis: M1 = M2 len (M1 @) = width M1 by MATRIX_1:def_6; then A3: width M1 = width M2 by A1, MATRIX_1:def_6; A4: Indices M2 = [:(dom M2),(Seg (width M2)):] ; for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) dom M1 = Seg (len M2) by A2, FINSEQ_1:def_3 .= dom M2 by FINSEQ_1:def_3 ; then (M2 @) * (j,i) = M2 * (i,j) by A3, A4, A5, MATRIX_1:def_6; hence M1 * (i,j) = M2 * (i,j) by A1, A5, MATRIX_1:def_6; ::_thesis: verum end; hence M1 = M2 by A2, A3, MATRIX_1:21; ::_thesis: verum end; theorem Th10: :: MATRIX_2:10 for D being non empty set for M being Matrix of D st width M > 0 holds ( len (M @) = width M & width (M @) = len M ) proof let D be non empty set ; ::_thesis: for M being Matrix of D st width M > 0 holds ( len (M @) = width M & width (M @) = len M ) let M be Matrix of D; ::_thesis: ( width M > 0 implies ( len (M @) = width M & width (M @) = len M ) ) assume A1: width M > 0 ; ::_thesis: ( len (M @) = width M & width (M @) = len M ) thus len (M @) = width M by MATRIX_1:def_6; ::_thesis: width (M @) = len M percases ( len M = 0 or len M > 0 ) ; suppose len M = 0 ; ::_thesis: width (M @) = len M hence width (M @) = len M by A1, MATRIX_1:def_3; ::_thesis: verum end; supposeA2: len M > 0 ; ::_thesis: width (M @) = len M for i, j being set holds ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] ) proof let i, j be set ; ::_thesis: ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] ) thus ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] implies [i,j] in [:(Seg (width M)),(dom M):] ) ::_thesis: ( [i,j] in [:(Seg (width M)),(dom M):] implies [i,j] in [:(dom (M @)),(Seg (width (M @))):] ) proof assume A3: [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; ::_thesis: [i,j] in [:(Seg (width M)),(dom M):] then ( i in dom (M @) & j in Seg (width (M @)) ) by ZFMISC_1:87; then reconsider i = i, j = j as Nat ; [i,j] in Indices (M @) by A3; then [j,i] in Indices M by MATRIX_1:def_6; hence [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:88; ::_thesis: verum end; assume A4: [i,j] in [:(Seg (width M)),(dom M):] ; ::_thesis: [i,j] in [:(dom (M @)),(Seg (width (M @))):] then ( i in Seg (width M) & j in dom M ) by ZFMISC_1:87; then reconsider i = i, j = j as Nat ; [j,i] in Indices M by A4, ZFMISC_1:88; then [i,j] in Indices (M @) by MATRIX_1:def_6; hence [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; ::_thesis: verum end; then ( dom M = Seg (len M) & [:(Seg (width M)),(dom M):] = [:(dom (M @)),(Seg (width (M @))):] ) by FINSEQ_1:def_3, ZFMISC_1:89; then dom M = Seg (width (M @)) by A1, A2, ZFMISC_1:110; hence width (M @) = len M by FINSEQ_1:def_3; ::_thesis: verum end; end; end; theorem :: MATRIX_2:11 for D being non empty set for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds M1 = M2 proof let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds M1 = M2 let M1, M2 be Matrix of D; ::_thesis: ( width M1 > 0 & width M2 > 0 & M1 @ = M2 @ implies M1 = M2 ) assume ( width M1 > 0 & width M2 > 0 ) ; ::_thesis: ( not M1 @ = M2 @ or M1 = M2 ) then A1: ( width (M1 @) = len M1 & width (M2 @) = len M2 ) by Th10; assume M1 @ = M2 @ ; ::_thesis: M1 = M2 hence M1 = M2 by A1, Th9; ::_thesis: verum end; theorem :: MATRIX_2:12 for D being non empty set for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) ) proof let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) ) let M1, M2 be Matrix of D; ::_thesis: ( width M1 > 0 & width M2 > 0 implies ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) ) ) assume that A1: width M1 > 0 and A2: width M2 > 0 ; ::_thesis: ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) ) thus ( M1 = M2 implies ( M1 @ = M2 @ & width M1 = width M2 ) ) ; ::_thesis: ( M1 @ = M2 @ & width M1 = width M2 implies M1 = M2 ) assume that A3: M1 @ = M2 @ and A4: width M1 = width M2 ; ::_thesis: M1 = M2 len M1 = width (M1 @) by A1, Th10; then A5: len M1 = len M2 by A2, A3, Th10; A6: Indices M2 = [:(dom M2),(Seg (width M2)):] ; for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume A7: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) dom M1 = Seg (len M2) by A5, FINSEQ_1:def_3 .= dom M2 by FINSEQ_1:def_3 ; then (M2 @) * (j,i) = M2 * (i,j) by A4, A6, A7, MATRIX_1:def_6; hence M1 * (i,j) = M2 * (i,j) by A3, A7, MATRIX_1:def_6; ::_thesis: verum end; hence M1 = M2 by A4, A5, MATRIX_1:21; ::_thesis: verum end; theorem Th13: :: MATRIX_2:13 for D being non empty set for M being Matrix of D st len M > 0 & width M > 0 holds (M @) @ = M proof let D be non empty set ; ::_thesis: for M being Matrix of D st len M > 0 & width M > 0 holds (M @) @ = M let M be Matrix of D; ::_thesis: ( len M > 0 & width M > 0 implies (M @) @ = M ) assume that A1: len M > 0 and A2: width M > 0 ; ::_thesis: (M @) @ = M set N = M @ ; A3: width (M @) = len M by A2, Th10; A4: len ((M @) @) = width (M @) by MATRIX_1:def_6; A5: len (M @) = width M by MATRIX_1:def_6; ( dom M = Seg (len M) & dom ((M @) @) = Seg (len ((M @) @)) ) by FINSEQ_1:def_3; then A6: Indices ((M @) @) = Indices M by A1, A5, A3, A4, Th10; A7: for i, j being Nat st [i,j] in Indices ((M @) @) holds ((M @) @) * (i,j) = M * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M @) @) implies ((M @) @) * (i,j) = M * (i,j) ) assume A8: [i,j] in Indices ((M @) @) ; ::_thesis: ((M @) @) * (i,j) = M * (i,j) then [j,i] in Indices (M @) by MATRIX_1:def_6; then ((M @) @) * (i,j) = (M @) * (j,i) by MATRIX_1:def_6; hence ((M @) @) * (i,j) = M * (i,j) by A6, A8, MATRIX_1:def_6; ::_thesis: verum end; width (M @) > 0 by A1, A2, Th10; then width ((M @) @) = width M by A5, Th10; hence (M @) @ = M by A3, A4, A7, MATRIX_1:21; ::_thesis: verum end; theorem Th14: :: MATRIX_2:14 for D being non empty set for M being Matrix of D for i being Nat st i in dom M holds Line (M,i) = Col ((M @),i) proof let D be non empty set ; ::_thesis: for M being Matrix of D for i being Nat st i in dom M holds Line (M,i) = Col ((M @),i) let M be Matrix of D; ::_thesis: for i being Nat st i in dom M holds Line (M,i) = Col ((M @),i) let i be Nat; ::_thesis: ( i in dom M implies Line (M,i) = Col ((M @),i) ) A1: len (M @) = width M by MATRIX_1:def_6; len (Col ((M @),i)) = len (M @) by MATRIX_1:def_8; then A2: len (Col ((M @),i)) = width M by MATRIX_1:def_6; then A3: dom (Col ((M @),i)) = Seg (width M) by FINSEQ_1:def_3; assume A4: i in dom M ; ::_thesis: Line (M,i) = Col ((M @),i) A5: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Col_((M_@),i))_holds_ (Line_(M,i))_._j_=_(Col_((M_@),i))_._j let j be Nat; ::_thesis: ( j in dom (Col ((M @),i)) implies (Line (M,i)) . j = (Col ((M @),i)) . j ) A6: dom (M @) = Seg (len (M @)) by FINSEQ_1:def_3; assume A7: j in dom (Col ((M @),i)) ; ::_thesis: (Line (M,i)) . j = (Col ((M @),i)) . j then ( (Line (M,i)) . j = M * (i,j) & [i,j] in Indices M ) by A4, A3, MATRIX_1:def_7, ZFMISC_1:87; hence (Line (M,i)) . j = (M @) * (j,i) by MATRIX_1:def_6 .= (Col ((M @),i)) . j by A1, A3, A7, A6, MATRIX_1:def_8 ; ::_thesis: verum end; len (Line (M,i)) = width M by MATRIX_1:def_7; hence Line (M,i) = Col ((M @),i) by A2, A5, FINSEQ_2:9; ::_thesis: verum end; theorem :: MATRIX_2:15 for D being non empty set for M being Matrix of D for j being Nat st j in Seg (width M) holds Line ((M @),j) = Col (M,j) proof let D be non empty set ; ::_thesis: for M being Matrix of D for j being Nat st j in Seg (width M) holds Line ((M @),j) = Col (M,j) let M be Matrix of D; ::_thesis: for j being Nat st j in Seg (width M) holds Line ((M @),j) = Col (M,j) let j be Nat; ::_thesis: ( j in Seg (width M) implies Line ((M @),j) = Col (M,j) ) assume A1: j in Seg (width M) ; ::_thesis: Line ((M @),j) = Col (M,j) then j in Seg (len (M @)) by MATRIX_1:def_6; then A2: j in dom (M @) by FINSEQ_1:def_3; percases ( len M = 0 or len M > 0 ) ; supposeA3: len M = 0 ; ::_thesis: Line ((M @),j) = Col (M,j) then Seg (len M) = {} ; hence Line ((M @),j) = Col (M,j) by A1, A3, MATRIX_1:def_3; ::_thesis: verum end; supposeA4: len M > 0 ; ::_thesis: Line ((M @),j) = Col (M,j) percases ( width M = 0 or width M > 0 ) ; suppose width M = 0 ; ::_thesis: Line ((M @),j) = Col (M,j) hence Line ((M @),j) = Col (M,j) by A1; ::_thesis: verum end; suppose width M > 0 ; ::_thesis: Line ((M @),j) = Col (M,j) then (M @) @ = M by A4, Th13; hence Line ((M @),j) = Col (M,j) by A2, Th14; ::_thesis: verum end; end; end; end; end; theorem :: MATRIX_2:16 for D being non empty set for M being Matrix of D for i being Nat st i in dom M holds M . i = Line (M,i) proof let D be non empty set ; ::_thesis: for M being Matrix of D for i being Nat st i in dom M holds M . i = Line (M,i) let M be Matrix of D; ::_thesis: for i being Nat st i in dom M holds M . i = Line (M,i) let i be Nat; ::_thesis: ( i in dom M implies M . i = Line (M,i) ) assume A1: i in dom M ; ::_thesis: M . i = Line (M,i) then A2: M . i in rng M by FUNCT_1:def_3; rng M c= D * by FINSEQ_1:def_4; then reconsider p = M . i as FinSequence of D by A2, FINSEQ_1:def_11; M <> {} by A1; then M is Matrix of len M, width M,D by MATRIX_1:20; then A3: len p = width M by A2, MATRIX_1:def_2; A4: len (Line (M,i)) = width M by MATRIX_1:def_7; then A5: dom (Line (M,i)) = Seg (width M) by FINSEQ_1:def_3; A6: for j being Nat st j in Seg (width M) holds M * (i,j) = p . j proof let j be Nat; ::_thesis: ( j in Seg (width M) implies M * (i,j) = p . j ) assume j in Seg (width M) ; ::_thesis: M * (i,j) = p . j then [i,j] in Indices M by A1, ZFMISC_1:87; then ex q being FinSequence of D st ( q = M . i & q . j = M * (i,j) ) by MATRIX_1:def_5; hence M * (i,j) = p . j ; ::_thesis: verum end; now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Line_(M,i))_holds_ (Line_(M,i))_._j_=_p_._j let j be Nat; ::_thesis: ( j in dom (Line (M,i)) implies (Line (M,i)) . j = p . j ) assume A7: j in dom (Line (M,i)) ; ::_thesis: (Line (M,i)) . j = p . j hence (Line (M,i)) . j = M * (i,j) by A5, MATRIX_1:def_7 .= p . j by A6, A5, A7 ; ::_thesis: verum end; hence M . i = Line (M,i) by A3, A4, FINSEQ_2:9; ::_thesis: verum end; notation let K be Field; let i be Nat; let M be Matrix of K; synonym DelLine (M,i) for Del (i,K); end; registration let K be Field; let i be Nat; let M be Matrix of K; cluster DelLine (,M) -> tabular ; coherence DelLine (,M) is tabular proof consider n being Nat such that A1: for x being set st x in rng M holds ex s being FinSequence st ( s = x & len s = n ) by MATRIX_1:def_1; take n ; :: according to MATRIX_1:def_1 ::_thesis: for b1 being set holds ( not b1 in rng (DelLine (,M)) or ex b2 being set st ( b2 = b1 & len b2 = n ) ) let x be set ; ::_thesis: ( not x in rng (DelLine (,M)) or ex b1 being set st ( b1 = x & len b1 = n ) ) A2: rng (DelLine (,M)) c= rng M by FINSEQ_3:106; assume x in rng (DelLine (,M)) ; ::_thesis: ex b1 being set st ( b1 = x & len b1 = n ) hence ex b1 being set st ( b1 = x & len b1 = n ) by A1, A2; ::_thesis: verum end; end; definition let K be Field; let i be Nat; let M be Matrix of K; :: original: DelLine redefine func DelLine (M,i) -> Matrix of K; coherence DelLine (,M) is Matrix of K by FINSEQ_3:105; end; definition let i, j, n be Nat; let K be Field; let M be Matrix of n,K; func Deleting (M,i,j) -> Matrix of K equals :: MATRIX_2:def 6 DelCol ((DelLine (M,i)),j); coherence DelCol ((DelLine (M,i)),j) is Matrix of K ; end; :: deftheorem defines Deleting MATRIX_2:def_6_:_ for i, j, n being Nat for K being Field for M being Matrix of n,K holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j); begin definition let IT be set ; attrIT is permutational means :Def7: :: MATRIX_2:def 7 ex n being Nat st for x being set st x in IT holds x is Permutation of (Seg n); end; :: deftheorem Def7 defines permutational MATRIX_2:def_7_:_ for IT being set holds ( IT is permutational iff ex n being Nat st for x being set st x in IT holds x is Permutation of (Seg n) ); registration cluster non empty permutational for set ; existence ex b1 being set st ( b1 is permutational & not b1 is empty ) proof set n = the Nat; set p = the Permutation of (Seg the Nat); take P = { the Permutation of (Seg the Nat)}; ::_thesis: ( P is permutational & not P is empty ) thus P is permutational ::_thesis: not P is empty proof take the Nat ; :: according to MATRIX_2:def_7 ::_thesis: for x being set st x in P holds x is Permutation of (Seg the Nat) let x be set ; ::_thesis: ( x in P implies x is Permutation of (Seg the Nat) ) assume x in P ; ::_thesis: x is Permutation of (Seg the Nat) hence x is Permutation of (Seg the Nat) by TARSKI:def_1; ::_thesis: verum end; thus not P is empty ; ::_thesis: verum end; end; definition let P be non empty permutational set ; func len P -> Nat means :Def8: :: MATRIX_2:def 8 ex s being FinSequence st ( s in P & it = len s ); existence ex b1 being Nat ex s being FinSequence st ( s in P & b1 = len s ) proof set x = the Element of P; consider n being Nat such that A1: for y being set st y in P holds y is Permutation of (Seg n) by Def7; reconsider n = n as Element of NAT by ORDINAL1:def_12; reconsider q = the Element of P as Permutation of (Seg n) by A1; A2: dom q = Seg n by FUNCT_2:52; then reconsider q = q as FinSequence by FINSEQ_1:def_2; take n ; ::_thesis: ex s being FinSequence st ( s in P & n = len s ) take q ; ::_thesis: ( q in P & n = len q ) thus ( q in P & n = len q ) by A2, FINSEQ_1:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex s being FinSequence st ( s in P & b1 = len s ) & ex s being FinSequence st ( s in P & b2 = len s ) holds b1 = b2 proof let n1, n2 be Nat; ::_thesis: ( ex s being FinSequence st ( s in P & n1 = len s ) & ex s being FinSequence st ( s in P & n2 = len s ) implies n1 = n2 ) given s1 being FinSequence such that A3: s1 in P and A4: n1 = len s1 ; ::_thesis: ( for s being FinSequence holds ( not s in P or not n2 = len s ) or n1 = n2 ) consider n being Nat such that A5: for y being set st y in P holds y is Permutation of (Seg n) by Def7; s1 is Function of (Seg n),(Seg n) by A3, A5; then ( n in NAT & dom s1 = Seg n ) by FUNCT_2:52, ORDINAL1:def_12; then A6: len s1 = n by FINSEQ_1:def_3; given s2 being FinSequence such that A7: s2 in P and A8: n2 = len s2 ; ::_thesis: n1 = n2 s2 is Permutation of (Seg n) by A7, A5; then dom s2 = Seg n by FUNCT_2:52; hence n1 = n2 by A4, A8, A6, FINSEQ_1:def_3; ::_thesis: verum end; end; :: deftheorem Def8 defines len MATRIX_2:def_8_:_ for P being non empty permutational set for b2 being Nat holds ( b2 = len P iff ex s being FinSequence st ( s in P & b2 = len s ) ); definition let P be non empty permutational set ; :: original: len redefine func len P -> Element of NAT ; coherence len P is Element of NAT by ORDINAL1:def_12; end; definition let P be non empty permutational set ; :: original: Element redefine mode Element of P -> Permutation of (Seg (len P)); coherence for b1 being Element of P holds b1 is Permutation of (Seg (len P)) proof let x be Element of P; ::_thesis: x is Permutation of (Seg (len P)) consider n being Nat such that A1: for y being set st y in P holds y is Permutation of (Seg n) by Def7; reconsider n = n as Element of NAT by ORDINAL1:def_12; reconsider q = x as Permutation of (Seg n) by A1; A2: dom q = Seg n by FUNCT_2:52; then reconsider q = q as FinSequence by FINSEQ_1:def_2; len q = n by A2, FINSEQ_1:def_3; then Seg (len P) = Seg n by Def8; hence x is Permutation of (Seg (len P)) by A1; ::_thesis: verum end; end; theorem :: MATRIX_2:17 for n being Nat ex P being non empty permutational set st len P = n proof let n be Nat; ::_thesis: ex P being non empty permutational set st len P = n set p = the Permutation of (Seg n); set P = { the Permutation of (Seg n)}; now__::_thesis:_ex_n_being_Nat_st_ for_x_being_set_st_x_in_{_the_Permutation_of_(Seg_n)}_holds_ x_is_Permutation_of_(Seg_n) take n = n; ::_thesis: for x being set st x in { the Permutation of (Seg n)} holds x is Permutation of (Seg n) let x be set ; ::_thesis: ( x in { the Permutation of (Seg n)} implies x is Permutation of (Seg n) ) assume x in { the Permutation of (Seg n)} ; ::_thesis: x is Permutation of (Seg n) hence x is Permutation of (Seg n) by TARSKI:def_1; ::_thesis: verum end; then reconsider P = { the Permutation of (Seg n)} as non empty permutational set by Def7; take P ; ::_thesis: len P = n len P = n proof set x = the Element of P; reconsider y = the Element of P as Function of (Seg n),(Seg n) by TARSKI:def_1; A1: dom y = Seg n by FUNCT_2:52; then reconsider s = y as FinSequence by FINSEQ_1:def_2; ( n in NAT & len P = len s ) by Def8, ORDINAL1:def_12; hence len P = n by A1, FINSEQ_1:def_3; ::_thesis: verum end; hence len P = n ; ::_thesis: verum end; definition let n be Nat; func Permutations n -> set means :Def9: :: MATRIX_2:def 9 for x being set holds ( x in it iff x is Permutation of (Seg n) ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Permutation of (Seg n) ) proof defpred S1[ set ] means \$1 is Permutation of (Seg n); consider P being set such that A1: for x being set holds ( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S1[x] ) ) from XBOOLE_0:sch_1(); take P ; ::_thesis: for x being set holds ( x in P iff x is Permutation of (Seg n) ) let x be set ; ::_thesis: ( x in P iff x is Permutation of (Seg n) ) thus ( x in P implies x is Permutation of (Seg n) ) by A1; ::_thesis: ( x is Permutation of (Seg n) implies x in P ) assume A2: x is Permutation of (Seg n) ; ::_thesis: x in P then x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; hence x in P by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds ( x in b2 iff x is Permutation of (Seg n) ) ) holds b1 = b2 proof let P1, P2 be set ; ::_thesis: ( ( for x being set holds ( x in P1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds ( x in P2 iff x is Permutation of (Seg n) ) ) implies P1 = P2 ) assume that A3: for x being set holds ( x in P1 iff x is Permutation of (Seg n) ) and A4: for x being set holds ( x in P2 iff x is Permutation of (Seg n) ) ; ::_thesis: P1 = P2 A5: now__::_thesis:_for_x_being_set_st_x_in_P2_holds_ x_in_P1 let x be set ; ::_thesis: ( x in P2 implies x in P1 ) assume x in P2 ; ::_thesis: x in P1 then x is Permutation of (Seg n) by A4; hence x in P1 by A3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_P1_holds_ x_in_P2 let x be set ; ::_thesis: ( x in P1 implies x in P2 ) assume x in P1 ; ::_thesis: x in P2 then x is Permutation of (Seg n) by A3; hence x in P2 by A4; ::_thesis: verum end; hence P1 = P2 by A5, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def9 defines Permutations MATRIX_2:def_9_:_ for n being Nat for b2 being set holds ( b2 = Permutations n iff for x being set holds ( x in b2 iff x is Permutation of (Seg n) ) ); registration let n be Nat; cluster Permutations n -> non empty permutational ; coherence ( Permutations n is permutational & not Permutations n is empty ) proof defpred S1[ set ] means n is Permutation of (Seg n); consider P being set such that A1: for x being set holds ( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S1[x] ) ) from XBOOLE_0:sch_1(); idseq n in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; then reconsider P = P as non empty set by A1; now__::_thesis:_ex_n_being_Nat_st_ for_x_being_set_st_x_in_P_holds_ x_is_Permutation_of_(Seg_n) take n = n; ::_thesis: for x being set st x in P holds x is Permutation of (Seg n) let x be set ; ::_thesis: ( x in P implies x is Permutation of (Seg n) ) assume x in P ; ::_thesis: x is Permutation of (Seg n) hence x is Permutation of (Seg n) by A1; ::_thesis: verum end; then reconsider P = P as non empty permutational set by Def7; for x being set holds ( x in P iff x is Permutation of (Seg n) ) proof let x be set ; ::_thesis: ( x in P iff x is Permutation of (Seg n) ) thus ( x in P implies x is Permutation of (Seg n) ) by A1; ::_thesis: ( x is Permutation of (Seg n) implies x in P ) assume A2: x is Permutation of (Seg n) ; ::_thesis: x in P then x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; hence x in P by A1, A2; ::_thesis: verum end; hence ( Permutations n is permutational & not Permutations n is empty ) by Def9; ::_thesis: verum end; end; theorem :: MATRIX_2:18 for n being Nat holds len (Permutations n) = n proof let n be Nat; ::_thesis: len (Permutations n) = n set x = the Element of Permutations n; reconsider q = the Element of Permutations n as Permutation of (Seg n) by Def9; A1: dom q = Seg n by FUNCT_2:52; then reconsider q = q as FinSequence by FINSEQ_1:def_2; n in NAT by ORDINAL1:def_12; then len q = n by A1, FINSEQ_1:def_3; hence len (Permutations n) = n by Def8; ::_thesis: verum end; theorem :: MATRIX_2:19 Permutations 1 = {(idseq 1)} proof A1: Permutations 1 c= {(idseq 1)} proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Permutations 1 or p in {(idseq 1)} ) assume p in Permutations 1 ; ::_thesis: p in {(idseq 1)} then reconsider q = p as Permutation of (Seg 1) by Def9; A2: dom q = Seg 1 by FUNCT_2:52; ( rng q = Seg 1 & 1 in {1} ) by FUNCT_2:def_3, TARSKI:def_1; then q . 1 in Seg 1 by FINSEQ_1:2, FUNCT_2:4; then A3: q . 1 = 1 by FINSEQ_1:2, TARSKI:def_1; reconsider q = q as FinSequence by A2, FINSEQ_1:def_2; len q = 1 by A2, FINSEQ_1:def_3; then q = idseq 1 by A3, FINSEQ_1:40, FINSEQ_2:50; hence p in {(idseq 1)} by TARSKI:def_1; ::_thesis: verum end; {(idseq 1)} c= Permutations 1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(idseq 1)} or x in Permutations 1 ) assume x in {(idseq 1)} ; ::_thesis: x in Permutations 1 then x = idseq 1 by TARSKI:def_1; hence x in Permutations 1 by Def9; ::_thesis: verum end; hence Permutations 1 = {(idseq 1)} by A1, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let n be Nat; func Group_of_Perm n -> strict multMagma means :Def10: :: MATRIX_2:def 10 ( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) ); existence ex b1 being strict multMagma st ( the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) ) proof defpred S1[ Element of Permutations n, Element of Permutations n, set ] means \$3 = \$2 * \$1; A1: for q, p being Element of Permutations n ex z being Element of Permutations n st S1[q,p,z] proof let q, p be Element of Permutations n; ::_thesis: ex z being Element of Permutations n st S1[q,p,z] reconsider p = p, q = q as Permutation of (Seg n) by Def9; reconsider z = p * q as Element of Permutations n by Def9; take z ; ::_thesis: S1[q,p,z] thus S1[q,p,z] ; ::_thesis: verum end; consider o being BinOp of (Permutations n) such that A2: for q, p being Element of Permutations n holds S1[q,p,o . (q,p)] from BINOP_1:sch_3(A1); take multMagma(# (Permutations n),o #) ; ::_thesis: ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) ) thus ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being strict multMagma st the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) & the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) holds b1 = b2 proof let G1, G2 be strict multMagma ; ::_thesis: ( the carrier of G1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q ) & the carrier of G2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ) implies G1 = G2 ) assume that A3: the carrier of G1 = Permutations n and A4: for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q and A5: the carrier of G2 = Permutations n and A6: for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ; ::_thesis: G1 = G2 now__::_thesis:_for_q,_p_being_Element_of_G1_holds_the_multF_of_G1_._(q,p)_=_the_multF_of_G2_._(q,p) let q, p be Element of G1; ::_thesis: the multF of G1 . (q,p) = the multF of G2 . (q,p) reconsider q9 = q, p9 = p as Element of Permutations n by A3; thus the multF of G1 . (q,p) = p9 * q9 by A4 .= the multF of G2 . (q,p) by A6 ; ::_thesis: verum end; hence G1 = G2 by A3, A5, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines Group_of_Perm MATRIX_2:def_10_:_ for n being Nat for b2 being strict multMagma holds ( b2 = Group_of_Perm n iff ( the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) ) ); registration let n be Nat; cluster Group_of_Perm n -> non empty strict ; coherence not Group_of_Perm n is empty proof the carrier of (Group_of_Perm n) = Permutations n by Def10; hence not the carrier of (Group_of_Perm n) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem Th20: :: MATRIX_2:20 for n being Nat holds idseq n is Element of (Group_of_Perm n) proof let n be Nat; ::_thesis: idseq n is Element of (Group_of_Perm n) the carrier of (Group_of_Perm n) = Permutations n by Def10; hence idseq n is Element of (Group_of_Perm n) by Def9; ::_thesis: verum end; theorem Th21: :: MATRIX_2:21 for n being Nat for p being Element of Permutations n holds ( p * (idseq n) = p & (idseq n) * p = p ) proof let n be Nat; ::_thesis: for p being Element of Permutations n holds ( p * (idseq n) = p & (idseq n) * p = p ) let p be Element of Permutations n; ::_thesis: ( p * (idseq n) = p & (idseq n) * p = p ) A1: ( Seg n = {} implies Seg n = {} ) ; p is Permutation of (Seg n) by Def9; then A2: rng p = Seg n by FUNCT_2:def_3; p is Function of (Seg n),(Seg n) by Def9; then dom p = Seg n by A1, FUNCT_2:def_1; hence ( p * (idseq n) = p & (idseq n) * p = p ) by A2, RELAT_1:52, RELAT_1:54; ::_thesis: verum end; theorem Th22: :: MATRIX_2:22 for n being Nat for p being Element of Permutations n holds ( p * (p ") = idseq n & (p ") * p = idseq n ) proof let n be Nat; ::_thesis: for p being Element of Permutations n holds ( p * (p ") = idseq n & (p ") * p = idseq n ) let p be Element of Permutations n; ::_thesis: ( p * (p ") = idseq n & (p ") * p = idseq n ) p is Permutation of (Seg n) by Def9; hence ( p * (p ") = idseq n & (p ") * p = idseq n ) by FUNCT_2:61; ::_thesis: verum end; theorem Th23: :: MATRIX_2:23 for n being Nat for p being Element of Permutations n holds p " is Element of (Group_of_Perm n) proof let n be Nat; ::_thesis: for p being Element of Permutations n holds p " is Element of (Group_of_Perm n) let p be Element of Permutations n; ::_thesis: p " is Element of (Group_of_Perm n) reconsider p = p as Permutation of (Seg n) by Def9; p " is Element of Permutations n by Def9; hence p " is Element of (Group_of_Perm n) by Def10; ::_thesis: verum end; registration let n be Nat; cluster Group_of_Perm n -> strict Group-like associative ; coherence ( Group_of_Perm n is associative & Group_of_Perm n is Group-like ) proof A1: ex e being Element of (Group_of_Perm n) st for p being Element of (Group_of_Perm n) holds ( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st ( p * g = e & g * p = e ) ) proof reconsider e = idseq n as Element of (Group_of_Perm n) by Th20; take e ; ::_thesis: for p being Element of (Group_of_Perm n) holds ( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st ( p * g = e & g * p = e ) ) reconsider e9 = idseq n as Element of Permutations n by Def9; A2: for p being Element of (Group_of_Perm n) ex g being Element of (Group_of_Perm n) st ( p * g = e & g * p = e ) proof let p be Element of (Group_of_Perm n); ::_thesis: ex g being Element of (Group_of_Perm n) st ( p * g = e & g * p = e ) reconsider q = p as Element of Permutations n by Def10; reconsider r = q as Permutation of (Seg n) by Def9; reconsider f = r " as Element of Permutations n by Def9; reconsider g = f as Element of (Group_of_Perm n) by Th23; take g ; ::_thesis: ( p * g = e & g * p = e ) A3: g * p = q * f by Def10 .= e by Th22 ; p * g = f * q by Def10 .= e by Th22 ; hence ( p * g = e & g * p = e ) by A3; ::_thesis: verum end; for p being Element of (Group_of_Perm n) holds ( p * e = p & e * p = p ) proof let p be Element of (Group_of_Perm n); ::_thesis: ( p * e = p & e * p = p ) reconsider p9 = p as Element of Permutations n by Def10; A4: e * p = p9 * e9 by Def10 .= p by Th21 ; p * e = e9 * p9 by Def10 .= p by Th21 ; hence ( p * e = p & e * p = p ) by A4; ::_thesis: verum end; hence for p being Element of (Group_of_Perm n) holds ( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st ( p * g = e & g * p = e ) ) by A2; ::_thesis: verum end; for p, q, r being Element of (Group_of_Perm n) holds (p * q) * r = p * (q * r) proof let p, q, r be Element of (Group_of_Perm n); ::_thesis: (p * q) * r = p * (q * r) reconsider p9 = p, q9 = q, r9 = r as Element of Permutations n by Def10; A5: ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) proof reconsider p9 = p9, q9 = q9, r9 = r9 as Permutation of (Seg n) by Def9; ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ; hence ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ; ::_thesis: verum end; then A6: q9 * p9 is Element of Permutations n by Def9; A7: r9 * q9 is Element of Permutations n by A5, Def9; (p * q) * r = the multF of (Group_of_Perm n) . ((q9 * p9),r9) by Def10 .= r9 * (q9 * p9) by A6, Def10 .= (r9 * q9) * p9 by RELAT_1:36 .= the multF of (Group_of_Perm n) . (p9,(r9 * q9)) by A7, Def10 .= p * (q * r) by Def10 ; hence (p * q) * r = p * (q * r) ; ::_thesis: verum end; hence ( Group_of_Perm n is associative & Group_of_Perm n is Group-like ) by A1, GROUP_1:1; ::_thesis: verum end; end; theorem Th24: :: MATRIX_2:24 for n being Nat holds idseq n = 1_ (Group_of_Perm n) proof let n be Nat; ::_thesis: idseq n = 1_ (Group_of_Perm n) reconsider e = idseq n as Element of (Group_of_Perm n) by Th20; reconsider e9 = idseq n as Element of Permutations n by Def9; for p being Element of (Group_of_Perm n) holds ( p * e = p & e * p = p ) proof let p be Element of (Group_of_Perm n); ::_thesis: ( p * e = p & e * p = p ) reconsider p9 = p as Element of Permutations n by Def10; A1: e * p = p9 * e9 by Def10 .= p by Th21 ; p * e = e9 * p9 by Def10 .= p by Th21 ; hence ( p * e = p & e * p = p ) by A1; ::_thesis: verum end; hence idseq n = 1_ (Group_of_Perm n) by GROUP_1:4; ::_thesis: verum end; definition let n be Nat; let p be Permutation of (Seg n); attrp is being_transposition means :: MATRIX_2:def 11 ex i, j being Nat st ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds p . k = k ) ); end; :: deftheorem defines being_transposition MATRIX_2:def_11_:_ for n being Nat for p being Permutation of (Seg n) holds ( p is being_transposition iff ex i, j being Nat st ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds p . k = k ) ) ); definition let n be Nat; let IT be Permutation of (Seg n); attrIT is even means :Def12: :: MATRIX_2:def 12 ex l being FinSequence of (Group_of_Perm n) st ( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds ex q being Element of Permutations n st ( l . i = q & q is being_transposition ) ) ); end; :: deftheorem Def12 defines even MATRIX_2:def_12_:_ for n being Nat for IT being Permutation of (Seg n) holds ( IT is even iff ex l being FinSequence of (Group_of_Perm n) st ( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds ex q being Element of Permutations n st ( l . i = q & q is being_transposition ) ) ) ); notation let n be Nat; let IT be Permutation of (Seg n); antonym odd IT for even ; end; theorem :: MATRIX_2:25 for n being Nat holds id (Seg n) is even proof let n be Nat; ::_thesis: id (Seg n) is even set l = <*> the carrier of (Group_of_Perm n); 0 = (2 * 0) + 0 ; then A1: (len (<*> the carrier of (Group_of_Perm n))) mod 2 = 0 by NAT_D:def_2; Product (<*> the carrier of (Group_of_Perm n)) = 1_ (Group_of_Perm n) by GROUP_4:8; then A2: idseq n = Product (<*> the carrier of (Group_of_Perm n)) by Th24; for i being Nat st i in dom (<*> the carrier of (Group_of_Perm n)) holds ex q being Element of Permutations n st ( (<*> the carrier of (Group_of_Perm n)) . i = q & q is being_transposition ) ; hence id (Seg n) is even by A1, A2, Def12; ::_thesis: verum end; definition let K be Field; let n be Nat; let x be Element of K; let p be Element of Permutations n; func - (x,p) -> Element of K equals :: MATRIX_2:def 13 x if p is even otherwise - x; correctness coherence ( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) ); consistency for b1 being Element of K holds verum; ; end; :: deftheorem defines - MATRIX_2:def_13_:_ for K being Field for n being Nat for x being Element of K for p being Element of Permutations n holds ( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) ); definition let X be set ; assume A1: X is finite ; func FinOmega X -> Element of Fin X equals :: MATRIX_2:def 14 X; coherence X is Element of Fin X by A1, FINSUB_1:def_5; end; :: deftheorem defines FinOmega MATRIX_2:def_14_:_ for X being set st X is finite holds FinOmega X = X; theorem :: MATRIX_2:26 for n being Nat holds Permutations n is finite proof let n be Nat; ::_thesis: Permutations n is finite A1: Permutations n c= Funcs ((Seg n),(Seg n)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Permutations n or x in Funcs ((Seg n),(Seg n)) ) assume x in Permutations n ; ::_thesis: x in Funcs ((Seg n),(Seg n)) then x is Function of (Seg n),(Seg n) by Def9; hence x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; ::_thesis: verum end; Funcs ((Seg n),(Seg n)) is finite by FRAENKEL:6; hence Permutations n is finite by A1, FINSET_1:1; ::_thesis: verum end;