:: Invertibility of Matrices of Field Elements :: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang :: :: Received April 2, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin definition let K be non empty ZeroStr ; let n be Element of NAT ; func 0* (K,n) -> FinSequence of K equals :: MATRIX14:def 1 n |-> (0. K); coherence n |-> (0. K) is FinSequence of K ; end; :: deftheorem defines 0* MATRIX14:def_1_:_ for K being non empty ZeroStr for n being Element of NAT holds 0* (K,n) = n |-> (0. K); definition let K be non empty ZeroStr ; let n be Element of NAT ; :: original:0* redefine func 0* (K,n) -> Element of n -tuples_on the carrier of K; coherence 0* (K,n) is Element of n -tuples_on the carrier of K ; end; theorem Th1: :: MATRIX14:1 for L being non empty addLoopStr for x being FinSequence of L holds x is Element of (len x) -tuples_on the carrier of L proofend; theorem Th2: :: MATRIX14:2 for L being non empty addLoopStr for x1, x2 being FinSequence of L st len x1 = len x2 holds len (x1 + x2) = len x1 proofend; theorem Th3: :: MATRIX14:3 for L being non empty addLoopStr for x1, x2 being FinSequence of L st len x1 = len x2 holds len (x1 - x2) = len x1 proofend; theorem Th4: :: MATRIX14:4 for G being non empty multLoopStr for x1, x2 being FinSequence of G for i being Element of NAT st i in dom (mlt (x1,x2)) holds ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) proofend; theorem Th5: :: MATRIX14:5 for L being non empty addLoopStr for x1, x2 being FinSequence of L for 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) ) proofend; theorem Th6: :: MATRIX14:6 for K being Field for a being Element of K for x being FinSequence of K holds ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) proofend; theorem Th7: :: MATRIX14:7 for G being non empty multLoopStr 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)) proofend; notation let K be Field; let e1, e2 be FinSequence of K; synonym |(e1,e2)| for e1 "*" e2; end; theorem Th8: :: MATRIX14:8 for K being Field for x, y being FinSequence of K for 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)) ) proofend; theorem :: MATRIX14:9 for K being Field for x, y being FinSequence of K for a being Element of K st len x = len y holds |((a * x),y)| = a * |(x,y)| proofend; theorem Th10: :: MATRIX14:10 for K being Field for x, y being FinSequence of K for a being Element of K st len x = len y holds |(x,(a * y))| = a * |(x,y)| proofend; theorem Th11: :: MATRIX14:11 for K being Field for x, y1, y2 being FinSequence of K for a being Element of K st len x = len y1 & len x = len y2 holds |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| proofend; theorem Th12: :: MATRIX14:12 for K being Field 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)| proofend; theorem Th13: :: MATRIX14:13 for n being Element of NAT for K being Field for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K) proofend; notation let n be Element of NAT ; let K be Field; let A be Matrix of n,K; synonym Inv A for A ~ ; end; begin theorem Th14: :: MATRIX14:14 for K being Field holds ( 1. (K,0) = 0. (K,0) & 1. (K,0) = {} ) proofend; theorem Th15: :: MATRIX14:15 for K being Field for A being Matrix of 0 ,K holds ( A = {} & A = 1. (K,0) & A = 0. (K,0) ) proofend; theorem :: MATRIX14:16 for K being Field for A being Matrix of 0 ,K holds A is invertible proofend; theorem Th17: :: MATRIX14:17 for n being Element of NAT for K being Field for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C) proofend; theorem Th18: :: MATRIX14:18 for n being Element of NAT for K being Field 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) ) ) proofend; theorem Th19: :: MATRIX14:19 for n being Element of NAT for K being Field 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) ) ) proofend; theorem Th20: :: MATRIX14:20 for K being Field for x being FinSequence of K holds |(x,(0* (K,(len x))))| = 0. K proofend; theorem Th21: :: MATRIX14:21 for K being Field for x being FinSequence of K holds |((0* (K,(len x))),x)| = 0. K proofend; theorem Th22: :: MATRIX14:22 for K being Field for a being Element of K holds |(<*(0. K)*>,<*a*>)| = 0. K proofend; definition let K be Field; let n, i be Nat; func Base_FinSeq (K,n,i) -> FinSequence of K equals :: MATRIX14:def 2 Replace ((n |-> (0. K)),i,(1. K)); coherence Replace ((n |-> (0. K)),i,(1. K)) is FinSequence of K ; end; :: deftheorem defines Base_FinSeq MATRIX14:def_2_:_ for K being Field for n, i being Nat holds Base_FinSeq (K,n,i) = Replace ((n |-> (0. K)),i,(1. K)); theorem Th23: :: MATRIX14:23 for K being Field for n, i being Nat holds len (Base_FinSeq (K,n,i)) = n proofend; theorem Th24: :: MATRIX14:24 for K being Field for i, n being Nat st 1 <= i & i <= n holds (Base_FinSeq (K,n,i)) . i = 1. K proofend; theorem Th25: :: MATRIX14:25 for K being Field for i, j, n being Nat st 1 <= j & j <= n & i <> j holds (Base_FinSeq (K,n,i)) . j = 0. K proofend; theorem Th26: :: MATRIX14:26 for K being Field for i, n being Nat st 1 <= i & i <= n holds (1. (K,n)) . i = Base_FinSeq (K,n,i) proofend; theorem Th27: :: MATRIX14:27 for n being Element of NAT for K being Field for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j proofend; theorem :: MATRIX14:28 for n being Element of NAT for K being Field 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 ) proofend; theorem Th29: :: MATRIX14:29 for n being Element of NAT for K being Field 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)) ) proofend; begin theorem Th30: :: MATRIX14:30 for n being Element of NAT for K being Field for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @) proofend; theorem Th31: :: MATRIX14:31 for n being Element of NAT for K being Field for A being Matrix of n,K st A is invertible holds ( A @ is invertible & (A @) ~ = (A ~) @ ) proofend; theorem Th32: :: MATRIX14:32 for K being Field for x being FinSequence of K for a being Element of K st ex i being Element of NAT st ( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds x . j = 0. K ) ) holds Sum x = a proofend; theorem :: MATRIX14:33 for K being Field for f1, f2 being FinSequence of K holds ( dom (mlt (f1,f2)) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt (f1,f2)) holds (mlt (f1,f2)) . i = (f1 /. i) * (f2 /. i) ) ) proofend; theorem Th34: :: MATRIX14:34 for m being Element of NAT for K being Field for x, y being FinSequence of K for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds ( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds y . j = 0. K ) ) proofend; theorem Th35: :: MATRIX14:35 for m, i being Element of NAT for K being Field 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 ) proofend; theorem Th36: :: MATRIX14:36 for K being Field for m, i being Element of NAT st 1 <= i & i <= m holds |((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K proofend; theorem Th37: :: MATRIX14:37 for n being Element of NAT for K being Field for a being Element of K for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds P . i = Base_FinSeq (K,n,i) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds Q . i = Base_FinSeq (K,n,i) ) holds ( P is invertible & Q = P ~ ) proofend; theorem Th38: :: MATRIX14:38 for n being Element of NAT for K being Field for a being Element of K for P being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds P . i = Base_FinSeq (K,n,i) ) holds P is invertible proofend; theorem Th39: :: MATRIX14:39 for n being Element of NAT for K being Field for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds ex P being Matrix of n,K st ( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds (A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds (A * P) * (i,1) = 0. K ) ) proofend; theorem Th40: :: MATRIX14:40 for n being Element of NAT for K being Field for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds ex P being Matrix of n,K st ( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds (P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds (P * A) * (1,j) = 0. K ) ) proofend; theorem Th41: :: MATRIX14:41 for n being Element of NAT for K being Field for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds ex P, Q being Matrix of n,K st ( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds ((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds ((P * A) * Q) * (1,j) = 0. K ) ) proofend; begin theorem Th42: :: MATRIX14:42 for D being non empty set for m, n, i, j being Element of NAT for A being Matrix of m,n,D holds Swap (A,i,j) is Matrix of m,n,D proofend; definition let K be Field; let n be Element of NAT ; let i0 be Nat; func SwapDiagonal (K,n,i0) -> Matrix of n,K equals :: MATRIX14:def 3 Swap ((1. (K,n)),1,i0); correctness coherence Swap ((1. (K,n)),1,i0) is Matrix of n,K; proofend; end; :: deftheorem defines SwapDiagonal MATRIX14:def_3_:_ for K being Field for n being Element of NAT for i0 being Nat holds SwapDiagonal (K,n,i0) = Swap ((1. (K,n)),1,i0); theorem Th43: :: MATRIX14:43 for K being Field for n being Element of NAT for i0 being Nat for 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 & i0 <> 1 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 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) ) proofend; theorem Th44: :: MATRIX14:44 for K being Field for n being Element of NAT for A being Matrix of n,K for i being Nat st 1 <= i & i <= n holds (SwapDiagonal (K,n,1)) * (i,i) = 1. K proofend; theorem Th45: :: MATRIX14:45 for K being Field for n being Element of NAT for A being Matrix of n,K for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds (SwapDiagonal (K,n,1)) * (i,j) = 0. K proofend; theorem Th46: :: MATRIX14:46 for K being Field for n, i0 being Element of NAT for A being Matrix of n,K st 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) proofend; theorem Th47: :: MATRIX14:47 for K being Field for n, i0 being Element of NAT for 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 & not i = i0 ) or ( not j = 1 & not 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) proofend; theorem Th48: :: MATRIX14:48 for n being Element of NAT for K being Field for A being Matrix of n,K for i0 being Element of NAT st 1 <= i0 & i0 <= n holds ( ( for j being Element of NAT 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 being Element of NAT st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds ((SwapDiagonal (K,n,i0)) * A) * (i,j) = A * (i,j) ) ) proofend; theorem Th49: :: MATRIX14:49 for n being Element of NAT for K being Field 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) ) proofend; theorem Th50: :: MATRIX14:50 for n being Element of NAT for K being Field for i0 being Element of NAT st 1 <= i0 & i0 <= n holds (SwapDiagonal (K,n,i0)) @ = SwapDiagonal (K,n,i0) proofend; theorem Th51: :: MATRIX14:51 for n being Element of NAT for K being Field for A being Matrix of n,K for j0 being Element of NAT st 1 <= j0 & j0 <= n holds ( ( for i being Element of NAT 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 being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds (A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) ) proofend; theorem Th52: :: MATRIX14:52 for n being Element of NAT for K being Field 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 ) proofend; begin theorem Th53: :: MATRIX14:53 for n being Element of NAT for K being Field 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 being Element of NAT st 1 < i & i <= n holds ((B * A) * C) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds ((B * A) * C) * (1,j) = 0. K ) ) proofend; theorem Th54: :: MATRIX14:54 for n being Element of NAT for K being Field for A, B being Matrix of n,K st B * A = 1. (K,n) holds ex B2 being Matrix of n,K st A * B2 = 1. (K,n) proofend; theorem Th55: :: MATRIX14:55 for n being Element of NAT for K being Field 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) ) proofend; theorem :: MATRIX14:56 for n being Element of NAT for K being Field for A, B being Matrix of n,K st A * B = 1. (K,n) holds ( A is invertible & B is invertible ) proofend;