:: Invertibility of Matrices of Field Elements :: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang :: :: Received April 2, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies VECTSP_1, RLVECT_1, MATRIX_1, ARYTM_1, FINSEQ_1, TREES_1, RELAT_1, GROUP_1, QC_LANG1, MATRIX_6, CAT_1, MATRIX14, MATRIXR2, FUNCT_1, ARYTM, MATRIX_3, BOOLE, FINSEQ_7, FINSEQ_2, FINSOP_1, PRALG_1, INCSP_1, CAT_3, RVSUM_1, EUCLID, EUCLID_2, FINSEQ_4, CQC_LANG, PARTFUN1, ALGSTR_0, RFINSEQ; notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, RELAT_1, FUNCT_1, BINOP_1, ALGSTR_0, ZFMISC_1, MATRIX_1, FVSUM_1, PARTFUN1, FUNCT_3, RLVECT_1, NUMBERS, FINSEQ_7, FUNCT_2, FUNCOP_1, FINSEQ_1, STRUCT_0, GROUP_1, MATRIX_3, MATRIX_6, BINARITH, XCMPLX_0, NAT_1, VECTSP_1, FINSEQ_2, FINSOP_1, RFINSEQ; constructors DOMAIN_1, RELAT_1, XXREAL_0, FUNCT_3, FVSUM_1, ALGSTR_0, SETWOP_2, NUMBERS, ORDINAL1, BINOP_2, VECTSP_2, MATRIX_1, FINSEQ_7, SETWISEO, FINSOP_1, VECTSP_1, MATRIX_4, MATRIX_2, MATRIX_3, BINOP_1, JORDAN3, BINARITH, RFINSEQ, FINSEQ_4, MATRIX_7, INTEGRA2, MATRIXR1, MATRIX_5, XCMPLX_0, FINSEQ_2, FINSEQOP, SEQ_1, GROUP_1, FINSEQ_1, XREAL_0, MATRIX_6, PARTFUN1, REAL_1, NAT_1, POLYNOM1; registrations FINSEQ_2, XREAL_0, NAT_1, FUNCOP_1, STRUCT_0, XBOOLE_0, VECTSP_1, ORDINAL1, XXREAL_0, RELAT_1, MATRIX_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0, MATRIX_1, STRUCT_0, BINOP_1, RLVECT_1, VECTSP_1, ALGSTR_0; theorems MATRIX_3, VECTSP_1, MATRIX_1, MATRIX_4, GROUP_1, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_7, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, FUNCT_2, XBOOLE_0, ZFMISC_1, MATRIX_7, MATRIXR1, FINSEQ_3, XXREAL_0, ORDINAL1, FINSEQ_4, MATRIXR2, XREAL_1, REAL_1, FUNCOP_1, BINARITH, RLVECT_1, MATRIX_6, MATRIX12, POLYNOM1, PARTFUN1, CARD_2; schemes NAT_1, MATRIX_1; begin :: Preparation reserve x,y,y1,y2 for set, D for non empty set, k,n,m,i,j,l for Element of NAT, K for Field; definition let K be non empty ZeroStr, n; func 0*(K,n) -> FinSequence of K equals n |-> (0.K); coherence; end; definition let K be non empty ZeroStr;let n; redefine func 0*(K,n) -> Element of n-tuples_on (the carrier of K); coherence proof A2: len (0*(K,n))=n by FINSEQ_2:69; (0*(K,n)) in (the carrier of K)* by FINSEQ_1:def 11;then 0*(K,n) in { s where s is Element of (the carrier of K)*:len s = n } by A2; hence thesis by FINSEQ_2:def 4; end; end; reserve L for non empty addLoopStr; theorem BB100: for x being FinSequence of L holds x is Element of (len x)-tuples_on the carrier of L proof let x be FinSequence of L; x is Element of (the carrier of L)* by FINSEQ_1:def 11;then A1: x in { s where s is Element of (the carrier of L)*: len s = len x }; thus thesis by A1,FINSEQ_2:def 4; end; theorem Th6: for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1+x2)=len x1 proof let x1,x2 be FinSequence of L; assume A1: len x1=len x2; set n=len x1; reconsider z1=x1 as Element of (len x1)-tuples_on (the carrier of L) by FINSEQ_2:110; reconsider z2=x2 as Element of n-tuples_on (the carrier of L) by A1,FINSEQ_2:110; dom (z1+z2)=Seg n by FINSEQ_2:144; hence thesis by FINSEQ_1:def 3; end; theorem Th7: for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1-x2)=len x1 proof let x1,x2 be FinSequence of L; assume A1: len x1=len x2; set n=len x1; reconsider z1=x1 as Element of (len x1)-tuples_on (the carrier of L) by FINSEQ_2:110; reconsider z2=x2 as Element of n-tuples_on (the carrier of L) by A1,FINSEQ_2:110; dom (z1-z2)=Seg n by FINSEQ_2:144; hence thesis by FINSEQ_1:def 3; end; reserve G for non empty multLoopStr; theorem FV73: for x1,x2 being FinSequence of G,i st i in dom mlt(x1,x2) holds mlt(x1,x2).i = (x1/.i)*(x2/.i) & (mlt(x1,x2))/.i=(x1/.i)*(x2/.i) proof let x1,x2 be FinSequence of G,i; assume A1: i in dom mlt(x1,x2); A4: dom (the multF of G)=[:the carrier of G,the carrier of G:] by FUNCT_2:def 1; A5: rng x1 c= the carrier of G by FINSEQ_1:def 4; rng x2 c= the carrier of G by FINSEQ_1:def 4;then A8: [:rng x1, rng x2:] c= dom the multF of G by ZFMISC_1:119,A5,A4; mlt(x1,x2)=(the multF of G).:(x1,x2) by FVSUM_1:def 7;then dom mlt(x1,x2) = dom x1 /\ dom x2 by A8,FUNCOP_1:84;then A6: i in dom x1 & i in dom x2 by A1,XBOOLE_0:def 3;then A2: x1/.i=x1.i by PARTFUN1:def 8; A3: x2/.i=x2.i by A6,PARTFUN1:def 8; thus mlt(x1,x2).i = (x1/.i)*(x2/.i) by A1,A2,A3,FVSUM_1:73; hence (mlt(x1,x2))/.i=(x1/.i)*(x2/.i) by A1,PARTFUN1:def 8; end; theorem BB120: for x1,x2 being FinSequence of L,i being Nat st len x1=len x2 & 1<=i & i<=len x1 holds (x1+x2).i=x1/.i + x2/.i & (x1-x2).i=x1/.i - x2/.i proof let x1,x2 be FinSequence of L,i be Nat; assume A1: len x1=len x2 & 1<=i & i<=len x1;then reconsider x10=x1,x20=x2 as Element of (len x1)-tuples_on the carrier of L by BB100; i in Seg len x1 by A1,FINSEQ_1:3;then A3: i in Seg len (x1+x2) by A1,Th6; A4: x10/.i=x10.i by A1,FINSEQ_4:24; A5: x20/.i=x20.i by A1,FINSEQ_4:24; i in dom (x1+x2) by FINSEQ_1:def 3,A3; hence (x1+x2).i=x1/.i + x2/.i by FVSUM_1:21,A4,A5; i in Seg len x1 by A1,FINSEQ_1:3;then i in Seg len (x1-x2) by A1,Th7;then i in dom (x1-x2) by FINSEQ_1:def 3; hence thesis by FVSUM_1:42,A4,A5; end; theorem BB200: for a being Element of K, x being FinSequence of K holds -a*x = (-a)*x & -a*x = a*(-x) proof let a be Element of K, x be FinSequence of K; set n=len x; reconsider x0=x as Element of n-tuples_on (the carrier of K) by BB100; reconsider x1=x as Element of (n-tuples_on (the carrier of K)) by BB100; reconsider y=a*x0 as Element of (n-tuples_on (the carrier of K)); thus -a*x=(-1_K)*y by FVSUM_1:72 .=((-1_K)*a)*x0 by FVSUM_1:67 .=(- 1_K *a)*x0 by VECTSP_1:40 .=(- a)*x by VECTSP_1:def 19; thus -a*x= (-1_K)*y by FVSUM_1:72 .=((-1_K)*a)*x0 by FVSUM_1:67 .=a*((-1_K)*x0) by FVSUM_1:67 .=a*(-x) by FVSUM_1:72; end; theorem BB240: for x1,x2,y1,y2 being FinSequence of G st len x1=len x2 & len y1=len y2 holds mlt(x1^y1,x2^y2)=(mlt(x1,x2))^(mlt(y1,y2)) proof let x1,x2,y1,y2 be FinSequence of G; assume A1: len x1=len x2 & len y1=len y2; A3: (the multF of G).:(x1^y1,x2^y2)=(the multF of G) * (<: x1^y1,x2^y2 :>) by FUNCOP_1:def 3; A4: dom (the multF of G)=[:the carrier of G,the carrier of G:] by FUNCT_2:def 1; A5: rng (x1^y1) c= the carrier of G by FINSEQ_1:def 4; B4c: rng (x2^y2) c= the carrier of G by FINSEQ_1:def 4; B4b: [:rng (x1^y1), rng (x2^y2):] c= dom (the multF of G) by ZFMISC_1:119,A5,A4,B4c; B4a: dom ((the multF of G) * (<: x1^y1,x2^y2 :>)) =dom (x1^y1) /\ dom (x2^y2) by FUNCOP_1:84,A3,B4b; B5: len (x1^y1)=len x1+len y1 by FINSEQ_1:35; B6: len (x2^y2)=len x2+len y2 by FINSEQ_1:35; B7: dom (x1^y1)=Seg len (x1^y1) by FINSEQ_1:def 3; D1: dom (x2^y2)=Seg len (x2^y2) by FINSEQ_1:def 3; D2: dom (x1^y1)=dom (x2^y2) by A1,FINSEQ_1:35,B6,B7,D1; B10: dom (mlt(x1^y1,x2^y2))= dom (x1^y1) by FVSUM_1:def 7,A3,B4a,D2; A8: len (mlt(x1^y1,x2^y2))=len (x1^y1) by B7,FINSEQ_1:def 3,B10 .=len x1 + len y1 by FINSEQ_1:35; C5: dom x2=Seg len x1 by FINSEQ_1:def 3,A1 .=dom x1 by FINSEQ_1:def 3; C5b: dom y2=Seg len y1 by FINSEQ_1:def 3,A1 .=dom y1 by FINSEQ_1:def 3; A3: (the multF of G).:(x1,x2)=(the multF of G) * (<:x1,x2:>) by FUNCOP_1:def 3; A4: dom (the multF of G)=[:the carrier of G,the carrier of G:] by FUNCT_2:def 1; A5: rng (x1) c= the carrier of G by FINSEQ_1:def 4; B12: rng (x2) c= the carrier of G by FINSEQ_1:def 4; B13: [:rng (x1), rng (x2):] c= dom (the multF of G) by ZFMISC_1:119,A5,A4,B12; B14: dom ((the multF of G) * (<:x1,x2:>)) =dom (x1) /\ dom (x2) by FUNCOP_1:84,A3,B13; C8: dom (mlt(x1,x2)) =dom x1 by C5,FVSUM_1:def 7,A3,B14; B16: dom (mlt(x1,x2))=Seg len x1 by FINSEQ_1:def 3,C8; A3: (the multF of G).:(y1,y2)=(the multF of G) * (<:y1,y2:>) by FUNCOP_1:def 3; A5: rng y1 c= the carrier of G by FINSEQ_1:def 4; B18: rng y2 c= the carrier of G by FINSEQ_1:def 4; B19: [:rng y1, rng y2:] c= dom the multF of G by ZFMISC_1:119,A5,A4,B18; B20: dom ((the multF of G) * (<:y1,y2:>)) =dom y1 /\ dom y2 by FUNCOP_1:84,A3,B19; C8b: dom mlt(y1,y2) =dom y1 by C5b,FVSUM_1:def 7,A3,B20; B21: dom (mlt(y1,y2))=Seg len y1 by FINSEQ_1:def 3,C8b; B23: len (mlt(y1,y2))= len y1 by FINSEQ_1:def 3,B21; B24:len (mlt(x1^y1,x2^y2)) =len (mlt(x1,x2))+ len(mlt(y1,y2)) by A8,FINSEQ_1:def 3,B16,B23; A2: len (mlt(x1^y1,x2^y2))=len ((mlt(x1,x2))^(mlt(y1,y2))) by FINSEQ_1:35,B24; for i being Nat st 1<=i & i<=len (mlt(x1^y1,x2^y2)) holds (mlt(x1^y1,x2^y2)).i=((mlt(x1,x2))^(mlt(y1,y2))).i proof let i be Nat; assume B1: 1<=i & i<=len (mlt(x1^y1,x2^y2)); B2: i in Seg len (mlt(x1^y1,x2^y2)) by FINSEQ_1:3,B1; B3: i in dom (mlt(x1^y1,x2^y2)) by FINSEQ_1:def 3,B2; B22: 1<=i & i<=len x1+len y1 by FINSEQ_1:3,B3,B7,B5,B10; K2: i<=len (x1^y1) by FINSEQ_1:3,B3,B7,B10; A36: (x1^y1)/.i= (x1^y1).i by B1,FINSEQ_4:24,K2; A36a: i<=len (x2^y2) by FINSEQ_1:3,B3,B7,B5,B10,B6,A1; A37: (x2^y2)/.i= (x2^y2).i by B1,FINSEQ_4:24,A36a; now per cases; suppose C0: i<=len x1;then C2: i in Seg len x1 by B1,FINSEQ_1:3; C1: i in dom x1 by FINSEQ_1:def 3,C2; A34: x1/.i=x1.i by B1,FINSEQ_4:24,C0; A35: x2/.i=x2.i by B1,FINSEQ_4:24,C0,A1; K2: i in dom x2 by FINSEQ_1:def 3,C2,A1; C4: (x2^y2).i=x2.i by FINSEQ_1:def 7,K2; C7: i in dom (mlt(x1,x2)) by FINSEQ_1:def 3,C2,C8; ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(x1,x2)).i by FINSEQ_1:def 7,C7 .=(x1/.i)*(x2/.i) by C7,FV73; hence ((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i by FINSEQ_1:def 7,C1,C4,A34,A35,A36,A37; end; suppose C0: i>len x1; set k=i -' len x1; C11: k=i-len x1 by BINARITH:50,C0; C2: i= len x1 +k by C11; C2a: k>0 by C0,C11,XREAL_1:52; C12: 0+1<=k by NAT_1:13,C2a; C12a: i-len x1 <=len x1 + len y1 - len x1 by B22,XREAL_1:15; C56: k<=len y1 by BINARITH:50,C0,C12a; C10: k in Seg len y1 by C12,FINSEQ_1:3,C56; C10a: k in dom y2 by FINSEQ_1:def 3,A1,C10; C4a: k in Seg len y1 by C12,FINSEQ_1:3,C56; C13: k in dom y1 by FINSEQ_1:def 3,C4a; C3: (x1^y1).i=y1.k by C2,FINSEQ_1:def 7,C13; C7: k in dom (mlt(y1,y2)) by C8b,FINSEQ_1:def 3,C4a; A34: y1/.k=y1.k by C56,C12,FINSEQ_4:24; A35: y2/.k=y2.k by C56,C12,FINSEQ_4:24,A1; K2: i<=len (x1^y1) by FINSEQ_1:3,B3,B7,B10; A36: (x1^y1)/.i= (x1^y1).i by B1,FINSEQ_4:24,K2; A36a: i<=len (x2^y2) by FINSEQ_1:3,B3,B7,B5,B10,B6,A1; A37: (x2^y2)/.i= (x2^y2).i by B1,FINSEQ_4:24,A36a; A37a: i=len (mlt(x1,x2)) +k by FINSEQ_1:def 3,B16,C2; ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(y1,y2)).k by C7,FINSEQ_1:def 7,A37a .=(y1/.k)*(y2/.k) by C7,FV73; hence ((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i by C3,C2,FINSEQ_1:def 7,A1,C10a,A34,A35,A36,A37; end; end; hence (mlt(x1^y1,x2^y2)).i=((mlt(x1,x2))^(mlt(y1,y2))).i by B3,FV73; end; hence thesis by FINSEQ_1:18,A2; end; notation let K;let e1,e2 be FinSequence of K; synonym |( e1,e2 )| for e1 "*" e2; end; theorem BB243: for x,y being FinSequence of K,a being Element of K st len x=len y holds mlt(a*x,y)=a*(mlt(x,y)) & mlt(x,a*y)=a*(mlt(x,y)) proof let x,y be FinSequence of K,a be Element of K; assume A0: len x=len y; reconsider x0=x as Element of (len x)-tuples_on (the carrier of K) by BB100; reconsider y0=y as Element of (len x)-tuples_on (the carrier of K) by BB100,A0; thus mlt(a*x,y)=a*(mlt(x0,y0)) by FVSUM_1:83 .=a*(mlt(x,y)); thus mlt(x,a*y)=a*(mlt(x0,y0)) by FVSUM_1:83 .=a*(mlt(x,y)); end; theorem for x,y being FinSequence of K,a being Element of K st len x=len y holds |(a*x,y)| = a*|(x,y)| proof let x,y be FinSequence of K,a be Element of K; assume A1: len x=len y; A3: Sum mlt(a*x,y) = Sum (a*(mlt(x,y))) by BB243,A1; A4: Sum mlt(a*x,y) =a*(Sum mlt(x,y)) by FVSUM_1:92,A3; Sum mlt(a*x,y) =a*|(x,y)| by FVSUM_1:def 10,A4; hence |(a*x,y)| = a*|(x,y)| by FVSUM_1:def 10; end; theorem BB246: for x,y being FinSequence of K,a being Element of K st len x=len y holds |(x,a*y)| = a*|(x,y)| proof let x,y be FinSequence of K,a be Element of K; assume A1: len x=len y; A3: Sum mlt(x,a*y) =(Sum (a*(mlt(x,y)))) by BB243,A1; A4: Sum mlt(x,a*y) =a*(Sum mlt(x,y)) by FVSUM_1:92,A3; Sum mlt(x,a*y) =a*|(x,y)| by FVSUM_1:def 10,A4; hence |(x,a*y)| = a*|(x,y)| by FVSUM_1:def 10; end; theorem BB248: for x,y1,y2 being FinSequence of K,a being Element of K st len x=len y1 & len x=len y2 holds |(x,y1+y2)| = |(x,y1)| + |(x,y2)| proof let x,y1,y2 be FinSequence of K,a be Element of K; assume A0: len x=len y1 & len x=len y2; reconsider x0=x as Element of (len x)-tuples_on (the carrier of K) by BB100; reconsider y10=y1,y20=y2 as Element of (len x)-tuples_on (the carrier of K) by BB100,A0; K2: Sum mlt(x,y1+y2) = Sum (mlt(x0,y10) + mlt(x0,y20)) by MATRIX_4:57,A0; K3: Sum mlt(x,y1+y2) = Sum mlt(x0,y10) + Sum mlt(x0,y20) by FVSUM_1:95,K2; K4: Sum mlt(x,y1+y2) = Sum mlt(x,y1) + |(x,y2)| by FVSUM_1:def 10,K3; Sum mlt(x,y1+y2) = |(x,y1)| + |(x,y2)| by FVSUM_1:def 10,K4; hence |(x,y1+y2)| = |(x,y1)| + |(x,y2)| by FVSUM_1:def 10; end; theorem BB250: for x1,x2,y1,y2 being FinSequence of K st len x1=len x2 & len y1=len y2 holds |( x1^y1, x2^y2 )| = |(x1,x2)| + |(y1,y2)| proof let x1,x2,y1,y2 be FinSequence of K; assume A1: len x1=len x2 & len y1=len y2; Sum ((mlt(x1,x2))^(mlt(y1,y2)))=Sum mlt(x1,x2) + Sum mlt(y1,y2) by RLVECT_1:58;then Sum mlt(x1^y1,x2^y2) = Sum mlt(x1,x2) + Sum mlt(y1,y2) by BB240,A1;then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + Sum mlt(y1,y2) by FVSUM_1:def 10;then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + |(y1,y2)| by FVSUM_1:def 10; hence |( x1^y1, x2^y2 )| = |(x1,x2)| + |(y1,y2)| by FVSUM_1:def 10; end; theorem Th2: for p1 being Element of n-tuples_on the carrier of K holds mlt(p1,(n |-> (0.K)))=n |-> (0.K) proof let p1 be Element of n-tuples_on (the carrier of K); thus mlt(p1,(n |-> (0.K)))= mlt(p1,(0.K)*(0*(K,n))) by FVSUM_1:71 .= (0.K)*(mlt(p1,0*(K,n))) by FVSUM_1:83 .= n |-> (0.K) by FVSUM_1:71; end; notation let n;let K;let A be Matrix of n,K; synonym Inv A for A~; end; begin :: Zero Vectors and Base Vectors of Field Elements theorem MR103: 1.(K,0)=0.(K,0) & 1.(K,0)={} proof A1: len 1.(K,0) = 0 & width 1.(K,0)=0 by MATRIX_1:25; len 0.(K,0) = 0 by MATRIX_1:25;then 0.(K,0)={} by CARD_2:59; hence 1.(K,0)=0.(K,0) by A1,CARD_2:59; thus 1.(K,0)={} by A1,CARD_2:59; end; theorem AA4350: for A being Matrix of 0,K holds A={} & A=1.(K,0) & A=0.(K,0) proof let A be Matrix of 0,K; len A=0 by MATRIX_1:25; hence A={} by CARD_2:59; hence A=1.(K,0) by MR103; hence A=0.(K,0) by MR103; end; theorem for A being Matrix of 0,K holds A is invertible proof let A be Matrix of 0,K; A*A= 1.(K,0) by AA4350;then A is_reverse_of A by MATRIX_6:def 2; hence A is invertible by MATRIX_6:def 3; end; theorem AA41: for A,B,C being Matrix of n,K holds A*B*C=A*(B*C) proof let A,B,C be Matrix of n,K; B1: len A=n & width A=n by MATRIX_1:25; B2: len B=n & width B=n by MATRIX_1:25; len C =n & width C =n by MATRIX_1:25; hence A*B*C=A*(B*C) by B1,B2,MATRIX_3:35; end; theorem AA4140: for A,B being Matrix of n,K holds A is invertible & B=A~ iff B*A=1.(K,n) & A*B=1.(K,n) proof let A,B be Matrix of n,K; hereby assume A is invertible & B=A~;then B is_reverse_of A by MATRIX_6:def 4; hence B*A=1.(K,n) & A*B=1.(K,n) by MATRIX_6:def 2; end; hereby assume B*A=1.(K,n) & A*B=1.(K,n);then B2: B is_reverse_of A by MATRIX_6:def 2; hence A is invertible by MATRIX_6:def 3; hence B=A~ by MATRIX_6:def 4,B2; end; end; theorem AA4145: for A being Matrix of n,K holds A is invertible iff ex B being Matrix of n,K st B*A=1.(K,n) & A*B=1.(K,n) proof let A be Matrix of n,K; thus A is invertible implies ex B being Matrix of n,K st B*A=1.(K,n) & A*B=1.(K,n) proof assume A is invertible;then (A~)*A=1.(K,n) & A*(A~)=1.(K,n) by AA4140; hence ex B being Matrix of n,K st B*A=1.(K,n) & A*B=1.(K,n); end; thus (ex B being Matrix of n,K st B*A=1.(K,n) & A*B=1.(K,n)) implies A is invertible by AA4140; end; theorem Th17: for x being FinSequence of K holds |(x, 0*(K,len x))| = 0.K proof let x be FinSequence of K; set n=len x; reconsider p1=x as Element of n-tuples_on (the carrier of K) by FINSEQ_2:110; |(x, 0*(K,n))| = Sum mlt(p1,0*(K,n)) by FVSUM_1:def 10 .= Sum 0*(K,n) by Th2 .= 0.K by MATRIX_3:13; hence thesis; end; theorem Th18: for x being FinSequence of K holds |(0*(K,len x),x)| = 0.K proof let x be FinSequence of K; thus |(0*(K,len x),x)| = |(x,0*(K,len x))| by FVSUM_1:115 .= 0.K by Th17; end; theorem BB270: for a being Element of K holds |( <* 0.K *>, <* a *> )|=0.K proof let a be Element of K; A1: len (<* a *>) =1 by FINSEQ_1:56; thus |( <* 0.K *>, <* a *> )| =|( 0*(K,1),<* a *> )| by FINSEQ_2:73 .= 0.K by A1,Th18; end; definition let K be non empty set, n be Nat, a be Element of K; redefine func n |-> a -> FinSequence of K; coherence proof reconsider n' = n as Element of NAT by ORDINAL1:def 13; n' |-> a is FinSequence of K; hence thesis; end; end; definition let K;let n,i be Nat; func Base_FinSeq(K,n,i) -> FinSequence of K equals Replace((n |-> 0.K),i,1.K); coherence; end; theorem AA1100: for n, i being Nat holds len Base_FinSeq(K,n,i)=n proof let n, i be Nat; len (Replace((n |-> (0.K)),i,1.K)) = len (n |-> (0.K)) by FINSEQ_7:7 .= n by FINSEQ_2:69; hence len (Base_FinSeq(K,n,i))=n; end; theorem AA1110: for i, n being Nat st 1<=i & i<=n holds (Base_FinSeq(K,n,i)).i=1.K proof let i, n be Nat; assume A1: 1<=i & i<=n; A3: len (n |-> (0.K))=n by FINSEQ_2:69; A2: len (Replace((n |-> (0.K)),i,1.K)) = len (n |-> 0.K) by FINSEQ_7:7 .= n by FINSEQ_2:69; thus (Base_FinSeq(K,n,i)).i = (Replace((n |-> (0.K)),i,1.K))/.i by FINSEQ_4:24,A2,A1 .= 1.K by FINSEQ_7:10,A1,A3; end; theorem AA1120: for i,j,n be Nat st 1<=i & i<=n & 1<=j & j<=n & i<>j holds (Base_FinSeq(K,n,i)).j=0.K proof let i,j,n be Nat; assume A1: 1<=i & i<=n & 1<=j & j<=n & i<>j;then A6: j in Seg n by FINSEQ_1:3; A3: len (n |-> (0.K))=n by FINSEQ_2:69; A2: len (Replace((n |-> (0.K)),i,(1.K))) = len (n |-> (0.K)) by FINSEQ_7:7 .= n by FINSEQ_2:69; thus (Base_FinSeq(K,n,i)).j = (Replace((n |-> (0.K)),i,(1.K)))/.j by FINSEQ_4:24,A2,A1 .= ((n |-> (0.K)))/.j by FINSEQ_7:12,A1,A3 .=((n |-> (0.K))).j by FINSEQ_4:24,A3,A1 .= 0.K by A1,A6,FINSEQ_2:71; end; theorem AA1200: for i,n being Nat st 1<=i & i<=n holds (1.(K,n)).i=Base_FinSeq(K,n,i) proof let i,n be Nat; assume A1: 1<=i & i<=n; A2: len (1.(K,n))=n by MATRIX_1:25; A12: 1<=n by A1,XXREAL_0:2; A3: len Base_FinSeq(K,n,i)=n by AA1100; [i,1] in Indices (1.(K,n)) by A1,A12,MATRIX_1:38;then consider q being FinSequence of K such that A10: q = (1.(K,n)).i & (1.(K,n))*(i,1) = q.1 by MATRIX_1:def 6; i in dom (1.(K,n)) by A1,A2,FINSEQ_3:27;then q in rng (1.(K,n)) by FUNCT_1:def 5,A10;then A2b: len q=n by MATRIX_1:def 3; for j be Nat st 1<=j & j<=n holds q.j=(Base_FinSeq(K,n,i)).j proof let j be Nat; assume B1: 1<=j & j<=n; A8: [i,j] in Indices (1.(K,n)) by A1,B1,MATRIX_1:38;then consider q0 being FinSequence of K such that A10b: q0 = (1.(K,n)).i & (1.(K,n))*(i,j) = q0.j by MATRIX_1:def 6; per cases; suppose B0: i=j; (1.(K,n))*(i,i) = 1_(K) by A8,MATRIX_1:def 12,B0; hence q.j=(Base_FinSeq(K,n,i)).j by B0,AA1110,A1,A10,A10b; end; suppose B0: i<>j; q.j=0.K by A8,MATRIX_1:def 12,B0,A10,A10b; hence q.j=(Base_FinSeq(K,n,i)).j by B0,AA1120,A1,B1; end; end; hence thesis by A10,A2b,A3,FINSEQ_1:18; end; theorem BB300: for i,j st 1<=i & i<=n & 1<=j & j<=n holds (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i)).j proof let i,j; assume A1: 1<=i & i<=n & 1<=j & j<=n;then [i,j] in Indices (1.(K,n)) by MATRIX_1:38;then ex p3 being FinSequence of K st p3 = (1.(K,n)).i & 1.(K,n)*(i,j) = p3.j by MATRIX_1:def 6; hence 1.(K,n)*(i,j)=(Base_FinSeq(K,n,i)).j by A1,AA1200; end; theorem for A being Matrix of n,K holds A=0.(K,n) iff for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K proof let A be Matrix of n,K; thus A=0.(K,n) implies for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K proof assume B1: A=0.(K,n); let i,j be Element of NAT; assume C1: 1<=i & i<=n & 1<=j & j<=n; set A3=0.(K,n,n); reconsider B3=0.(K,n,n) as Matrix of n,K; set A2=0.(K,n),B2=0.(K,n); C3: A3=A2 & B3=B2 & A=A2 & B2=A by B1,MATRIX_3:def 1; C6: [i,j] in Indices A2 by C1,MATRIX_1:38; C7: (A2+B2)*(i,j)=A2*(i,j)+B2*(i,j) by MATRIX_3:def 3,C6; C8: A2*(i,j)=A2*(i,j)+A2*(i,j) by MATRIX_3:6,C3,C7; A2*(i,j) - A2*(i,j) = A2*(i,j) +(A2*(i,j) - A2*(i,j)) by RLVECT_1:42,C8 .=A2*(i,j) +0.K by RLVECT_1:28 .=A2*(i,j) by RLVECT_1:10; hence A*(i,j)=0.K by B1,RLVECT_1:28; end; assume B1: for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K; B2: len A=n & width A=n & Indices A=[: Seg n,Seg n :] by MATRIX_1:25; for i,j being Nat st [i,j] in Indices A holds A*(i,j) = A*(i,j) + A*(i,j) proof let i,j be Nat; assume [i,j] in Indices A;then i in Seg n & j in Seg n by B2,ZFMISC_1:106;then C2: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; A*(i0,j0)=0.K by B1,C2; hence A*(i,j) = A*(i,j) + A*(i,j) by RLVECT_1:10; end;then B4: A=A+A by MATRIX_3:def 3,B2; A = 0.(K,len A,width A) by B4,MATRIX_4:6; hence A=0.(K,n) by B2,MATRIX_3:def 1; end; theorem BB370: for A being Matrix of n,K holds A=1.(K,n) iff for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=IFEQ(i,j,1.K,0.K) proof let A be Matrix of n,K; B2: len A=n & width A=n & Indices A=[: Seg n,Seg n :] by MATRIX_1:25; B2b: len (1.(K,n))=n & width (1.(K,n))=n & Indices (1.(K,n))=[: Seg n,Seg n :] by MATRIX_1:25; thus A=1.(K,n) implies for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=IFEQ(i,j,1.K,0.K) proof assume B1:A=1.(K,n); let i,j be Element of NAT; assume X: 1<=i & i<=n & 1<=j & j<=n; C2: [i,j] in Indices A by MATRIX_1:38,X; per cases; suppose D1: i=j;then A*(i,j)=1.K by MATRIX_1:def 12,C2,B1; hence A*(i,j)=IFEQ(i,j,1.K,0.K) by D1,FUNCOP_1:def 8; end; suppose D1: i<>j;then A*(i,j)=0.K by MATRIX_1:def 12,C2,B1; hence A*(i,j)=IFEQ(i,j,1.K,0.K) by D1,FUNCOP_1:def 8; end; end; thus (for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=IFEQ(i,j,1.K,0.K)) implies A=1.(K,n) proof assume C1: for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=IFEQ(i,j,1.K,0.K); C3: len A = len (1.(K,n)) & width A = width (1.(K,n)) by MATRIX_1:25,B2b; for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (1.(K,n))*(i,j) proof let i,j be Nat; assume D1: [i,j] in Indices A;then i in Seg n & j in Seg n by B2,ZFMISC_1:106;then D3: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; D4: A*(i0,j0)=IFEQ(i0,j0,1.K,0.K) by C1,D3; per cases; suppose E1: i0=j0;then A*(i0,j0)=1_K by D4,FUNCOP_1:def 8; hence A*(i,j) = (1.(K,n))*(i,j) by E1,MATRIX_1:def 12,D1,B2,B2b; end; suppose E1: i0<>j0;then A*(i0,j0)=0.K by D4,FUNCOP_1:def 8; hence A*(i,j) = (1.(K,n))*(i,j) by E1,MATRIX_1:def 12,D1,B2,B2b; end; end; hence A=1.(K,n) by MATRIX_1:21,C3; end; end; begin :: Conditions of Invertibility theorem AA44: for A,B being Matrix of n,K holds (A*B)@=(B@)*(A@) proof let A,B be Matrix of n,K; per cases; suppose B0: n<>0; B1: len A=n & len B=n by MATRIX_1:25; width A=n & width B=n by MATRIX_1:25; hence (A*B)@=(B@)*(A@) by MATRIX_3:24,B0,B1; end; suppose B0: n=0; thus (A*B)@=1.(K,n) by AA4350,B0 .=(B@)*(A@) by AA4350,B0; end; end; theorem BB400: for A being Matrix of n,K st A is invertible holds A@ is invertible & (A@)~ =(A~)@ proof let A be Matrix of n,K; assume A is invertible;then consider B being Matrix of n,K such that A2: B*A=1.(K,n) & A*B=1.(K,n) by AA4145; (A*B)@ = (B@)*(A@) by AA44;then A3: (B@)*(A@)=1.(K,n) by A2,MATRIX_6:10; (B*A)@ = (A@)*(B@) by AA44;then A4: (A@)*(B@)=1.(K,n) by A2,MATRIX_6:10; B=A~ by AA4140,A2; hence A@ is invertible & (A@)~=(A~)@ by AA4140,A3,A4; end; theorem AA2626: for x being FinSequence of K, a being Element of K st (ex i st 1<=i & i<=len x & x.i=a & (for j st j<>i & 1<=j & j<=len x holds x.j=0.K)) holds Sum x=a proof let x be FinSequence of K, a be Element of K; given i such that A2: 1<=i & i<=len x & x.i=a & (for j st j<>i & 1<=j & j<=len x holds x.j=0.K); A9: 1<=len x by A2,XXREAL_0:2; consider f being Function of NAT,(the carrier of K) such that A4: f.1 = x.1 & (for n st 0 <> n & n < len x holds f.(n + 1) = (the addF of K).(f.n,x.(n + 1))) & (the addF of K) "**" x = f.(len x) by FINSOP_1:def 1,A9; A30: for j st 1<=j & jk;then D2: 1>=k+1 by NAT_1:13; 1<=1+k by NAT_1:12;then D3: k+1=1 by D2,XXREAL_0:1; now per cases; suppose k+1=i; hence 1<=k+1 & k+1=i; hence 1<=k+1 & k+1i & 1<=j & j<=m holds y.j= 0.K) proof let x,y be FinSequence of K,i; assume A1: len x=m & y=mlt (x,Base_FinSeq(K,m,i)) & 1<=i & i<=m; A2: i in dom x by FINSEQ_3:27,A1; A3: len (Base_FinSeq(K,m,i))=m by AA1100; A4: dom (the multF of K)=[:the carrier of K,the carrier of K:] by FUNCT_2:def 1; A5: rng (x) c= the carrier of K by FINSEQ_1:def 4; B1: rng (Base_FinSeq(K,m,i)) c= the carrier of K by FINSEQ_1:def 4; B2: [:rng (x), rng (Base_FinSeq(K,m,i)):] c= dom (the multF of K) by ZFMISC_1:119,A5,A4,B1; B3: dom ((the multF of K).:(x,Base_FinSeq(K,m,i))) =dom x /\ dom (Base_FinSeq(K,m,i)) by FUNCOP_1:84,B2; A5: dom (mlt (x,Base_FinSeq(K,m,i)))= dom x /\ dom (Base_FinSeq(K,m,i)) by FVSUM_1:def 7,B3 .= Seg m /\ dom (Base_FinSeq(K,m,i)) by FINSEQ_1:def 3,A1 .= Seg m /\ Seg m by FINSEQ_1:def 3,A3 .= Seg m;then A4: i in dom (mlt (x,Base_FinSeq(K,m,i))) by A1,FINSEQ_1:3; C1: 1<=i & i<=len (Base_FinSeq(K,m,i)) by A1,AA1100; A32: (Base_FinSeq(K,m,i))/.i=(Base_FinSeq(K,m,i)).i by FINSEQ_4:24,C1; (mlt (x,Base_FinSeq(K,m,i))).i=(x/.i)*((Base_FinSeq(K,m,i))/.i) by A4,FV73 .= (x/.i)* 1.K by AA1110,A1,A32 .= x/.i by VECTSP_1:def 16 .= x.i by PARTFUN1:def 8,A2; hence y.i=x.i by A1; let j; assume B1: j<>i & 1<=j & j<=m; C2: 1<=j & j<=len (Base_FinSeq(K,m,i)) by B1,AA1100; C3: (Base_FinSeq(K,m,i))/.j = (Base_FinSeq(K,m,i)).j by C2,FINSEQ_4:24 .= 0.K by B1,AA1120,A1; A4b: j in dom (mlt (x,Base_FinSeq(K,m,i))) by FINSEQ_1:3,A5,B1; (mlt (x,Base_FinSeq(K,m,i))).j = (x/.j)*((Base_FinSeq(K,m,i))/.j) by A4b,FV73 .= 0.K by C3,VECTSP_1:36; hence y.j= 0.K by A1; end; theorem AA2627: for x being FinSequence of K st len x=m & 1<=i & i<=m holds |( x,Base_FinSeq(K,m,i) )|=x.i & |( x,Base_FinSeq(K,m,i) )|=x/.i proof let x be FinSequence of K; assume A1: len x=m & 1<=i & i<=m; reconsider q=(mlt (x,Base_FinSeq(K,m,i))) as FinSequence of K; A3: len (Base_FinSeq(K,m,i))=m by AA1100; A4: dom (the multF of K)=[:the carrier of K,the carrier of K:] by FUNCT_2:def 1; A5: rng (x) c= the carrier of K by FINSEQ_1:def 4; rng (Base_FinSeq(K,m,i)) c= the carrier of K by FINSEQ_1:def 4;then [:rng (x), rng (Base_FinSeq(K,m,i)):] c= dom (the multF of K) by ZFMISC_1:119,A5,A4;then A5d: dom ((the multF of K).:(x,Base_FinSeq(K,m,i))) =dom x /\ dom (Base_FinSeq(K,m,i)) by FUNCOP_1:84; B1: dom (mlt (x,Base_FinSeq(K,m,i)))= dom x /\ dom (Base_FinSeq(K,m,i)) by FVSUM_1:def 7,A5d .= Seg m /\ dom (Base_FinSeq(K,m,i)) by FINSEQ_1:def 3,A1 .= Seg m /\ Seg m by FINSEQ_1:def 3,A3 .= Seg m; A18: x/.i=x.i by A1,FINSEQ_4:24; A2: len (mlt (x,Base_FinSeq(K,m,i)))=m by FINSEQ_1:def 3,B1; A2a: (mlt(x,Base_FinSeq(K,m,i))).i=x/.i & (for j st j<>i & 1<=j & j<=m holds (mlt (x,Base_FinSeq(K,m,i))).j= 0.K) by AA2626b,A1,A18; A2b: Sum (mlt (x,Base_FinSeq(K,m,i)))=x.i by AA2626,A1,A2,A18,A2a; hence |( x,Base_FinSeq(K,m,i) )|=x.i by FVSUM_1:def 10; x.i=x/.i by A1,FINSEQ_4:24; hence |( x,Base_FinSeq(K,m,i) )|=x/.i by FVSUM_1:def 10,A2b; end; theorem AA2629: for m,i st 1<=i & i<=m holds |( Base_FinSeq(K,m,i),Base_FinSeq(K,m,i) )|= 1.K proof let m,i; assume A0: 1<=i & i<=m; len (Base_FinSeq(K,m,i))=m by AA1100; hence |( Base_FinSeq(K,m,i),Base_FinSeq(K,m,i) )| = (Base_FinSeq(K,m,i)).i by A0,AA2627 .=1.K by AA1110,A0; end; theorem AA3000: for a being Element of K,P,Q being Matrix of n,K st n>0 & a<>0.K & P*(1,1)= a" & (for i st 10 & a<>0.K & P*(1,1)= a" & (for i st 11; thus (a*(Base_FinSeq(K,n,1))).k= a*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,B92,A13 .= a*(0.K) by A13,AA1120,B1,C0,A13a .= 0.K by VECTSP_1:36; end; B6: now assume C0: k=1; thus (a*(Base_FinSeq(K,n,1))).k=a*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,B92,A13 .= a*(1.K) by AA1110,C0,B1,A13 .= a by VECTSP_1:def 16; end; now assume B20: k<>1;then B19: 1 j; (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j)))*((Base_FinSeq(K,n,1))/.k) by C4,FINSEQ_4:24,B4,C0 .=(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1 .= 0.K by VECTSP_1:36;then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by BB120,B4,B5b,C0 .= (Base_FinSeq(K,n,j))/.k by RLVECT_1:10 .= (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; hence p.k=q.k by D2,AA1120,B1,C0,E0; end; suppose E0: k=j; (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j)))*((Base_FinSeq(K,n,1))/.k) by C4,FINSEQ_4:24,B4,C0 .=(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1 .= 0.K by VECTSP_1:36;then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by BB120,B4,B5b,C0 .= (Base_FinSeq(K,n,j))/.k by RLVECT_1:10 .= (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by AA1110,C0,E0; hence p.k=q.k by D2,AA1110,C0,E0; end; end; hence p.k=q.k; end; end;then B7: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; A2a: len P=n & width P=n by MATRIX_1:25; K2: len Line(P,1) = n by MATRIX_1:def 8,A2a; K3: (Line(P,1))/.j = ( Line(P,1)).j by FINSEQ_4:24,K2,B1 .= P*(1,j) by MATRIX_1:def 8,B20,A2a; K0: (Line(P,1))/.1 = (Line(P,1)).1 by FINSEQ_4:24,K2,A4 .=a" by A1,MATRIX_1:def 8,A10; (P*Q)*(1,j)= |( Line(P,1), Col(Q,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(P,1), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,1), Base_FinSeq(K,n,j) )| by BB248,B4,A2,B7,B5b .= |( Line(P,1), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P,1), Base_FinSeq(K,n,j) )| by BB200 .=(-a*(P*(1,j)))* |( Line(P,1), (Base_FinSeq(K,n,1)) )| +|( Line(P,1), Base_FinSeq(K,n,j) )| by BB246,A2,A2b .=(-a*(P*(1,j)))* (a") +|( Line(P,1), Base_FinSeq(K,n,j) )| by K0,AA2627,A2,A4 .= -(a*(P*(1,j)))* (a") +|( Line(P,1), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((P*(1,j))*(a* (a"))) +|( Line(P,1), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -((P*(1,j))*(1_K)) +|( Line(P,1), Base_FinSeq(K,n,j) )| by VECTSP_1:def 22,A1 .= -(P*(1,j)*(1.K)) + (Line(P,1))/.j by AA2627,B1,A2 .= -(P*(1,j)) + P*(1,j) by K3,VECTSP_1:def 16 .= 0.K by RLVECT_1:16; hence (P*Q)*(1,j)= 0.K; end; A15: for i,j st 1j holds (P*Q)*(i,j)= 0.K proof let i,j; assume B1: 1j;then B20: i in Seg n & j in Seg n by FINSEQ_1:3; B2: [i,j] in Indices P by B1,MATRIX_1:38; A22: [i,j] in Indices (P*Q) by B1,MATRIX_1:38; A23b: [i,1] in Indices P by B1,MATRIX_1:38,A40; B3: len (Col(Q,j))=len Q by MATRIX_1:def 9 .=n by MATRIX_1:25; B4: len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) =len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) by BB200 .=len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .=n by AA1100; B5b: len (Base_FinSeq(K,n,j))=n by AA1100;then B5: len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by B4,Th6; B4b: len (a*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .=n by AA1100; now per cases; suppose F0: j>1; reconsider p=Col(Q,j),q=-a*(P*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(K,n,j) as FinSequence of K; for k be Nat st 1 <=k & k <= n holds p.k=q.k proof let k be Nat; assume C0: 1 <=k & k <= n; C10a: len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .=n by AA1100; B92b: k in dom ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) by C0,FINSEQ_3:27,C10a; C12: k in dom Q by C0,FINSEQ_3:27,A2d; C2: p.k=Q*(k,j) by MATRIX_1:def 9,C12; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; C4: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))).k by BB200 .=(-a*(P*(1,j)))*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,B92b,A13; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; per cases by C0,REAL_1:def 5; suppose D0: 1=k; K3: 1 <= k & k <= len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) by C0,C10a,BB200; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by D0,B1,AA1120,C0,F0; K2: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k = (-a*(P*(1,j)))*((Base_FinSeq(K,n,1))/.k) by C4,FINSEQ_4:24,K3 .= (-a*(P*(1,j)))*(1.K) by D0,AA1110,A4,E1; q.k= (-a*(P*(1,j)))*(1.K)+ 0.K by BB120,B4,B5b,C0,K2,K1 .= (-a*(P*(1,j)))*(1_K) by RLVECT_1:10 .= (-a*(P*(1,j))) by GROUP_1:def 5; hence p.k=q.k by A1,B1,F0,C2,D0; end; suppose D0: 1 j; E4: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; K1: (Base_FinSeq(K,n,j))/.k =(Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; K2: q.k = (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k +0.K by BB120,B4,B5b,C0,K1; q.k = (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k by RLVECT_1:10,K2 .= (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,K3; hence p.k=q.k by D2,AA1120,B1,C0,E0,E4; end; suppose E0: k=j;then E2: p.k=1.K by D2,AA1110,C0; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by AA1110,C0,E0; K2: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,A13,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 1.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; end; hence p.k=q.k; end; end;then B7: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; A2a: len P=n & width P=n by MATRIX_1:25; K2: len Line(P,i) = n by MATRIX_1:def 8,A2a; K3: (Line(P,i))/.j = (Line(P,i)).j by FINSEQ_4:24,K2,B1 .= P*(i,j) by MATRIX_1:def 8,B20,A2a; K0: (Line(P,i))/.1 = (Line(P,i)).1 by FINSEQ_4:24,K2,A4 .= P*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(P,i), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB248,B4,K2,B7,B5b .= |( Line(P,i), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB200 .=(-a*(P*(1,j)))* |( Line(P,i), (Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB246,K2,A2b .=(-a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by K0,AA2627,K2,A4 .= -(a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((P*(1,j))*(a* (P*(i,1)))) +|( Line(P,i), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -(P*(1,j))*(a* (P*(i,1))) + P*(i,j) by K3,AA2627,B1,K2; consider p1 being FinSequence of K such that A97: p1 = P.i & P*(i,j) = p1.j by MATRIX_1:def 6,B2; p1=Base_FinSeq(K,n,i) by A1,A97,B1;then A98: p1.j= 0.K by AA1120,B1; consider p2 being FinSequence of K such that A99: p2 = P.i & P*(i,1) = p2.1 by MATRIX_1:def 6,A23b; K2: p2=Base_FinSeq(K,n,i) by A1,A99,B1; (P*Q)*(i,j)= -(P*(1,j))*(a* (0.K)) + P*(i,j) by B28,A99,AA1120,B18,B1,K2 .= -(P*(1,j))*(0.K) + P*(i,j) by VECTSP_1:36 .= - (0.K) + P*(i,j) by VECTSP_1:36 .= 0.K + 0.K by A97,A98,RLVECT_1:25 .= 0.K by RLVECT_1:10; hence thesis; end; suppose F1: j<=1; reconsider p=Col(Q,j),q=a*(Base_FinSeq(K,n,1)) as FinSequence of K; F2: for k be Nat st 1 <=k & k <= n holds p.k=q.k proof let k be Nat; assume C0: 1 <=k & k <= n; B92: k in dom (a*(Base_FinSeq(K,n,1))) by A21,C0,FINSEQ_3:27; C12: k in dom Q by C0,FINSEQ_3:27,A2d; A2b: len (Base_FinSeq(K,n,1))=n by AA1100; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; C4: (a*(Base_FinSeq(K,n,1))).k =a*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,B92,A13; per cases by C0,REAL_1:def 5; suppose D0: 1=k; D2: p.k=Q*(1,j) by MATRIX_1:def 9,C12,D0 .=a by A1,F1,B1,XXREAL_0:1; q.k= (a)*(1.K) by C4,D0,AA1110,C0,A13 .=a by VECTSP_1:def 16; hence p.k=q.k by D2; end; suppose D0: 1 j; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; A13a: 1<=n by C0,XXREAL_0:2; a*(Base_FinSeq(K,n,1))/.k = a*(0.K) by A13,AA1120,D0,C0,A13a .= 0.K by VECTSP_1:36; hence p.k=q.k by E0,D2,AA1120,B1,C0,C4; end; suppose k=j; hence p.k=q.k by F1,D0; end; end; hence p.k=q.k; end; end; A2x: len (Line(P,i))=n by MATRIX_1:def 8,A2a; K0: (Line(P,i))/.1 = (Line(P,i)).1 by FINSEQ_4:24,A2x,A4 .= P*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(P,i), a*(Base_FinSeq(K,n,1)) )| by F2,B3,B4b,FINSEQ_1:18 .= a* |( Line(P,i), (Base_FinSeq(K,n,1)) )| by BB246,A2x,A2b .= a* (P*(i,1)) by K0,AA2627,A2x,A4; consider p2 being FinSequence of K such that A99: p2 = P.i & P*(i,1) = p2.1 by MATRIX_1:def 6,A23b; p2=Base_FinSeq(K,n,i) by A1,A99,B1; hence (P*Q)*(i,j)= a*(0.K) by B28,A99,AA1120,B18,B1 .=0.K by VECTSP_1:36; end; end; hence (P*Q)*(i,j)= 0.K; end; A85: for i,j st 1 j;then E2: p.k= 0.K by D2,AA1120,B1,C0; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; K2: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,A13,C4 .= 0.K by VECTSP_1:36; q.k=0.K + 0.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; suppose E0: k=j;then E2: p.k=1.K by D2,AA1110,C0; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by B1,AA1110,E0; K2: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K) by D0,AA1120,A4,C0,A13,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 1.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; end; hence p.k=q.k; end; end;then B7: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; A2a: len P=n & width P=n by MATRIX_1:25; K2: len Line(P,i) = n by MATRIX_1:def 8,A2a; K0: (Line(P,i))/.j = (Line(P,i)).j by FINSEQ_4:24,K2,B1 .= P*(i,j) by MATRIX_1:def 8,B20,A2a; K3: (Line(P,i))/.1 = (Line(P,i)).1 by FINSEQ_4:24,K2,A4 .= P*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(P,i), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB248,B4,K2,B7,B5b .= |( Line(P,i), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB200 .=(-a*(P*(1,j)))* |( Line(P,i), (Base_FinSeq(K,n,1)) )| +|( Line(P,i), Base_FinSeq(K,n,j) )| by BB246,K2,A2b .=(-a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by K3,AA2627,K2,A4 .= -(a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((P*(1,j))*(a* (P*(i,1)))) +|( Line(P,i), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -(P*(1,j))*(a* (P*(i,1))) + P*(i,j) by K0,AA2627,B1,K2; consider p1 being FinSequence of K such that A97: p1 = P.i & P*(i,j) = p1.j by MATRIX_1:def 6,B2; p1=Base_FinSeq(K,n,i) by A1,A97,B1;then A98: p1.j=1.K by AA1110,B1; consider p2 being FinSequence of K such that A99: p2 = P.i & P*(i,1) = p2.1 by MATRIX_1:def 6,A23b; p2=Base_FinSeq(K,n,i) by A1,A99,B1; hence (P*Q)*(i,j)= -(P*(1,j))*(a* (0.K)) + P*(i,j) by A99,B28,AA1120,B18,B1 .= -(P*(1,j))*((0.K)) + P*(i,j) by VECTSP_1:36 .= -((0.K)) + P*(i,j) by VECTSP_1:36 .= 0.K + 1.K by A97,A98,RLVECT_1:25 .= 1.K by RLVECT_1:10; end; for i,j being Nat st [i,j] in Indices (P*Q) holds (P*Q)*(i,j)=(1.(K,n))*(i,j) proof let i,j be Nat; assume [i,j] in Indices (P*Q);then B2: i in Seg n & j in Seg n by A18,ZFMISC_1:106;then B3: 1<=i & i<=n by FINSEQ_1:3; B4: 1<=j & j<=n by B2,FINSEQ_1:3; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; per cases by B3,REAL_1:def 5; suppose C0: 1j; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .= 0.K by AA1120,D0,B3,B4; thus (P*Q)*(i,j)=(P*Q)*(i0,j0) .=(1.(K,n))*(i,j) by D1,C0,B3,B4,A15,D0; end; suppose D0: i=j; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .=1.K by AA1110,D0,B4; thus (P*Q)*(i,j)=(P*Q)*(i0,j0) .=(1.(K,n))*(i,j) by D1,C0,B4,A85,D0; end; end; hence (P*Q)*(i,j)=(1.(K,n))*(i,j); end; suppose C0: 1=i; now per cases; suppose D0: i=j;then D0: i=j by B4,XXREAL_0:1,C0; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .=1.K by D0,AA1110,B4; thus (P*Q)*(i,j)=(1.(K,n))*(i,j) by D1,C0,A13,D9,B4,XXREAL_0:1; end; end; hence (P*Q)*(i,j)=(1.(K,n))*(i,j); end; end;then A5: P*Q=1.(K,n) by MATRIX_1:28; A2d: len P=n & width P=n by MATRIX_1:25; A2a: len Q=n & width Q=n by MATRIX_1:25; A2: len (Line(Q,1))=n by MATRIX_1:def 8,A2a; A2b: len (Base_FinSeq(K,n,1))=n by AA1100; A20: len (Col(P,1))=len P by MATRIX_1:def 9 .=n by MATRIX_1:25; A21: len ((a")*(Base_FinSeq(K,n,1)))=len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .= n by AA1100; for k be Nat st 1<=k & k<=n holds (Col(P,1)).k=((a")*(Base_FinSeq(K,n,1))).k proof let k be Nat; B: k in NAT by ORDINAL1:def 13; assume B1: 1<=k & k<=n;then B32: k in Seg n by FINSEQ_1:3;then B3: k in dom P by FINSEQ_1:def 3,A2d; B92: k in dom ((a")*(Base_FinSeq(K,n,1))) by A21,B1,FINSEQ_3:27; 1<=n by B1,XXREAL_0:2;then B11: 1 in dom P by FINSEQ_3:27,A2d; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by B1,FINSEQ_4:24,A2b; A13a: 1<=n by B1,XXREAL_0:2; B5: now assume C0: k<>1; thus ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,B92,A13 .= (a")*(0.K) by A13,AA1120,B1,C0,A13a .= 0.K by VECTSP_1:36; end; B6: now assume C0: k=1; k in dom ((a")*(Base_FinSeq(K,n,1))) by B32,FINSEQ_1:def 3,A21; hence ((a")*(Base_FinSeq(K,n,1))).k =(a")*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,A13 .=(a")*(1.K) by AA1110,C0,B1,A13 .= a" by VECTSP_1:def 16; end; now assume B20: k<>1;then B19: 1 j;then E2: p.k= 0.K by D2,AA1120,B1,C0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; K2: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 0.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; suppose E0: k=j;then E2: p.k=1.K by D2,AA1110,C0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,k))/.k = (Base_FinSeq(K,n,k)).k by FINSEQ_4:24,B5b,C0,E0 .= 1.K by B1,AA1110,E0; K2: (-(a")*(Q*(1,k))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,k))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0,E0; E3: (-(a")*(Q*(1,k))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,k)))*(0.K) by D0,AA1120,A4,C0,E1,C4,E0 .= 0.K by VECTSP_1:36; q.k= 0.K + 1.K by BB120,B4,B5b,C0,E3,K1,K2,E0; hence p.k=q.k by E2,RLVECT_1:10; end; end; hence p.k=q.k; end; end;then B7: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; K1: 1<=n by B1,XXREAL_0:2; B8: 1 in Seg width Q by FINSEQ_1:3,A2a,K1; K2: (Line(Q,1))/.1 = (Line(Q,1)).1 by FINSEQ_4:24,K1,A2 .= a by A1,MATRIX_1:def 8,B8; K2a: len Line(Q,1) = n by MATRIX_1:def 8,A2a; K3: (Line(Q,1))/.j = (Line(Q,1)).j by FINSEQ_4:24,K2a,B1; (Q*P)*(1,j)= |( Line(Q,1), Col(P,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(Q,1), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,1), Base_FinSeq(K,n,j) )| by BB248,B4,A2,B7,B5b .= |( Line(Q,1), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,1), Base_FinSeq(K,n,j) )| by BB200 .=(-(a")*(Q*(1,j)))* |( Line(Q,1), (Base_FinSeq(K,n,1)) )| +|( Line(Q,1), Base_FinSeq(K,n,j) )| by BB246,A2,A2b .=(-(a")*(Q*(1,j)))* a +|( Line(Q,1), Base_FinSeq(K,n,j) )| by K2,AA2627,A2,A4 .= -((a")*(Q*(1,j)))* a +|( Line(Q,1), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((Q*(1,j))*((a")* a)) +|( Line(Q,1), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -((Q*(1,j))*(1.K)) +|( Line(Q,1), Base_FinSeq(K,n,j) )| by VECTSP_1:def 22,A1 .= -((Q*(1,j))*(1.K)) + ( Line(Q,1))/.j by AA2627,A2,B1 .= -(Q*(1,j)) + ( Line(Q,1))/.j by VECTSP_1:def 16 .= -(Q*(1,j)) + Q*(1,j) by MATRIX_1:def 8,A2a,B20,K3 .= 0.K by RLVECT_1:16; hence (Q*P)*(1,j)= 0.K; end; A15: for i,j st 1j holds (Q*P)*(i,j)= 0.K proof let i,j; assume B1: 1j;then B20: i in Seg n & j in Seg n by FINSEQ_1:3; B2: [i,j] in Indices Q by B1,MATRIX_1:38; A22: [i,j] in Indices (Q*P) by B1,MATRIX_1:38; A23b: [i,1] in Indices Q by B1,MATRIX_1:38,A4; B3: len (Col(P,j))=len P by MATRIX_1:def 9 .=n by MATRIX_1:25; B4: len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))) =len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) by BB200 .=len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .=n by AA1100; B4d: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)) by MATRIXR1:16 .=n by AA1100; B5b: len (Base_FinSeq(K,n,j))=n by AA1100;then B5: len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by B4,Th6; B4b: len ((a")*(Base_FinSeq(K,n,1))) =len Base_FinSeq(K,n,1) by MATRIXR1:16 .=n by AA1100; now per cases; suppose F0: j>1; reconsider p=Col(P,j),q=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(K,n,j) as FinSequence of K; for k be Nat st 1 <=k & k <= n holds p.k=q.k proof let k be Nat; assume C0: 1 <=k & k <= n;then k in Seg n by FINSEQ_1:3;then C10b: k in dom ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) by B4d,FINSEQ_1:def 3; C12: k in dom P by C0,FINSEQ_3:27,A2d; C2: p.k=P*(k,j) by MATRIX_1:def 9,C12; A2b: len (Base_FinSeq(K,n,1))=n by AA1100; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; C4: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))).k by BB200 .=(-(a")*(Q*(1,j)))*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,C10b,A13; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; per cases by C0,REAL_1:def 5; suppose D0: 1=k; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by D0,B1,AA1120,C0,F0; K2: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; D1:(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*(1.K) by D0,AA1110,A4,A13,C4; q.k= (-(a")*(Q*(1,j)))*(1.K)+ 0.K by BB120,B4,B5b,C0,D1,K1,K2 .= (-(a")*(Q*(1,j)))*(1.K) by RLVECT_1:10 .=-(a")*(Q*(1,j)) by VECTSP_1:def 16; hence p.k=q.k by A1b,B1,F0,C2,D0; end; suppose D0: 1 j; (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j)))*((Base_FinSeq(K,n,1))/.k) by C4,FINSEQ_4:24,B4,C0 .=(-(a")*(Q*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1 .= 0.K by VECTSP_1:36;then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by BB120,B4,B5b,C0 .= (Base_FinSeq(K,n,j))/.k by RLVECT_1:10 .= (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; hence p.k=q.k by D2,AA1120,B1,C0,E0; end; suppose E0: k=j; (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j)))*((Base_FinSeq(K,n,1))/.k) by C4,FINSEQ_4:24,B4,C0 .=(-(a")*(Q*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1 .= 0.K by VECTSP_1:36;then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by BB120,B4,B5b,C0 .= (Base_FinSeq(K,n,j))/.k by RLVECT_1:10 .= (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by B1,AA1110,E0; hence p.k=q.k by D2,AA1110,C0,E0; end; end; hence p.k=q.k; end; end;then B7: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; A2a: len Q=n & width Q=n by MATRIX_1:25; K2: len Line(Q,i) = n by MATRIX_1:def 8,A2a; K3: (Line(Q,i))/.j = ( Line(Q,i)).j by FINSEQ_4:24,K2,B1 .= Q*(i,j) by MATRIX_1:def 8,B20,A2a; K0: (Line(Q,i))/.1 = (Line(Q,i)).1 by FINSEQ_4:24,K2,A4 .= Q*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(Q,i), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB248,B4,K2,B7,B5b .= |( Line(Q,i), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB200 .=(-(a")*(Q*(1,j)))* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB246,K2,A2b .=(-(a")*(Q*(1,j)))* (Q*(i,1)) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by K0,AA2627,K2,A4 .= -((Q*(1,j))*(a")* (Q*(i,1))) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((Q*(1,j))*((a")* (Q*(i,1)))) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -(Q*(1,j))*((a")* (Q*(i,1))) + Q*(i,j) by K3,AA2627,B1,K2; consider p1 being FinSequence of K such that A97: p1 = Q.i & Q*(i,j) = p1.j by MATRIX_1:def 6,B2; p1=Base_FinSeq(K,n,i) by A1,A97,B1;then A98: p1.j= 0.K by AA1120,B1; consider p2 being FinSequence of K such that A99: p2 = Q.i & Q*(i,1) = p2.1 by MATRIX_1:def 6,A23b; p2=Base_FinSeq(K,n,i) by A1,A99,B1; hence (Q*P)*(i,j) = -(Q*(1,j))*((a")* (0.K)) + Q*(i,j) by B28,A99,AA1120,B18,B1 .= -(Q*(1,j))*((0.K)) + Q*(i,j) by VECTSP_1:36 .= -(0.K) + Q*(i,j) by VECTSP_1:36 .= 0.K + 0.K by A97,A98,RLVECT_1:25 .= 0.K by RLVECT_1:10; end; suppose F1: j<=1; reconsider p=Col(P,j),q=a"*(Base_FinSeq(K,n,1)) as FinSequence of K; F2: for k be Nat st 1 <=k & k <= n holds p.k=q.k proof let k be Nat; assume C0: 1 <=k & k <= n;then C10: k in Seg n by FINSEQ_1:3;then C10b: k in dom ((a")*(Base_FinSeq(K,n,1))) by B4b,FINSEQ_1:def 3; A2b: len (Base_FinSeq(K,n,1))=n by AA1100; C12: k in dom P by C0,FINSEQ_3:27,A2d; C2: p.k=P*(k,j) by MATRIX_1:def 9,C12; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; C4: ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,C10b,A13; per cases by C0,REAL_1:def 5; suppose D0: 1=k; q.k= (a")*(1.K) by C4,D0,AA1110,C0,A13 .=a" by VECTSP_1:def 16; hence p.k=q.k by A1,F1,B1,XXREAL_0:1,C2,D0; end; suppose D0: 1 j; A13: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A2b; A13a: 1<=n by C0,XXREAL_0:2; (a")*(Base_FinSeq(K,n,1))/.k = a"*(0.K) by A13,AA1120,D0,C0,A13a .= 0.K by VECTSP_1:36; hence p.k=q.k by E0,D2,AA1120,B1,C0,C4; end; suppose k=j; hence p.k=q.k by F1,D0; end; end; hence p.k=q.k; end; end; A2a: len Q=n & width Q=n by MATRIX_1:25; K2: len Line(Q,i) = n by MATRIX_1:def 8,A2a; K0: (Line(Q,i))/.1 = (Line(Q,i)).1 by FINSEQ_4:24,K2,A4 .= Q*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(Q,i), a"*(Base_FinSeq(K,n,1)) )| by F2,B3,B4b,FINSEQ_1:18 .= a"* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| by BB246,K2,A2b .= a"* (Q*(i,1)) by K0,AA2627,K2,A4; consider p2 being FinSequence of K such that A99: p2 = Q.i & Q*(i,1) = p2.1 by MATRIX_1:def 6,A23b; p2=Base_FinSeq(K,n,i) by A1,A99,B1; hence (Q*P)*(i,j)=a"* (0.K) by B28,A99,AA1120,B18,B1 .= 0.K by VECTSP_1:36; end; end; hence (Q*P)*(i,j)= 0.K; end; A85: for i,j st 1 j;then E2: p.k= 0.K by D2,AA1120,B1,C0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; K2: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 0.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; suppose E0: k=j;then E2: p.k=1.K by D2,AA1110,C0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by AA1110,C0,E0; K2: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 1.K by BB120,B4,B5b,C0,E3,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; end; hence p.k=q.k; end; end;then B7: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; K2: len Line(Q,i)=n by MATRIX_1:def 8,A2a; A2a: len Q=n & width Q=n by MATRIX_1:25; K3: (Line(Q,i))/.j = (Line(Q,i)).j by FINSEQ_4:24,K2,B1 .= Q*(i,j) by MATRIX_1:def 8,B20,A2a; K0: (Line(Q,i))/.1 = (Line(Q,i)).1 by FINSEQ_4:24,K2,A4 .= Q*(i,1) by MATRIX_1:def 8,A10; B18: 1<=n by XXREAL_0:2,B1; B28: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(Q,i), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB248,B4,K2,B7,B5b .= |( Line(Q,i), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB200 .=(-(a")*(Q*(1,j)))* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| +|( Line(Q,i), Base_FinSeq(K,n,j) )| by BB246,K2,A2b .=(-(a")*(Q*(1,j)))* (Q*(i,1)) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by K0,AA2627,K2,A4 .= -((Q*(1,j))*(a")* (Q*(i,1))) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((Q*(1,j))*((a")* (Q*(i,1)))) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -(Q*(1,j))*((a")* (Q*(i,1))) + Q*(i,j) by K3,AA2627,B1,K2; consider p1 being FinSequence of K such that A97: p1 = Q.i & Q*(i,j) = p1.j by MATRIX_1:def 6,B2; p1=Base_FinSeq(K,n,i) by A1,A97,B1;then A98: p1.j=1.K by AA1110,B1; consider p2 being FinSequence of K such that A99: p2 = Q.i & Q*(i,1) = p2.1 by MATRIX_1:def 6,A23b; p2=Base_FinSeq(K,n,i) by A1,A99,B1; hence (Q*P)*(i,j)= -(Q*(1,j))*((a")* ( 0.K)) + Q*(i,j) by B28,A99,AA1120,B18,B1 .= -(Q*(1,j))*(( 0.K)) + Q*(i,j) by VECTSP_1:36 .= -(0.K) + Q*(i,j) by VECTSP_1:36 .= (0.K) + 1.K by A97,A98,RLVECT_1:25 .= 1.K by RLVECT_1:10; end; KK1: for i,j being Nat st [i,j] in Indices (Q*P) holds (Q*P)*(i,j)=(1.(K,n))*(i,j) proof let i,j be Nat; assume [i,j] in Indices (Q*P);then B2: i in Seg n & j in Seg n by A18,ZFMISC_1:106;then B3: 1<=i & i<=n by FINSEQ_1:3; B4: 1<=j & j<=n by B2,FINSEQ_1:3; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; per cases by B3,REAL_1:def 5; suppose C0: 1j; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .= 0.K by AA1120,D0,B3,B4; thus (Q*P)*(i,j)=(Q*P)*(i0,j0) .=(1.(K,n))*(i,j) by D1,C0,B3,B4,A15,D0; end; suppose D0: i=j; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .=1.K by AA1110,D0,B4; thus (Q*P)*(i,j)=(Q*P)*(i0,j0) .=(1.(K,n))*(i,j) by D1,C0,B4,A85,D0; end; end; hence (Q*P)*(i,j)=(1.(K,n))*(i,j); end; suppose C0: 1=i; now per cases; suppose D0: i=j;then D0: i=j by B4,XXREAL_0:1,C0; D1: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by BB300,B3,B4 .=1.K by D0,AA1110,B4; thus (Q*P)*(i,j)=(1.(K,n))*(i,j) by D1,C0,A13,D9,B4,XXREAL_0:1; end; end; hence (Q*P)*(i,j)=(1.(K,n))*(i,j); end; end; A25: Q*P=1.(K,n) by MATRIX_1:28,KK1; hence P is invertible by AA4145,A5; thus Q= P~ by AA4140,A5,A25; end; theorem AA3010: for a being Element of K,P being Matrix of n,K st n>0 & a<>0.K & P*(1,1)= a" & (for i st 10 & a<>0.K & P*(1,1)= a" & (for i st 11 implies $3=- a*( P*(1,$2) )))) & ($1 <>1 implies for i0 being Element of NAT st i0=$1 holds $3= (Base_FinSeq(K,n,i0)).$2); A5: for i,j being Nat st [i,j] in [:Seg n, Seg n:] for x1,x2 being Element of K st P[i,j,x1] & P[i,j,x2] holds x1 = x2 proof let i,j be Nat; assume [i,j] in [:Seg n, Seg n:]; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; thus for x1,x2 being Element of K st P[i,j,x1] & P[i,j,x2] holds x1 = x2 proof let x1,x2 be Element of K; assume B1: P[i,j,x1] & P[i,j,x2]; per cases; suppose C0: i=1; thus x1 = x2 by C0,B1; end; suppose i<>1; then x1= (Base_FinSeq(K,n,i0)).j & x2= (Base_FinSeq(K,n,i0)).j by B1; hence x1 = x2; end; end; end; A6: for i,j being Nat st [i,j] in [:Seg n, Seg n:] ex x being Element of K st P[i,j,x] proof let i,j be Nat; assume B1: [i,j] in [:Seg n, Seg n:]; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; i0 in Seg n & j0 in Seg n by B1,ZFMISC_1:106;then B1b: 1<=i0 & i0 <=n & 1<=j0 & j0<=n by FINSEQ_1:3; per cases; suppose C0: i=1; now per cases; case D0: j=1; set x1=a; thus (i=1 implies ((j=1 implies x1=a)& (j<>1 implies x1=- a*(P*(1,j) )))) & (i <>1 implies for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq(K,n,i1)).j) by C0,D0; end; case D0: j<>1; set x1= -(a)*( P*(1,j) ); thus (i=1 implies ((j=1 implies x1=a)& (j<>1 implies x1=- a*(P*(1,j))))) & (i <>1 implies for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq(K,n,i1)).j) by C0,D0; end; end; hence ex x being Element of K st (i=1 implies ((j=1 implies x=a)& (j<>1 implies x=- a*( P*(1,j) )))) & (i <>1 implies for i1 being Element of NAT st i1=i holds x= (Base_FinSeq(K,n,i1)).j); end; suppose C0: i<>1; len (Base_FinSeq(K,n,i0))=n by AA1100;then (Base_FinSeq(K,n,i0))/.j0= (Base_FinSeq(K,n,i0)).j0 by B1b,FINSEQ_4:24;then reconsider x1= (Base_FinSeq(K,n,i0)).j0 as Element of K; (i=1 implies ((j=1 implies x1=a)& (j<>1 implies x1=- a*( P*(1,j) )))) & (i <>1 implies for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq(K,n,i1)).j) by C0; hence ex x being Element of K st (i=1 implies ((j=1 implies x=a)& (j<>1 implies x=- a*( P*(1,j) )))) & (i <>1 implies for i1 being Element of NAT st i1=i holds x= (Base_FinSeq(K,n,i1)).j); end; end; consider Q0 being Matrix of n,n,K such that A7: for i,j being Nat st [i,j] in Indices Q0 holds P[i,j,Q0*(i,j)] from MATRIX_1:sch 2(A5,A6); A70: Indices Q0=[:Seg n,Seg n:] by MATRIX_1:25; A70a: 0+1<=n by A1,NAT_1:13; A30: 1 in Seg n by FINSEQ_1:3,A70a; A30a: [1,1] in Indices Q0 by A70a,MATRIX_1:38; A10: Q0*(1,1)=a by A7,A30a; A11: for j st 10 & A*(1,1)<>0.K ex P being Matrix of n,K st P is invertible & (A*P)*(1,1)=1.K & (for j st 10 & A*(1,1)<>0.K; set a=A*(1,1); defpred P[Nat,Nat,Element of K] means ($1=1 implies (($2=1 implies $3=a")& ($2<>1 implies $3=- (a")*( A*(1,$2) )))) & ($1 <>1 implies for i0 being Element of NAT st i0=$1 holds $3= (Base_FinSeq(K,n,i0)).$2); A5: for i,j being Nat st [i,j] in [:Seg n, Seg n:] for x1,x2 being Element of K st P[i,j,x1] & P[i,j,x2] holds x1 = x2 proof let i,j be Nat; assume [i,j] in [:Seg n, Seg n:]; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; let x1,x2 be Element of K; assume B1: P[i,j,x1] & P[i,j,x2]; per cases; suppose i=1; hence x1 = x2 by B1; end; suppose i<>1; then x1= (Base_FinSeq(K,n,i0)).j & x2= (Base_FinSeq(K,n,i0)).j by B1; hence x1 = x2; end; end; A6: for i,j being Nat st [i,j] in [:Seg n, Seg n:] ex x being Element of K st P[i,j,x] proof let i,j be Nat; assume B1: [i,j] in [:Seg n, Seg n:]; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; B1a: i0 in Seg n & j0 in Seg n by B1,ZFMISC_1:106; B1b: 1<=i0 & i0 <=n & 1<=j0 & j0<=n by FINSEQ_1:3,B1a; per cases; suppose C0: i=1; per cases; suppose D0: j=1; set x1=a"; thus ex x being Element of K st P[i,j,x] by C0,D0; end; suppose D0: j<>1; set x1= -(a")*( A*(1,j) ); thus ex x being Element of K st P[i,j,x] by C0,D0; end; end; suppose C0: i<>1; set x1= (Base_FinSeq(K,n,i0))/.j0; C7: len (Base_FinSeq(K,n,i0))=n by AA1100; for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq(K,n,i1)).j by B1b,FINSEQ_4:24,C7; hence ex x being Element of K st P[i,j,x] by C0; end; end; consider P0 being Matrix of n,n,K such that A7: for i,j being Nat st [i,j] in Indices P0 holds P[i,j,P0*(i,j)] from MATRIX_1:sch 2(A5,A6); A40: 0+1<=n by A1,NAT_1:13; A72a: [1,1] in Indices P0 by A40,MATRIX_1:38; A12: P0*(1,1)= a" by A7,A72a; A91: for i st 11; thus ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by FVSUM_1:62,C10d,A13 .= (a")*(0.K) by A13,AA1120,B1,C0,A13a .= 0.K by VECTSP_1:36; end; B6: now assume C0: k=1; thus ((a")*(Base_FinSeq(K,n,1))).k =(a")*((Base_FinSeq(K,n,1))/.1) by C10d,FVSUM_1:62,A13,C0 .=(a")*(1.K) by AA1110,C0,B1,A13 .= a" by VECTSP_1:def 16; end; now assume B20: k<>1; B: k in NAT by ORDINAL1:def 13; B19: 1 j;then E2: p.k= 0.K by D2,AA1120,B1,C0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 0.K by B1,AA1120,C0,E0; K2: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(A*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 0.K by E3,BB120,B4,B5b,C0,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; suppose E0: k=j; E2: p.k=1.K by D2,AA1110,C0,E0; A3a: len (Base_FinSeq(K,n,1))=n by AA1100; E1: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by C0,FINSEQ_4:24,A3a; K1: (Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by FINSEQ_4:24,B5b,C0 .= 1.K by AA1110,C0,E0; K2: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k by FINSEQ_4:24,B4,C0; E3: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(A*(1,j)))*(0.K) by D0,AA1120,A4,C0,E1,C4 .= 0.K by VECTSP_1:36; q.k= 0.K + 1.K by BB120,B4,B5b,C0,E3,K1,K2; hence p.k=q.k by E2,RLVECT_1:10; end; end; end;then B7: Col(P0,j)=-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by B3,B5,FINSEQ_1:18; A2a: len A=n & width A=n by MATRIX_1:25; K2: len Line(A,1) = n by MATRIX_1:def 8,A2a; K3: (Line(A,1))/.j = (Line(A,1)).j by FINSEQ_4:24,K2,B1 .= A*(1,j) by MATRIX_1:def 8,B20,A2a; K0: (Line(A,1))/.1 = (Line(A,1)).1 by FINSEQ_4:24,K2,A4 .= a by MATRIX_1:def 8,A10; (A*P0)*(1,j)= |( Line(A,1), Col(P0,j) )| by MATRIX_3:def 4,A2a,A2d,A22 .= |( Line(A,1), -(a")*(A*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(A,1), Base_FinSeq(K,n,j) )| by BB248,B4,A2,B7,B5b .= |( Line(A,1), (-(a")*(A*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(A,1), Base_FinSeq(K,n,j) )| by BB200 .=(-(a")*(A*(1,j)))* |( Line(A,1), (Base_FinSeq(K,n,1)) )| +|( Line(A,1), Base_FinSeq(K,n,j) )| by BB246,A2,A2b .=(-(a")*(A*(1,j)))* a +|( Line(A,1), Base_FinSeq(K,n,j) )| by K0,AA2627,A2,A4 .= -((a")*(A*(1,j)))* a +|( Line(A,1), Base_FinSeq(K,n,j) )| by VECTSP_1:41 .= -((A*(1,j))*((a")* a)) +|( Line(A,1), Base_FinSeq(K,n,j) )| by GROUP_1:def 4 .= -((A*(1,j))*(1.K)) +|( Line(A,1), Base_FinSeq(K,n,j) )| by VECTSP_1:def 22,A1 .= -((A*(1,j))*(1.K)) +( Line(A,1))/.j by AA2627,B1,A2 .= -(A*(1,j)) + A*(1,j) by K3,VECTSP_1:def 16 .= 0.K by RLVECT_1:16; hence (A*P0)*(1,j)= 0.K; end; for i st 10 & A*(1,1)<>0.K ex P being Matrix of n,K st P is invertible & (P*A)*(1,1)=1.K & (for i st 10 & A*(1,1)<>0.K; set B=A@; X: 0+1<=n by A1,NAT_1:13; [1,1] in Indices A by X,MATRIX_1:38;then A5: B*(1,1)=A*(1,1) by MATRIX_1:def 7; consider P0 being Matrix of n,K such that A6: P0 is invertible & (B*P0)*(1,1)=1.K & (for i st 10 & A*(1,1)<>0.K ex P,Q being Matrix of n,K st P is invertible & Q is invertible & (P*A*Q)*(1,1)=1.K & (for i st 10 & A*(1,1)<>0.K;then consider P being Matrix of n,K such that A3: P is invertible & (P*A)*(1,1)=1.K & (for i st 1 Matrix of n,K equals Swap(1.(K,n),1,i0); correctness proof i0 in NAT by ORDINAL1:def 13; hence thesis by AA330; end; end; theorem XA: for n being Element of NAT,i0 being Nat,A being Matrix of n,K st 1<=i0 & i0<=n & A= SwapDiagonal(K,n,i0) holds for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i0<>1 implies (i=1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=1 implies A*(i,j)=1.K)& (i=1 & j=1 implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K))) proof let n be Element of NAT,i0 be Nat,A be Matrix of n,K; assume A0: 1<=i0 & i0<=n; assume A1: A= SwapDiagonal(K,n,i0); B44: len A=n & width A=n & Indices A=[: Seg n,Seg n :] by MATRIX_1:25; let i,j be Nat; assume B1: 1<=i & i<=n & 1<=j & j<=n; B2: [i,j] in Indices A by B1,MATRIX_1:38; B77: 1<=n by B1,XXREAL_0:2; assume C1: i0<>1; thus i=1 & j=i0 implies A*(i,j)=1.K proof assume D0: i=1 & j=i0;then D1: 1)^h) = len (<*f/.i0*>)+len (h) by FINSEQ_1:35 .= 1+len (h) by FINSEQ_1:56;then D7: 1<= len ((<*f/.i0*>)^h) by NAT_1:11; D8: 1= len (<*f/.i0*>) by FINSEQ_1:56; D28: A.i=((<*f/.i0*>)^h^<*f/.1*>^(f/^i0)).i by D0,D1,B1,D20,FINSEQ_7:30,A1 .= ((<*f/.i0*>)^h^(<*f/.1*>^(f/^i0))).i by FINSEQ_1:45 .= (<*f/.i0*>^h).1 by D0,FINSEQ_1:85,D7 .= (<*f/.i0*>).1 by FINSEQ_1:85,D8 .= f/.i0 by FINSEQ_1:def 8; reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; 1 <= i0 & i0 <= len f by D0,B1,MATRIX_1:def 3;then f/.i0=f.i0 by FINSEQ_4:24.=Base_FinSeq(K,n,i0) by AA1200,D0,B1;then qq.j=1.K by D0,B1,AA1110; hence A*(i,j)=1.K by D28,B2,MATRIX_1:def 6; end; thus i=i0 & j=1 implies A*(i,j)=1.K proof assume D0: i=i0 & j=1; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.1 by B1,D20,A1,FINSEQ_7:33,D0; reconsider qq=(f/.1) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.1=f.1 by B77,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,1) by B77,AA1200;then qq.j=1.K by D0,B1,AA1110; hence A*(i,j)=1.K by D28,B2,MATRIX_1:def 6; end; thus i=1 & j=1 implies A*(i,j)=0.K proof assume D0: i=1 & j=1; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i0 by A0,D20,B1,A1,FINSEQ_7:33,D0; reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.i0=f.i0 by A0,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,i0) by AA1200,A0;then qq.j=0.K by D0,B1,C1,AA1120,A0; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; thus i=i0 & j=i0 implies A*(i,j)=0.K proof assume D0: i=i0 & j=i0; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.1 by B1,D20,B77,A1,FINSEQ_7:33,D0; reconsider qq=(f/.1) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.1=f.1 by B77,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,1) by B77,AA1200;then qq.j=0.K by D0,C1,AA1120,A0,B77; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; assume E0: not ((i=1 or i=i0) &(j=1 or j=i0)); per cases by E0; suppose E1: i<>1 & i<>i0; thus i=j implies A*(i,j)=1.K proof assume D0: i=j; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i by B1,D20,A1,FINSEQ_7:32,E1; reconsider qq=(f/.i) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; 1 <= j & j <= len f by B1,MATRIX_1:def 3;then f/.i=f.i by D0,FINSEQ_4:24 .=Base_FinSeq(K,n,i) by AA1200,B1;then qq.j=1.K by D0,B1,AA1110; hence A*(i,j)=1.K by D28,B2,MATRIX_1:def 6; end; thus i<>j implies A*(i,j)=0.K proof assume D0: i<>j; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i by B1,D20,A1,FINSEQ_7:32,E1; reconsider qq=(f/.i) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.i=f.i by B1,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,i) by AA1200,B1;then qq.j=0.K by D0,AA1120,B1; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; end; suppose F0: j<>1 & j<>i0; thus i=j implies A*(i,j)=1.K proof assume D0: i=j; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i by B1,D20,A1,FINSEQ_7:32,D0,F0; reconsider qq=(f/.i) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; 1 <= j & j <= len f by B1,MATRIX_1:def 3;then f/.i=f.i by D0,FINSEQ_4:24 .=Base_FinSeq(K,n,i) by AA1200,B1;then qq.j=1.K by D0,B1,AA1110; hence A*(i,j)=1.K by D28,B2,MATRIX_1:def 6; end; thus i<>j implies A*(i,j)=0.K proof assume D0: i<>j; per cases; suppose G0: not(i=1 or i=i0); reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i by B1,D20,A1,FINSEQ_7:32,G0; reconsider qq=(f/.i) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.i=f.i by B1,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,i) by AA1200,B1;then qq.j=0.K by D0,AA1120,B1; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; suppose G0: i=1 or i=i0; per cases by G0; suppose H0: i=1; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.i0 by A0,D20,B1,A1,FINSEQ_7:33,H0; reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.i0=f.i0 by A0,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,i0) by AA1200,A0;then qq.j=0.K by AA1120,A0,B1,F0; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; suppose H0: i=i0; reconsider f=1.(K,n) as FinSequence of (the carrier of K)*; D20: len f=n by MATRIX_1:def 3; reconsider g=f/^1 as FinSequence of (the carrier of K)*; reconsider j0=i0-'2 as Element of NAT; reconsider h= (g|j0) as FinSequence of (the carrier of K)*; D28: A.i=A/.i by FINSEQ_4:24,B44,B1 .=f/.1 by B1,D20,B77,A1,FINSEQ_7:33,H0; reconsider qq=(f/.1) as FinSequence of (the carrier of K) by FINSEQ_1:def 11; f/.1=f.1 by B77,D20,FINSEQ_4:24 .=Base_FinSeq(K,n,1) by B77,AA1200;then qq.j=0.K by AA1120,B77,B1,F0; hence A*(i,j)=0.K by D28,B2,MATRIX_1:def 6; end; end; end; end; end; theorem XB: for n being Element of NAT, A being Matrix of n,K for i being Nat st 1<=i & i<=n holds SwapDiagonal(K,n,1)*(i,i)=1.K proof let n be Element of NAT, A be Matrix of n,K; set A= SwapDiagonal(K,n,1); let i be Nat; assume X: 1<=i & i<=n ; C2: A=1.(K,n) by FINSEQ_7:21; [i,i] in Indices A by X,MATRIX_1:38; hence A*(i,i)=1.K by MATRIX_1:def 12,C2; end; theorem XC: for n being Element of NAT, A being Matrix of n,K for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i<>j implies SwapDiagonal(K,n,1)*(i,j)=0.K) proof let n be Element of NAT, A be Matrix of n,K; set A= SwapDiagonal(K,n,1); let i,j be Nat; assume 1<=i & i<=n & 1<=j & j<=n;then B2: [i,j] in Indices A by MATRIX_1:38; C2: A=1.(K,n) by FINSEQ_7:21; thus i<>j implies A*(i,j)=0.K by MATRIX_1:def 12,B2,C2; end; theorem AA4000: for K for n,i0 being Element of NAT,A being Matrix of n,K st 1<=i0 & i0<=n & i0 = 1 & for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K) holds A= SwapDiagonal(K,n,i0) proof let K;let n,i0 be Element of NAT,A be Matrix of n,K; assume A0: 1<=i0 & i0<=n & i0 = 1; assume B0: for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K); for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (SwapDiagonal(K,n,i0))*(i,j) proof let i,j be Nat; assume C0: [i,j] in Indices A; len A = n & width A = n & Indices A = [:Seg n, Seg n:] by MATRIX_1:25;then i in Seg n & j in Seg n by C0,ZFMISC_1:106;then B1: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3;then (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K) by B0; hence A*(i,j) = (SwapDiagonal(K,n,i0))*(i,j) by XB,A0,B1,XC; end; hence A= SwapDiagonal(K,n,i0) by MATRIX_1:28; end; theorem AA400X: for K for n,i0 being Element of NAT,A being Matrix of n,K st 1<=i0 & i0<=n & i0 <> 1 & for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=1 implies A*(i,j)=1.K)& (i=1 & j=1 implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K)) holds A= SwapDiagonal(K,n,i0) proof let K;let n,i0 be Element of NAT,A be Matrix of n,K; assume A0: 1<=i0 & i0<=n & i0<>1; assume B0: for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds ( (i=1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=1 implies A*(i,j)=1.K)& (i=1 & j=1 implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K))); for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (SwapDiagonal(K,n,i0))*(i,j) proof let i,j be Nat; assume C0: [i,j] in Indices A; len A = n & width A = n & Indices A = [:Seg n, Seg n:] by MATRIX_1:25;then i in Seg n & j in Seg n by C0,ZFMISC_1:106;then B1: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3;then B2: (i=1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=1 implies A*(i,j)=1.K)& (i=1 & j=1 implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K)) by B0; (i=1 & j=i0 implies (SwapDiagonal(K,n,i0))*(i,j)=1.K)& (i=i0 & j=1 implies (SwapDiagonal(K,n,i0))*(i,j)=1.K)& (i=1 & j=1 implies (SwapDiagonal(K,n,i0))*(i,j)=0.K)& (i=i0 & j=i0 implies (SwapDiagonal(K,n,i0))*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies (SwapDiagonal(K,n,i0))*(i,j)=1.K)& (i<>j implies (SwapDiagonal(K,n,i0))*(i,j)=0.K)) by XA,A0,B1; hence A*(i,j) = (SwapDiagonal(K,n,i0))*(i,j) by B2; end; hence A= SwapDiagonal(K,n,i0) by MATRIX_1:28; end; theorem AA4100: for A being (Matrix of n,K),i0 being Element of NAT st 1<=i0 & i0 <=n holds (for j st 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i0,j)=A*(1,j) & ((SwapDiagonal(K,n,i0))*A)*(1,j)=A*(i0,j))& (for i,j st i<>1 & i<>i0 & 1<=i & i<=n & 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i,j)=A*(i,j)) proof let A be (Matrix of n,K),i0 be Element of NAT; assume A1: 1<=i0 & i0 <=n; thus for j st 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i0,j)=A*(1,j) & ((SwapDiagonal(K,n,i0))*A)*(1,j)=A*(i0,j) proof let j; assume B1: 1<=j & j<=n; B12: 1<=n by XXREAL_0:2,B1; B3: 1 in Seg n by FINSEQ_1:3,B12; B2: j in Seg n by FINSEQ_1:3,B1; set Q=(SwapDiagonal(K,n,i0)) ,P=A; B9: len (Q*P)=n & width (Q*P)=n & Indices (Q*P)=[: Seg n,Seg n :] by MATRIX_1:25; A2a: len Q=n & width Q=n & Indices Q=[: Seg n,Seg n :] by MATRIX_1:25; A2d: len P=n & width P=n & Indices P=[: Seg n,Seg n :] by MATRIX_1:25; A9: 1 in dom P by B3,FINSEQ_1:def 3,A2d; C1: 1<=n & 1<=i0 & i0<=n by XXREAL_0:2,A1; C1a: i0 in Seg n by FINSEQ_1:3,A1; A9b: i0 in dom P by FINSEQ_1:def 3,A2d,C1a; A6: Line(Q,1)=Base_FinSeq(K,n,i0) proof C2: len (Base_FinSeq(K,n,i0)) = n by AA1100 .= width Q by MATRIX_1:25; for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,i0)).j2 = Q*(1,j2) proof let j2 be Nat; assume j2 in Seg width Q;then D2: 1<=j2 & j2<=n by A2a,FINSEQ_1:3; reconsider j3=j2 as Element of NAT by ORDINAL1:def 13; now per cases; suppose D0: i0<>1; now per cases; suppose i0=1 & j2=i0; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by D0; end; suppose E0: i0=i0 & j2=1; (SwapDiagonal(K,n,i0))*(1,j3)=0.K by XA,D2,D0,E0,A1; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by C1,E0,AA1120,D0; end; suppose i0=1 & j2=1; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by D0; end; suppose E0: i0=i0 & j2=i0; (SwapDiagonal(K,n,i0))*(1,j3)=1.K by C1,XA,D0,E0; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by D2,E0,AA1110; end; suppose E0: not ((i0=1 or i0=i0) &(j2=1 or j2=i0)); now per cases; suppose F0: i0=j2; thus (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by E0,F0; end; suppose F0: i0<>j2; (SwapDiagonal(K,n,i0))*(1,j3)=0.K by C1,XA,E0,D2,D0; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by A1,D2,F0,AA1120; end; end; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2); end; end; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2); end; suppose D0: i0=1; now per cases; suppose E0: i0=j2; (SwapDiagonal(K,n,i0))*(1,j3)=1.K by XB,D2,D0,E0; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by AA1110,D2,E0; end; suppose E0: i0<>j2; (SwapDiagonal(K,n,i0))*(1,j3)=0.K by A1,D2,XC,D0,E0; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2) by A1,D2,E0,AA1120; end; end; hence (Base_FinSeq(K,n,i0)).j2 = (SwapDiagonal(K,n,i0))*(1,j2); end; end; hence (Base_FinSeq(K,n,i0)).j2 = Q*(1,j2); end; hence Line(Q,1)=Base_FinSeq(K,n,i0) by MATRIX_1:def 8,C2; end; A6b: Line(Q,i0)=Base_FinSeq(K,n,1) proof C1: 1<=n & 1<=i0 & i0<=n by XXREAL_0:2,A1; C2: len (Base_FinSeq(K,n,1)) = n by AA1100 .= width Q by MATRIX_1:25; for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,1)).j2 = Q*(i0,j2) proof let j2 be Nat; assume j2 in Seg width Q;then D2: 1<=j2 & j2<=n by A2a,FINSEQ_1:3; reconsider j3=j2 as Element of NAT by ORDINAL1:def 13; now per cases; suppose D0: i0<>1; now per cases; suppose i0=1 & j2=i0; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by D0; end; suppose E0: i0=i0 & j2=1; (SwapDiagonal(K,n,i0))*(i0,j3)=1.K by C1,XA,D0,E0; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by D2,E0,AA1110; end; suppose i0=1 & j2=1; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by D0; end; suppose E0: i0=i0 & j2=i0;then (SwapDiagonal(K,n,i0))*(i0,j3)=0.K by XA,D2,D0; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by C1,E0,AA1120,D0; end; suppose E0: not ((i0=1 or i0=i0) &(j2=1 or j2=i0)); now per cases; suppose F0: i0=j2; thus (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by E0,F0; end; suppose i0<>j2; (SwapDiagonal(K,n,i0))*(i0,j3)=0.K by A1,XA,E0,D2,D0; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by C1,D2,E0,AA1120; end; end; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2); end; end; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2); end; suppose D0: i0=1; now per cases; suppose E0: i0=j2; (SwapDiagonal(K,n,i0))*(i0,j3)=1.K by XB,D2,D0,E0; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by AA1110,D2,D0,E0; end; suppose E0: i0<>j2; (SwapDiagonal(K,n,1))*(i0,j3)=0.K by D2,XC,E0,A1; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2) by A1,D2,E0,AA1120,D0; end; end; hence (Base_FinSeq(K,n,1)).j2 = (SwapDiagonal(K,n,i0))*(i0,j2); end; end; hence (Base_FinSeq(K,n,1)).j2 = Q*(i0,j2); end; hence Line(Q,i0)=Base_FinSeq(K,n,1) by MATRIX_1:def 8,C2; end; A10: len (Col(P,j))=n by A2d,MATRIX_1:def 9; B18: 1<=n by XXREAL_0:2,B1; B8b: 1 in Seg n by B18,FINSEQ_1:3; A22: [i0,j] in Indices (Q*P) by B1,MATRIX_1:38,A1; A22b: [1,j] in Indices (Q*P) by B8b,ZFMISC_1:106,B2,B9; thus ((SwapDiagonal(K,n,i0))*A)*(i0,j) = |( Base_FinSeq(K,n,1),Col(P,j))| by A6b,MATRIX_3:def 4,A2a,A2d,A22 .= |( Col(P,j),Base_FinSeq(K,n,1) )| by FVSUM_1:115 .= (Col(P,j)).1 by AA2627,A10,B12 .=A*(1,j) by MATRIX_1:def 9,A9; thus ((SwapDiagonal(K,n,i0))*A)*(1,j) = |( Base_FinSeq(K,n,i0),Col(P,j))| by A6,MATRIX_3:def 4,A2a,A2d,A22b .= |( Col(P,j),Base_FinSeq(K,n,i0) )| by FVSUM_1:115 .= (Col(P,j)).i0 by A1,AA2627,A10 .=A*(i0,j) by MATRIX_1:def 9,A9b; end; thus (for i,j st i<>1 & i<>i0 & 1<=i & i<=n & 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i,j)=A*(i,j)) proof let i,j; assume B1: i<>1 & i<>i0 & 1<=i & i<=n & 1<=j & j<=n; B3b: i in Seg n by FINSEQ_1:3,B1; set Q=(SwapDiagonal(K,n,i0)) ,P=A; A2a: len Q=n & width Q=n & Indices Q=[: Seg n,Seg n :] by MATRIX_1:25; A2d: len P=n & width P=n & Indices P=[: Seg n,Seg n :] by MATRIX_1:25; A9c: i in dom P by FINSEQ_1:def 3,B3b,A2d; A6d: Line(Q,i)=Base_FinSeq(K,n,i) proof C2: len (Base_FinSeq(K,n,i)) = n by AA1100 .= width Q by MATRIX_1:25; for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,i)).j2 = Q*(i,j2) proof let j2 be Nat; assume j2 in Seg width Q;then D2: 1<=j2 & j2<=n by A2a,FINSEQ_1:3; reconsider j3=j2 as Element of NAT by ORDINAL1:def 13; now per cases; suppose D0: i0<>1; now per cases; suppose i=1 & j2=i0; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1; end; suppose i=i0 & j2=1; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1; end; suppose i=1 & j2=1; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1; end; suppose E0: i=i0 & j2=i0; thus (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1,E0; end; suppose E0: not ((i=1 or i=i0) &(j2=1 or j2=i0)); now per cases; suppose F0: i=j2;then (SwapDiagonal(K,n,i0))*(i,j3)=1.K by XA,A1,E0,D2,D0; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1,F0,AA1110; end; suppose F0: i<>j2; (SwapDiagonal(K,n,i0))*(i,j3)=0.K by B1,XA,A1,D2,D0,F0; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by B1,D2,F0,AA1120; end; end; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2); end; end; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2); end; suppose D0: i0=1; now per cases; suppose E0: i=j2; (SwapDiagonal(K,n,i0))*(i,j3)=1.K by XB,D2,D0,E0; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by AA1110,D2,E0; end; suppose E0: i<>j2; (SwapDiagonal(K,n,i0))*(i,j3)=0.K by B1,D2,XC,D0,E0; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2) by AA1120,B1,D2,E0; end; end; hence (Base_FinSeq(K,n,i)).j2 = (SwapDiagonal(K,n,i0))*(i,j2); end; end; hence (Base_FinSeq(K,n,i)).j2 = Q*(i,j2); end; hence Line(Q,i)=Base_FinSeq(K,n,i) by MATRIX_1:def 8,C2; end; A10: len (Col(P,j))=n by A2d,MATRIX_1:def 9; A22: [i,j] in Indices (Q*P) by B1,MATRIX_1:38; thus ((SwapDiagonal(K,n,i0))*A)*(i,j) = |( Base_FinSeq(K,n,i),Col(P,j))| by A6d,MATRIX_3:def 4,A2a,A2d,A22 .= |( Col(P,j),Base_FinSeq(K,n,i) )| by FVSUM_1:115 .= (Col(P,j)).i by AA2627,A10,B1 .=A*(i,j) by MATRIX_1:def 9,A9c; end; end; theorem AA4150: for i0 being Element of NAT st 1<=i0 & i0<=n holds SwapDiagonal(K,n,i0) is invertible & (SwapDiagonal(K,n,i0))~ =SwapDiagonal(K,n,i0) proof let i0 be Element of NAT; assume A1: 1<=i0 & i0<=n; A51: 1<=n by XXREAL_0:2,A1; set R=(SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0)); A10: len R=n & width R=n & Indices R=[: Seg n,Seg n :] by MATRIX_1:25; A11: len (1.(K,n))=n & width (1.(K,n))=n & Indices (1.(K,n))=[: Seg n,Seg n :] by MATRIX_1:25; A5: len R = len (1.(K,n)) & width R = width (1.(K,n)) by MATRIX_1:25,A11; for i4,j4 being Nat st [i4,j4] in Indices R holds R*(i4,j4) = (1.(K,n))*(i4,j4) proof let i4,j4 be Nat; assume B1: [i4,j4] in Indices R; reconsider i=i4,j=j4 as Element of NAT by ORDINAL1:def 13; B15: i in Seg n & j in Seg n by B1,A10,ZFMISC_1:106; B2: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3,B15; B77: [i,j] in Indices (1.(K,n)) by MATRIX_1:25,A10,B1; per cases by B2,REAL_1:def 5; suppose C0: 1i0; now per cases; suppose E0: i=j; E1: (1.(K,n))*(i,j)= 1.K by MATRIX_1:def 12,B77,E0; now per cases; suppose i0<>1; hence (SwapDiagonal(K,n,i0))*(i,j)=1.K by XA,A1,D0,E0,C0,B2; end; suppose i0=1; hence (SwapDiagonal(K,n,i0))*(i,j)=1.K by E0,XB,B2; end; end; hence R*(i,j) = (1.(K,n))*(i,j) by AA4100,A1,C0,B2,D0,E1; end; suppose E0: i<>j; E1: (1.(K,n))*(i,j)=0.K by MATRIX_1:def 12,B77,E0; now per cases; suppose i0=1; hence (SwapDiagonal(K,n,i0))*(i,j)=0.K by XC,E0,B2; end; suppose i0<>1; hence (SwapDiagonal(K,n,i0))*(i,j)=0.K by XA,A1,D0,E0,C0,B2; end; end; hence R*(i,j) = (1.(K,n))*(i,j) by E1,AA4100,A1,C0,B2,D0; end; end; hence R*(i,j) = (1.(K,n))*(i,j); end; suppose D0: i=i0; now per cases; suppose E0: i=j;then E1: (1.(K,n))*(i,j)=1.K by MATRIX_1:def 12,B77; now per cases; suppose i0=1; hence (SwapDiagonal(K,n,i0))*(1,i0)=1.K by D0,C0; end; suppose i0<>1; hence (SwapDiagonal(K,n,i0))*(1,i0)=1.K by XA,A1,A51; end; end; hence R*(i,j) = (1.(K,n))*(i,j) by E1,E0,D0,AA4100,A1; end; suppose E0: i<>j;then E1: (1.(K,n))*(i,j)=0.K by MATRIX_1:def 12,B77; now per cases; suppose i0=1; hence (SwapDiagonal(K,n,i0))*(1,j)=0.K by D0,C0; end; suppose i0<>1; now per cases; suppose j=1; hence (SwapDiagonal(K,n,i0))*(1,j)=0.K by XA,A1,D0,C0,A51; end; suppose j<>1; hence (SwapDiagonal(K,n,i0))*(1,j)=0.K by XA,D0,E0,C0,B2,A51; end; end; hence (SwapDiagonal(K,n,i0))*(1,j)=0.K; end; end; hence R*(i,j) = (1.(K,n))*(i,j) by E1,D0,B2,AA4100; end; end; hence R*(i,j) = (1.(K,n))*(i,j); end; end; hence R*(i4,j4) = (1.(K,n))*(i4,j4); end; suppose C0: 1=i; now per cases; suppose D0: i0<>1; per cases; suppose E0: j<>1;then E1: (1.(K,n))*(i,j)=0.K by C0,MATRIX_1:def 12,B77; now per cases; suppose j=i0; hence (SwapDiagonal(K,n,i0))*(i0,j)=0.K by XA,E0,B2; end; suppose j<>i0; hence (SwapDiagonal(K,n,i0))*(i0,j)=0.K by A1,XA,D0,E0,B2; end; end; hence R*(i,j) = (1.(K,n))*(i,j) by C0,E1,AA4100,A1,B2; end; suppose E0: j=1;then E1: (1.(K,n))*(i,j)= 1.K by MATRIX_1:def 12,B77,C0; (SwapDiagonal(K,n,i0))*(i0,j)=1.K by XA,A1,D0,E0,A51; hence R*(i,j) = (1.(K,n))*(i,j) by C0,E1,AA4100,A1,B2; end; end; suppose D0: i0=1; now per cases; suppose E0: i<>j;then E1: (1.(K,n))*(i,j)=0.K by MATRIX_1:def 12,B77; (SwapDiagonal(K,n,1))*(1,j)=0.K by XC,E0,C0,B2; hence R*(i,j) = (1.(K,n))*(i,j) by C0,E1,AA4100,B2,D0; end; suppose E0: i=j; E1: (1.(K,n))*(j,j)= 1.K by MATRIX_1:def 12,B77,E0; ((SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0)))*(1,j) =(SwapDiagonal(K,n,i0))*(i0,j) by AA4100,A1,B2; hence R*(i,j) = (1.(K,n))*(i,j) by XB,A1,D0,E0,C0,E1; end; end; hence R*(i,j) = (1.(K,n))*(i,j); end; end; hence R*(i4,j4) = (1.(K,n))*(i4,j4); end; end;then A88: (SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0))=1.(K,n) by A5,MATRIX_1:21; hence SwapDiagonal(K,n,i0) is invertible by AA4145; thus (SwapDiagonal(K,n,i0))~=SwapDiagonal(K,n,i0) by AA4140,A88; end; theorem AA4160: for i0 being Element of NAT st 1<=i0 & i0<=n holds (SwapDiagonal(K,n,i0))@=(SwapDiagonal(K,n,i0)) proof let i0 be Element of NAT; assume A1: 1<=i0 & i0<=n; per cases; suppose S: i0<> 1; for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=1 & j=i0 implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i=i0 & j=1 implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i=1 & j=1 implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K)& (i=i0 & j=i0 implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies SwapDiagonal(K,n,i0)@ *(i,j)=1.K)& (i<>j implies SwapDiagonal(K,n,i0)@*(i,j)=0.K)) proof let i,j be Nat; assume B1: 1<=i & i<=n & 1<=j & j<=n; B2: i in Seg n & j in Seg n by FINSEQ_1:3,B1; A5: len (SwapDiagonal(K,n,i0))=n & width (SwapDiagonal(K,n,i0))=n & Indices (SwapDiagonal(K,n,i0))=[: Seg n,Seg n :] by MATRIX_1:25; hereby assume C0: i=1 & j=i0; [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by MATRIX_1:def 7 .=1.K by S,C0,XA,B1; end; hereby assume C0: i=i0 & j=1; [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by MATRIX_1:def 7 .=1.K by S,C0,XA,B1; end; hereby assume C0: i=1 & j=1; [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by MATRIX_1:def 7 .= 0.K by S,C0,XA,A1,B1; end; hereby assume C0: i=i0 & j=i0; [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by MATRIX_1:def 7 .= 0.K by S,C0,XA,B1; end; hereby assume C0: not ((i=1 or i=i0) &(j=1 or j=i0)); C1: [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; C2: now assume D0: i=j; thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by C1,MATRIX_1:def 7 .=1.K by S,C0,XA,A1,B1,D0; end; now assume D0: i<>j; thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by C1,MATRIX_1:def 7 .= 0.K by S,C0,XA,A1,B1,D0; end; hence (i=j implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i<>j implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K) by C2; end; end; hence thesis by AA400X,A1,S; end; suppose S: i0=1; for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=j implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i<>j implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K) proof let i,j be Nat; assume B1: 1<=i & i<=n & 1<=j & j<=n; B2: i in Seg n & j in Seg n by FINSEQ_1:3,B1; A5: len (SwapDiagonal(K,n,i0))=n & width (SwapDiagonal(K,n,i0))=n & Indices (SwapDiagonal(K,n,i0))=[: Seg n,Seg n :] by MATRIX_1:25; C1: [j,i] in Indices (SwapDiagonal(K,n,i0)) by B2,A5,ZFMISC_1:106; hereby assume C0: i=j; thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by C1,MATRIX_1:def 7 .=1.K by S,C0,XB,B1; end; hereby assume C0: i<>j; thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by C1,MATRIX_1:def 7 .= 0.K by S,C0,XC,B1; end; end; hence thesis by AA4000,A1,S; end; end; theorem AA4170: for A being (Matrix of n,K),j0 being Element of NAT st 1<=j0 & j0 <=n holds (for i st 1<=i & i<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j0)=A*(i,1) & (A*(SwapDiagonal(K,n,j0)))*(i,1)=A*(i,j0))& (for i,j st j<>1 & j<>j0 & 1<=i & i<=n & 1<=j & j<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j)=A*(i,j)) proof let A be (Matrix of n,K),j0 be Element of NAT; assume A1: 1<=j0 & j0 <=n; A5: ((SwapDiagonal(K,n,j0))*(A@))@=(A@@)*((SwapDiagonal(K,n,j0))@) by AA44 .= A*((SwapDiagonal(K,n,j0))@) by MATRIXR2:29 .= A*(SwapDiagonal(K,n,j0)) by AA4160,A1; A12: for i st 1<=i & i<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j0)=A*(i,1) & (A*(SwapDiagonal(K,n,j0)))*(i,1)=A*(i,j0) proof let i; assume B1: 1<=i & i<=n;then X: 1<=n by XXREAL_0:2; B2: [j0,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by B1,MATRIX_1:38,A1; B15: [1,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by B1,MATRIX_1:38,X; B3: [i,1] in Indices A by B1,MATRIX_1:38,X; B14: [i,j0] in Indices A by B1,MATRIX_1:38,A1; thus (A*(SwapDiagonal(K,n,j0)))*(i,j0) =(((SwapDiagonal(K,n,j0))*(A@)))*(j0,i) by MATRIX_1:def 7,B2,A5 .=(A@)*(1,i) by B1,A1,AA4100 .=A*(i,1) by MATRIX_1:def 7,B3; thus (A*(SwapDiagonal(K,n,j0)))*(i,1) =(((SwapDiagonal(K,n,j0))*(A@)))*(1,i) by MATRIX_1:def 7,B15,A5 .=(A@)*(j0,i) by B1,A1,AA4100 .=A*(i,j0) by MATRIX_1:def 7,B14; end; for i,j st j<>1 & j<>j0 & 1<=i & i<=n & 1<=j & j<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j)=A*(i,j) proof let i,j; assume B1: j<>1 & j<>j0 & 1<=i & i<=n & 1<=j & j<=n; B15: [j,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by B1,MATRIX_1:38; B17: [i,j] in Indices A by B1,MATRIX_1:38; thus (A*(SwapDiagonal(K,n,j0)))*(i,j) =(((SwapDiagonal(K,n,j0))*(A@)))*(j,i) by MATRIX_1:def 7,B15,A5 .=(A@)*(j,i) by B1,A1,AA4100 .=A*(i,j) by MATRIX_1:def 7,B17; end; hence thesis by A12; end; theorem AA4190: for A being Matrix of n,K holds A=0.(K,n) iff (for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)= 0.K) proof let A be Matrix of n,K; A2: len A=n & width A=n & Indices A=[: Seg n,Seg n :] by MATRIX_1:25; thus A=0.(K,n) implies for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)= 0.K proof assume A=0.(K,n);then B1b: A=0.(K,n,n) by MATRIX_3:def 1; thus for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)= 0.K proof let i,j; assume C1: 1<=i & i<=n & 1<=j & j<=n; [i,j] in Indices A by C1,MATRIX_1:38; hence A*(i,j)= 0.K by B1b,MATRIX_3:3; end; end; assume B0: (for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K); for i,j being Nat st [i,j] in Indices A holds A*(i,j)=(A+A)*(i,j) proof let i,j be Nat; assume B1: [i,j] in Indices A;then i in Seg n & j in Seg n by A2,ZFMISC_1:106;then B3: 1<=i & i<=n & 1<=j & j<=n by FINSEQ_1:3; reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 13; B4: A*(i0,j0)= 0.K by B3,B0; (A+A)*(i,j) = 0.K+(A*(i,j)) by B4,MATRIX_3:def 3,B1 .= A*(i,j) by RLVECT_1:10; hence thesis; end;then A=A+A by MATRIX_1:28; then A = 0.(K,n,n) by MATRIX_4:6,A2; hence A= 0.(K,n) by MATRIX_3:def 1; end; begin :: Left/Right Invertibility and Invertibility theorem AA4200: for A being Matrix of n,K st A<> 0.(K,n) holds ex B,C being Matrix of n,K st B is invertible & C is invertible & (B*A*C)*(1,1) =1.K & (for i st 1 0.(K,n); consider i0,j0 being Element of NAT such that A4: 1<=i0 & i0<=n & 1<=j0 & j0<=n & A*(i0,j0)<>0.K by AA4190,A0; set A2= ((SwapDiagonal(K,n,i0))*A); B1: 1<=n by A4,XXREAL_0:2; B3: (((SwapDiagonal(K,n,i0))*A)*(SwapDiagonal(K,n,j0)))*(1,1) =A2*(1,j0) by A4,AA4170,B1 .=A*(i0,j0) by A4,AA4100; set A3=((SwapDiagonal(K,n,i0))*A)*(SwapDiagonal(K,n,j0)); consider P,Q being Matrix of n,K such that A13: P is invertible & Q is invertible & (P*A3*Q)*(1,1)=1.K & (for i st 1)=1 by FINSEQ_1:57; for i,j being Element of NAT st 1<=i & i<=k & 1<=j & j<=k holds (G*F)*(i,j)=IFEQ(i,j,1.K,0.K) proof let i,j be Element of NAT; assume E1: 1<=i & i<=k & 1<=j & j<=k; E40: len (Line(B3,i+1))=width B3 by MATRIX_1:def 8; E40b: len (Col(A3,j+1))=len A3 by MATRIX_1:def 9; E45: len (Line(G,i))=width G by MATRIX_1:def 8; E46: len (Col(F,j))=len F by MATRIX_1:def 9; E12: 1<=i+1 & 1<=j+1 by NAT_1:11; E13: i+1<=k+1 by E1,XREAL_1:9; E13a: j+1<=k+1 by E1,XREAL_1:9; E3: [i,j] in Indices (G*F) by MATRIX_1:38,E1; E4: len G=k & width G=k & Indices G=[: Seg k,Seg k :] by MATRIX_1:25; E3b: [i+1,j+1] in Indices (B3*A3) by MATRIX_1:38,E12,E13,E13a; E29: k+1=len (<* 0.K *>) +k by FINSEQ_1:56;then E30a: dom (Line(B3,i+1)) = Seg (len (<* 0.K *>) + len (Line(G,i))) by FINSEQ_1:def 3,E4b,E40,E45,E4; E31: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Line(B3,i+1)).k2=(<* 0.K *>).k2 proof let k2 be Nat; assume F1a: k2 in dom (<* 0.K *>); F1b: k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3,F1a; F1d: k2 in {1} by FINSEQ_1:4,FINSEQ_1:57,F1b; F5: k2=1 by TARSKI:def 1,F1d; F1e: 1<=1+k by NAT_1:11; F8a: 1<=k+1 by NAT_1:11; F12: k2 in Seg width B3 by F5,E4b,FINSEQ_1:3,F8a; E12b: 1).k2 by FINSEQ_1:57,F5; end; for k2 being Nat st k2 in dom (Line(G,i)) holds (Line(B3,i+1)).(len (<* 0.K *>) + k2) = (Line(G,i)).k2 proof let k2 be Nat; assume F1a: k2 in dom (Line(G,i)); F1: k2 in Seg len (Line(G,i)) by FINSEQ_1:def 3,F1a; F1b: len (Line(G,i))=width G by MATRIX_1:def 8.=k by MATRIX_1:25; F2: 1<=k2 & k2<=k by FINSEQ_1:3,F1,F1b; E4c: len B3=k+1 & width B3=k+1 & Indices B3=[: Seg (k+1),Seg (k+1) :] by MATRIX_1:25; F30f: 1<=k2+1 & k2+1<=k+1 by F2,XREAL_1:9, NAT_1:11; F3: k2+1 in Seg width B3 by E4c,FINSEQ_1:3,F30f; F30d: [i,k2] in Indices G by MATRIX_1:38,F2,E1; F30: B3*(i+1,k2+1) = G*(i,k2) by D13,F30d; F30a: k2 in Seg k by FINSEQ_1:def 3,F1a,F1b; F30b: k2 in Seg width G by MATRIX_1:25,F30a; F30c: B3*(i+1,k2+1)=(Line(G,i)).k2 by F30,MATRIX_1:def 8,F30b; ((Line(B3,i+1)).(k2+1) = (Line(G,i)).k2) by F3,MATRIX_1:def 8,F30c; hence ((Line(B3,i+1)).(len (<* 0.K *>) + k2) = (Line(G,i)).k2) by FINSEQ_1:57; end;then E18: (<* 0.K *>) ^ Line(G,i)= (Line(B3,i+1)) by FINSEQ_1:def 7,E30a,E31; E30b: dom (Col(A3,j+1)) = Seg (len (<* 0.K *>) + len (Col(F,j))) by FINSEQ_1:def 3,E5b,E29,E40b,E46,E5; E31b: (for k2 being Nat st k2 in dom (<* 0.K *>) holds (Col(A3,j+1)).k2=(<* 0.K *>).k2) proof let k2 be Nat; assume F1a: k2 in dom (<* 0.K *>); F1b: k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3,F1a; F1d: k2 in {1} by FINSEQ_1:4,FINSEQ_1:57,F1b; F5: k2=1 by TARSKI:def 1,F1d; F16a: 1<=k+1 by NAT_1:11; F16b: k2 in Seg len A3 by F5,E5b,FINSEQ_1:3,F16a; F12: k2 in dom A3 by FINSEQ_1:def 3,F16b; F71: 1<=j+1 & j+1<=k+1 by NAT_1:11,E1,XREAL_1:9; F1f: 1).k2 by FINSEQ_1:57,F5; end; for k2 being Nat st k2 in dom (Col(F,j)) holds ((Col(A3,j+1)).(len (<* 0.K *>) + k2) = (Col(F,j)).k2) proof let k2 be Nat; assume F0: k2 in dom (Col(F,j)); reconsider j0=j+1 as Element of NAT; E46: len (Col(F,j0-'1))=len F by MATRIX_1:def 9; F33: j0-'1=j by BINARITH:39; F33a: k2 in Seg len (Col(F,j0-'1)) by F0,FINSEQ_1:def 3,F33; F2: 1<=k2 & k2<=k by E5,E46,FINSEQ_1:3,F33a; K11: 1<=k2+1 & k2+1<=k+1 by F2,XREAL_1:9,NAT_1:11; F3: k2+1 in dom A3 by E5b,FINSEQ_3:27,K11; K4: [k2,j] in Indices F by MATRIX_1:38,F2,E1; K5: [k2,j0-'1] in Indices F by BINARITH:39,K4; F30: A3*(k2+1,j0-'1+1) = F*(k2,j0-'1) by D12,K5; K6: k2 in Seg k by E5,E46,F0,FINSEQ_1:def 3,F33; K7: k2 in dom F by E5,FINSEQ_1:def 3,K6; A3*(k2+1,j0-'1+1)=(Col(F,j0-'1)).k2 by F30,MATRIX_1:def 9,K7; hence thesis by F33,E22,F3,MATRIX_1:def 9; end;then E19: (<* 0.K *>) ^ Col(F,j)= (Col(A3,j+1)) by FINSEQ_1:def 7,E30b,E31b; E20: len (Line(G,i))=width G by MATRIX_1:def 8 .=k by MATRIX_1:25; E21: len (Col(F,j)) = len F by MATRIX_1:def 9 .=k by MATRIX_1:25; E23: (B3*A3)*(i+1,j+1) =|( Line(B3,i+1),Col(A3,j+1) )| by MATRIX_3:def 4,E3b,E4b,E5b .=|( <* 0.K *>, <* 0.K *> )| + |( Line(G,i), Col(F,j) )| by BB250,E20,E21,E18,E19,E22 .= 0.K +|( Line(G,i), Col(F,j) )| by BB270 .= |( Line(G,i), Col(F,j) )| by RLVECT_1:10; now per cases; suppose F0: i=j; [i+1,j+1] in Indices (1.(K,k+1)) by MATRIX_1:38,E12,E13,E13a; then (1.(K,k+1))*(i+1,j+1)= 1.K by F0,MATRIX_1:def 12; hence (1.(K,k+1))*(i+1,j+1)=IFEQ(i,j,1.K,0.K) by FUNCOP_1:def 8,F0; end; suppose F0: i<>j; F3: [i+1,j+1] in Indices (1.(K,k+1)) by MATRIX_1:38,E12,E13,E13a; i+1 <> j+1 implies (1.(K,k+1))*(i+1,j+1) = 0.K by MATRIX_1:def 12,F3; hence (1.(K,k+1))*(i+1,j+1)=IFEQ(i,j,1.K,0.K) by FUNCOP_1:def 8,F0; end; end; hence (G*F)*(i,j)=IFEQ(i,j,1.K,0.K) by E23,MATRIX_3:def 4,E3,E4,E5,D44; end;then G*F=1.(K,k) by BB370;then consider G2 being Matrix of k,K such that D16: F*G2=1.(K,k) by C1; D16b: len F=k & width F=k & Indices F=[:Seg (k),Seg (k):] by MATRIX_1:25; D16c: len G2=k & width G2=k & Indices G2=[:Seg (k),Seg (k):] by MATRIX_1:25; deffunc h(Nat,Nat) = IFEQ($1,1,IFEQ($2,1,1.K,0.K), IFEQ($2,1,0.K,G2*($1-'1,$2-'1))); consider B4 being Matrix of k+1,k+1,K such that D13: for i,j being Nat st [i,j] in Indices B4 holds B4*(i,j) = h(i,j) from MATRIX_1:sch 1; D70: len B4=k+1 & width B4=k+1 & Indices B4=[:Seg (k+1),Seg (k+1):] by MATRIX_1:25; D71: len (A3*B4)=k+1 & width (A3*B4)=k+1 & Indices (A3*B4)=[:Seg (k+1),Seg (k+1):] by MATRIX_1:25; D92c: len (Line(A3,1))=width A3 by MATRIX_1:def 8 .=k+1 by MATRIX_1:25; D92k: len (Line(A3,1))=len (Base_FinSeq(K,k+1,1)) by AA1100,D92c; D94a: for j be Nat st 1<=j & j<=len (Line(A3,1)) holds (Line(A3,1)).j=(Base_FinSeq(K,k+1,1)).j proof let j be Nat; assume E0: 1<=j & j<=len (Line(A3,1)); E1: len (Line(A3,1))=width A3 by MATRIX_1:def 8; E2: j in Seg width A3 by E0,FINSEQ_1:3,E1; E3: 1<=j & j<=k+1 by E0,MATRIX_1:def 8,E5b; E3b: 1<=k+1 by XXREAL_0:2,E3; per cases by E0,REAL_1:def 5; suppose F0: 1=j; (Line(A3,1)).j=1.K by D9,F0,E2,MATRIX_1:def 8; hence thesis by F0,AA1110,E3; end; suppose F0: 11; 1<=len B4 by D100,MATRIX_1:25;then G5: 1 in dom B4 by FINSEQ_3:27; (A3*B4)*(i,j)=|( Line(A3,i0),Col(B4,j0) )| by MATRIX_3:def 4,E0,E4b,E4c .=|(Base_FinSeq(K,k+1,1),Col(B4,j0))| by F0,FINSEQ_1:18,D92k,D94a .=|(Col(B4,j0),Base_FinSeq(K,k+1,1))| by FVSUM_1:115 .=(Col(B4,j0)).1 by AA2627,E40d,D100 .= B4*(1,j) by MATRIX_1:def 9,G5 .= IFEQ(i,1,IFEQ(j,1,1.K,0.K), IFEQ(j,1,0.K,G2*(i-'1,j-'1))) by D13,E89,F0 .=IFEQ(j,1,1.K,0.K) by FUNCOP_1:def 8,F0 .= 0.K by G0,FUNCOP_1:def 8; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j) by F0,G0,E30,MATRIX_1:def 12,E101; end; end; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j); end; suppose F0: 11; G1b: 1+1<=j by NAT_1:13,G0; G1: i-'1=i-1 by F0,BINARITH:50; G2: 1<=i-1 by F1b,XREAL_1:21; G3: j-'1=j-1 by G0,BINARITH:50; G4: 1<=j-1 by G1b,XREAL_1:21; G5: i-'1<=k by E3,G1,XREAL_1:22; G6: j-'1<=k by E3,G3,XREAL_1:22; G7: i-'1 in Seg k by FINSEQ_1:3,G1,G2,G5; j-'1 in Seg k by FINSEQ_1:3,G3,G4,G6;then G9: [i-'1,j-'1] in [:Seg k,Seg k:] by ZFMISC_1:106,G7; E45b: len (Line(F,i-'1))=width F by MATRIX_1:def 8.=k by MATRIX_1:25; E46: len (Col(G2,j-'1))=len G2 by MATRIX_1:def 9.=k by MATRIX_1:25; E30a: dom (Line(A3,i-'1+1))= Seg (k+1) by E40c,G1,FINSEQ_1:def 3 .=Seg (len (<* 0.K *>) + len (Line(F,i-'1))) by FINSEQ_1:56,E45b; E31: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Line(A3,i-'1+1)).k2=(<* 0.K *>).k2 proof let k2 be Nat; assume F1a: k2 in dom (<* 0.K *>); F1b: k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3,F1a; F1d: k2 in {1} by FINSEQ_1:4,FINSEQ_1:57,F1b; F5: k2=1 by TARSKI:def 1,F1d; F1e: 1<=k+1 by NAT_1:11; F12: k2 in Seg width A3 by E4c,F5,FINSEQ_1:3,F1e; F1g: A3*(i0,1) = 0.K by D9,E3,F0; (Line(A3,i)).k2=0.K by F12,F5,MATRIX_1:def 8,F1g; hence (Line(A3,i-'1+1)).k2=(<* 0.K *>).k2 by G1,FINSEQ_1:57,F5; end; (for k2 being Nat st k2 in dom (Line(F,i-'1)) holds (Line(A3,i-'1+1)).(len (<* 0.K *>) + k2) = (Line(F,i-'1)).k2) proof let k2 be Nat; assume F2a: k2 in dom (Line(F,i-'1)); F2b: k2 in Seg len (Line(F,i-'1)) by FINSEQ_1:def 3,F2a; F2: 1<=k2 & k2<=k by E45b,FINSEQ_1:3,F2b; F2d: 1<=k2+1 & k2+1<=k+1 by F2,XREAL_1:9,NAT_1:11; F3: k2+1 in Seg width A3 by E4c,FINSEQ_1:3,F2d; F2f: [i-'1,k2] in Indices F by MATRIX_1:38,F2,G1,G2,G5; F30: A3*(i-'1+1,k2+1) = F*(i-'1,k2) by D12,F2f; F2h: k2 in Seg width F by D16b,E45b,FINSEQ_1:def 3,F2a; F2k: A3*(i-'1+1,k2+1)=(Line(F,i-'1)).k2 by F30,MATRIX_1:def 8,F2h; ((Line(A3,i-'1+1)).(k2+1) = (Line(F,i-'1)).k2) by F3,MATRIX_1:def 8,F2k; hence ((Line(A3,i-'1+1)).(len (<* 0.K *>) + k2) = (Line(F,i-'1)).k2) by FINSEQ_1:57; end;then E18: (<* 0.K *>) ^ Line(F,i-'1)= (Line(A3,i-'1+1)) by FINSEQ_1:def 7,E30a,E31; E30b: dom (Col(B4,j-'1+1)) = Seg len (Col(B4,j-'1+1)) by FINSEQ_1:def 3 .=Seg (len (<* 0.K *>) + len (Col(G2,j-'1))) by E46,FINSEQ_1:56,E40d,G3; E31b: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Col(B4,j-'1+1)).k2=(<* 0.K *>).k2 proof let k2 be Nat; assume F8a: k2 in dom (<* 0.K *>); F8b: k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3,F8a; F8d: k2 in {1} by FINSEQ_1:4,FINSEQ_1:57,F8b; F5: k2=1 by TARSKI:def 1,F8d; F8e: 1<=1+k by NAT_1:11; F8f: 1<=k+1 by NAT_1:11; F8g: k2 in Seg len B4 by F5,E4b,FINSEQ_1:3,F8f; F12: k2 in dom B4 by FINSEQ_1:def 3,F8g; F8h: [1,j] in Indices B4 by MATRIX_1:38,F8e,E3; F8k: B4*(1,j) = IFEQ(1,1, IFEQ(j,1,1.K,0.K), IFEQ(j,1,0.K,G2*(1-'1,j-'1))) by D13,F8h; F8m: B4*(1,j) = IFEQ(j,1,1.K,0.K) by FUNCOP_1:def 8,F8k .= 0.K by FUNCOP_1:def 8,G0; (Col(B4,j)).k2=0.K by F12,F5,MATRIX_1:def 9,F8m; hence (Col(B4,j-'1+1)).k2=(<* 0.K *>).k2 by G3,FINSEQ_1:57,F5; end; for k2 be Nat st k2 in dom (Col(G2,j-'1)) holds ((Col(B4,j-'1+1)).(len (<* 0.K *>) + k2) = (Col(G2,j-'1)).k2) proof let k2 be Nat; assume F3a: k2 in dom (Col(G2,j-'1)); F2: 1<=k2 & k2<=k by E46,FINSEQ_3:27,F3a; F20: 1) + k2) = (Col(G2,j-'1)).k2) by FINSEQ_1:57; end;then E19: (<* 0.K *>) ^ Col(G2,j-'1)= (Col(B4,j-'1+1)) by FINSEQ_1:def 7,E30b,E31b; E88c: [i-'1,j-'1] in Indices (F*G2) by G9,MATRIX_1:25; E88b: [i-'1,j-'1] in Indices (1.(K,k)) by G9,MATRIX_1:25; E160: i-'1+1=i-1+1 by F0,BINARITH:50 .=i; E161: j-'1+1=j-1+1 by G0,BINARITH:50 .=j; G4: (A3*B4)*(i,j)=|( Line(A3,i-'1+1),Col(B4,j-'1+1) )| by E160,E161,MATRIX_3:def 4,E0,E4b,E4c .=|( <* 0.K *>, <* 0.K *> )| + |( Line(F,i-'1), Col(G2,j-'1) )| by BB250,E20b,E21b,E18,E19,E22 .= 0.K +|( Line(F,i-'1), Col(G2,j-'1) )| by BB270 .= 0.K +(F*G2)*(i-'1,j-'1) by MATRIX_3:def 4,E88c,D16b,D16c .= (1.(K,k))*(i-'1,j-'1) by D16,RLVECT_1:10; now per cases; suppose H0: i=j;then (1.(K,k+1))*(i0,j0) =1.K by MATRIX_1:def 12,E104; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j) by G4,H0,MATRIX_1:def 12,E88b; end; suppose H0: i<>j; i-1<>j-1 by H0;then i0-'1<> j0-'1 by F0,BINARITH:50,G3;then (1.(K,k))*(i0-'1,j0-'1) =0.K by MATRIX_1:def 12,E88b; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j) by MATRIX_1:def 12,E104,H0,G4; end; end; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j); end; end; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j); end; end; hence (A3*B4)*(i,j) = (1.(K,k+1))*(i,j); end; K2: width Inv B= k+1 by MATRIX_1:25; K3: len (A2*(C*B4))=k+1 by MATRIX_1:25; K3a: B*A2*C*B4=1.(K,k+1) by MATRIX_1:28,FF0; K3b: (Inv(B))*(B*A2*C*B4)=Inv B by MATRIXR2:67,K2,K3a; K3c: (Inv(B))*(B*A2*C*B4)*B=1.(K,k+1) by D9,AA4140,K3b; K3d: (Inv(B))*(B*A2*(C*B4))*B=1.(K,k+1) by AA41,K3c; K3e: (Inv(B))*(B*(A2*(C*B4)))*B=1.(K,k+1) by AA41,K3d; K3f: (Inv(B))*B*(A2*(C*B4))*B=1.(K,k+1) by AA41,K3e; K3g: (1.(K,k+1))*(A2*(C*B4))*B=1.(K,k+1) by D9,AA4140,K3f; K3h: A2*(C*B4)*B=1.(K,k+1) by MATRIXR2:68,K3,K3g; A2*((C*B4)*B)=1.(K,k+1) by AA41,K3h; hence thesis; end; hence P[k+1]; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(B3,B4); hence thesis by B1; end; end; theorem AA4600: for A being Matrix of n,K holds (ex B1 being Matrix of n,K st B1*A=1.(K,n)) iff (ex B2 being Matrix of n,K st A*B2=1.(K,n)) proof let A be Matrix of n,K; per cases; suppose A1: n>0; thus (ex B being Matrix of n,K st B*A=1.(K,n)) implies (ex B2 being Matrix of n,K st A*B2=1.(K,n)) by AA4500; thus (ex B being Matrix of n,K st A*B=1.(K,n)) implies (ex B2 being Matrix of n,K st B2*A=1.(K,n)) proof assume (ex B being Matrix of n,K st A*B=1.(K,n));then consider B being Matrix of n,K such that B2: A*B=1.(K,n); B12: len A=n & width A=n by MATRIX_1:25; B13: len B=n & width B=n by MATRIX_1:25; (A*B)@=1.(K,n) by B2,MATRIX_6:10;then (B@)*(A@)=1.(K,n) by MATRIX_3:24,A1,B12,B13;then consider B2 being Matrix of n,K such that B3: (A@)*B2= 1.(K,n) by AA4500; B12: len (A@) =n & width (A@) =n by MATRIX_1:25; B13: len B2=n & width B2=n by MATRIX_1:25; ((A@)*B2)@ = 1.(K,n) by B3,MATRIX_6:10;then (B2@)*((A@)@) = 1.(K,n) by MATRIX_3:24,A1,B12,B13;then (B2@)*A= 1.(K,n) by MATRIXR2:29; hence thesis; end; end; suppose B0: n=0;then A*A=1.(K,0) by AA4350; hence thesis by B0; end; end; theorem for A,B being Matrix of n,K st A*B = 1.(K,n) holds A is invertible & B is invertible proof let A,B be Matrix of n,K; assume A1: A*B = 1.(K,n); consider B2 being Matrix of n,K such that A5: B2*A= 1.(K,n) by AA4600,A1; B2=B2*(1.(K,n)) by MATRIX_3:21 .=(B2*A)*B by AA41,A1 .=B by A5,MATRIX_3:20;then A is_reverse_of B by MATRIX_6:def 2,A1,A5; hence A is invertible by MATRIX_6:def 3; consider B3 being Matrix of n,K such that A5: B*B3= 1.(K,n) by AA4500,A1; B3=(1.(K,n))*B3 by MATRIX_3:20 .=A*(B*B3) by AA41,A1 .=A by A5,MATRIX_3:21;then B is_reverse_of A by MATRIX_6:def 2,A1,A5; hence thesis by MATRIX_6:def 3; end;