:: A Theory of Matrices of Real Elements :: by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang :: :: Received February 20, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin theorem :: MATRIXR1:1 for r1, r2 being Real for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds r1 + r2 = fr1 + fr2 ; theorem :: MATRIXR1:2 for r1, r2 being Real for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds r1 * r2 = fr1 * fr2 ; theorem Th3: :: MATRIXR1:3 for F being FinSequence of REAL holds ( F + (- F) = 0* (len F) & F - F = 0* (len F) ) proofend; theorem :: MATRIXR1:4 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 - F2 = F1 + (- F2) ; theorem :: MATRIXR1:5 for F being FinSequence of REAL holds F - (0* (len F)) = F proofend; theorem :: MATRIXR1:6 for F being FinSequence of REAL holds (0* (len F)) - F = - F proofend; theorem :: MATRIXR1:7 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 - (- F2) = F1 + F2 ; theorem :: MATRIXR1:8 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds - (F1 - F2) = F2 - F1 by RVSUM_1:35; theorem :: MATRIXR1:9 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds - (F1 - F2) = (- F1) + F2 by RVSUM_1:36; theorem :: MATRIXR1:10 for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds F1 = F2 proofend; theorem :: MATRIXR1:11 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds (F1 - F2) - F3 = F1 - (F2 + F3) by RVSUM_1:39; theorem :: MATRIXR1:12 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds F1 + (F2 - F3) = (F1 + F2) - F3 by RVSUM_1:40; theorem :: MATRIXR1:13 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds F1 - (F2 - F3) = (F1 - F2) + F3 by RVSUM_1:41; theorem Th14: :: MATRIXR1:14 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 = (F1 + F2) - F2 proofend; theorem :: MATRIXR1:15 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 = (F1 - F2) + F2 proofend; begin theorem Th16: :: MATRIXR1:16 for K being non empty multMagma for p being FinSequence of K for a being Element of K holds len (a * p) = len p proofend; theorem Th17: :: MATRIXR1:17 for r being Real for fr being Element of F_Real for p being FinSequence of REAL for fp being FinSequence of F_Real st r = fr & p = fp holds r * p = fr * fp proofend; theorem :: MATRIXR1:18 for K being Field for a being Element of K for A being Matrix of K holds Indices (a * A) = Indices A proofend; theorem Th19: :: MATRIXR1:19 for i being Nat for K being Field for a being Element of K for M being Matrix of K st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) proofend; theorem :: MATRIXR1:20 for K being Field for a being Element of K for M being Matrix of K for i being Nat st 1 <= i & i <= len M holds Line ((a * M),i) = a * (Line (M,i)) proofend; theorem :: MATRIXR1:21 for K being Field for A, B being Matrix of K st width A = len B holds ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) proofend; theorem Th22: :: MATRIXR1:22 for K being Field for a being Element of K for A, B being Matrix of K st width A = len B holds A * (a * B) = a * (A * B) proofend; definition let A be Matrix of REAL; func MXR2MXF A -> Matrix of F_Real equals :: MATRIXR1:def 1 A; coherence A is Matrix of F_Real ; end; :: deftheorem defines MXR2MXF MATRIXR1:def_1_:_ for A being Matrix of REAL holds MXR2MXF A = A; definition let A be Matrix of F_Real; func MXF2MXR A -> Matrix of REAL equals :: MATRIXR1:def 2 A; coherence A is Matrix of REAL ; end; :: deftheorem defines MXF2MXR MATRIXR1:def_2_:_ for A being Matrix of F_Real holds MXF2MXR A = A; theorem :: MATRIXR1:23 for D1, D2 being set for A being Matrix of D1 for B being Matrix of D2 st A = B holds for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) proofend; theorem :: MATRIXR1:24 for K being Field for A, B being Matrix of K holds Indices (A + B) = Indices A proofend; definition let A, B be Matrix of REAL; funcA + B -> Matrix of REAL equals :: MATRIXR1:def 3 MXF2MXR ((MXR2MXF A) + (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) is Matrix of REAL ; end; :: deftheorem defines + MATRIXR1:def_3_:_ for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B)); theorem Th25: :: MATRIXR1:25 for A, B being Matrix of REAL holds ( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) proofend; theorem Th26: :: MATRIXR1:26 for A, B, C being Matrix of REAL st len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds C = A + B proofend; definition let A be Matrix of REAL; func - A -> Matrix of REAL equals :: MATRIXR1:def 4 MXF2MXR (- (MXR2MXF A)); coherence MXF2MXR (- (MXR2MXF A)) is Matrix of REAL ; end; :: deftheorem defines - MATRIXR1:def_4_:_ for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A)); definition let A, B be Matrix of REAL; funcA - B -> Matrix of REAL equals :: MATRIXR1:def 5 MXF2MXR ((MXR2MXF A) - (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ; funcA * B -> Matrix of REAL equals :: MATRIXR1:def 6 MXF2MXR ((MXR2MXF A) * (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ; end; :: deftheorem defines - MATRIXR1:def_5_:_ for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B)); :: deftheorem defines * MATRIXR1:def_6_:_ for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B)); definition let a be real number ; let A be Matrix of REAL; funca * A -> Matrix of REAL means :Def7: :: MATRIXR1:def 7 for ea being Element of F_Real st ea = a holds it = MXF2MXR (ea * (MXR2MXF A)); existence ex b1 being Matrix of REAL st for ea being Element of F_Real st ea = a holds b1 = MXF2MXR (ea * (MXR2MXF A)) proofend; uniqueness for b1, b2 being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds b1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds b2 = MXF2MXR (ea * (MXR2MXF A)) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines * MATRIXR1:def_7_:_ for a being real number for A, b3 being Matrix of REAL holds ( b3 = a * A iff for ea being Element of F_Real st ea = a holds b3 = MXF2MXR (ea * (MXR2MXF A)) ); theorem Th27: :: MATRIXR1:27 for a being Real for A being Matrix of REAL holds ( len (a * A) = len A & width (a * A) = width A ) proofend; theorem Th28: :: MATRIXR1:28 for a being Real for A being Matrix of REAL holds Indices (a * A) = Indices A proofend; theorem Th29: :: MATRIXR1:29 for a being Real for A being Matrix of REAL for i2, j2 being Nat st [i2,j2] in Indices A holds (a * A) * (i2,j2) = a * (A * (i2,j2)) proofend; theorem Th30: :: MATRIXR1:30 for a being Real for A being Matrix of REAL st width A > 0 holds (a * A) @ = a * (A @) proofend; theorem :: MATRIXR1:31 for a being Real for i being Nat for A being Matrix of REAL st len A > 0 & i in dom A holds ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) proofend; theorem :: MATRIXR1:32 for A being Matrix of REAL holds 1 * A = A proofend; theorem :: MATRIXR1:33 for A being Matrix of REAL holds A + A = 2 * A proofend; theorem :: MATRIXR1:34 for A being Matrix of REAL holds (A + A) + A = 3 * A proofend; definition let n, m be Nat; func 0_Rmatrix (n,m) -> Matrix of REAL equals :: MATRIXR1:def 8 MXF2MXR (0. (F_Real,n,m)); coherence MXF2MXR (0. (F_Real,n,m)) is Matrix of REAL ; end; :: deftheorem defines 0_Rmatrix MATRIXR1:def_8_:_ for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m)); theorem :: MATRIXR1:35 for A, B being Matrix of REAL holds A - (- B) = A + B proofend; theorem Th36: :: MATRIXR1:36 for n, m being Nat for A being Matrix of REAL st len A = n & width A = m & n > 0 holds ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) proofend; theorem :: MATRIXR1:37 for A, B being Matrix of REAL st len A = len B & width A = width B & A = A + B holds B = 0_Rmatrix ((len A),(width A)) proofend; theorem :: MATRIXR1:38 for A, B being Matrix of REAL st len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) holds B = - A proofend; theorem :: MATRIXR1:39 for A, B being Matrix of REAL st len A = len B & width A = width B & B - A = B holds A = 0_Rmatrix ((len A),(width A)) proofend; theorem Th40: :: MATRIXR1:40 for a being Real for A, B being Matrix of REAL st width A = len B holds A * (a * B) = a * (A * B) proofend; theorem :: MATRIXR1:41 for a being Real for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds (a * A) * B = a * (A * B) proofend; theorem :: MATRIXR1:42 for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M proofend; theorem :: MATRIXR1:43 for a being real number for A, B being Matrix of REAL st len A = len B & width A = width B holds a * (A + B) = (a * A) + (a * B) proofend; theorem :: MATRIXR1:44 for A being Matrix of REAL st len A > 0 holds 0 * A = 0_Rmatrix ((len A),(width A)) proofend; definition let x be FinSequence of REAL ; assume A1: len x > 0 ; func ColVec2Mx x -> Matrix of REAL means :Def9: :: MATRIXR1:def 9 ( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds it . j = <*(x . j)*> ) ); existence ex b1 being Matrix of REAL st ( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds b1 . j = <*(x . j)*> ) ) proofend; uniqueness for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds b2 . j = <*(x . j)*> ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines ColVec2Mx MATRIXR1:def_9_:_ for x being FinSequence of REAL st len x > 0 holds for b2 being Matrix of REAL holds ( b2 = ColVec2Mx x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds b2 . j = <*(x . j)*> ) ) ); theorem :: MATRIXR1:45 for x being FinSequence of REAL for M being Matrix of REAL st len x > 0 holds ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) proofend; theorem Th46: :: MATRIXR1:46 for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) proofend; theorem Th47: :: MATRIXR1:47 for a being Real for x being FinSequence of REAL st len x > 0 holds ColVec2Mx (a * x) = a * (ColVec2Mx x) proofend; definition let x be FinSequence of REAL ; func LineVec2Mx x -> Matrix of REAL means :Def10: :: MATRIXR1:def 10 ( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds it * (1,j) = x . j ) ); existence ex b1 being Matrix of REAL st ( width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds b1 * (1,j) = x . j ) ) proofend; uniqueness for b1, b2 being Matrix of REAL st width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds b1 * (1,j) = x . j ) & width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds b2 * (1,j) = x . j ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines LineVec2Mx MATRIXR1:def_10_:_ for x being FinSequence of REAL for b2 being Matrix of REAL holds ( b2 = LineVec2Mx x iff ( width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds b2 * (1,j) = x . j ) ) ); theorem :: MATRIXR1:48 for x being FinSequence of REAL for M being Matrix of REAL holds ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) ) proofend; theorem Th49: :: MATRIXR1:49 for x being FinSequence of REAL st len x > 0 holds ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) proofend; theorem Th50: :: MATRIXR1:50 for x1, x2 being FinSequence of REAL st len x1 = len x2 holds LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) proofend; theorem :: MATRIXR1:51 for a being Real for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x) proofend; definition let M be Matrix of REAL; let x be FinSequence of REAL ; funcM * x -> FinSequence of REAL equals :: MATRIXR1:def 11 Col ((M * (ColVec2Mx x)),1); coherence Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ; funcx * M -> FinSequence of REAL equals :: MATRIXR1:def 12 Line (((LineVec2Mx x) * M),1); coherence Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ; end; :: deftheorem defines * MATRIXR1:def_11_:_ for M being Matrix of REAL for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1); :: deftheorem defines * MATRIXR1:def_12_:_ for M being Matrix of REAL for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1); theorem Th52: :: MATRIXR1:52 for x being FinSequence of REAL for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds (A @) * x = x * A proofend; theorem Th53: :: MATRIXR1:53 for x being FinSequence of REAL for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds A * x = x * (A @) proofend; theorem Th54: :: MATRIXR1:54 for A, B being Matrix of REAL st len A = len B holds for i being Nat st 1 <= i & i <= width A holds Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) proofend; theorem Th55: :: MATRIXR1:55 for A, B being Matrix of REAL st width A = width B holds for i being Nat st 1 <= i & i <= len A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) proofend; theorem Th56: :: MATRIXR1:56 for a being Real for M being Matrix of REAL for i being Nat st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) proofend; theorem :: MATRIXR1:57 for x1, x2 being FinSequence of REAL for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds A * (x1 + x2) = (A * x1) + (A * x2) proofend; theorem :: MATRIXR1:58 for x1, x2 being FinSequence of REAL for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds (x1 + x2) * A = (x1 * A) + (x2 * A) proofend; theorem Th59: :: MATRIXR1:59 for a being Real for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds A * (a * x) = a * (A * x) proofend; theorem :: MATRIXR1:60 for a being Real for x being FinSequence of REAL for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (a * x) * A = a * (x * A) proofend; theorem Th61: :: MATRIXR1:61 for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds len (A * x) = len A proofend; theorem Th62: :: MATRIXR1:62 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x holds len (x * A) = width A proofend; theorem Th63: :: MATRIXR1:63 for x being FinSequence of REAL for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds (A + B) * x = (A * x) + (B * x) proofend; theorem Th64: :: MATRIXR1:64 for x being FinSequence of REAL for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds x * (A + B) = (x * A) + (x * B) proofend; theorem :: MATRIXR1:65 for n, m being Element of NAT for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds (0_Rmatrix (n,m)) * x = 0* n proofend; theorem :: MATRIXR1:66 for n, m being Element of NAT for x being FinSequence of REAL st len x = n & n > 0 holds x * (0_Rmatrix (n,m)) = 0* m proofend;