:: Invertibility of Matrices of Field Elements
:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users


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
proof end;

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
proof end;

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
proof end;

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) )
proof end;

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) )
proof end;

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) )
proof end;

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))
proof end;

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)) )
proof end;

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)|
proof end;

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)|
proof end;

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)|
proof end;

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)|
proof end;

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)
proof end;

notation
let n be Element of NAT ;
let K be Field;
let A be Matrix of n,K;
synonym Inv A for A ~ ;
end;

theorem Th14: :: MATRIX14:14
for K being Field holds
( 1. (K,0) = 0. (K,0) & 1. (K,0) = {} )
proof end;

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) )
proof end;

theorem :: MATRIX14:16
for K being Field
for A being Matrix of 0 ,K holds A is invertible
proof end;

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)
proof end;

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) ) )
proof end;

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) ) )
proof end;

theorem Th20: :: MATRIX14:20
for K being Field
for x being FinSequence of K holds |(x,(0* (K,(len x))))| = 0. K
proof end;

theorem Th21: :: MATRIX14:21
for K being Field
for x being FinSequence of K holds |((0* (K,(len x))),x)| = 0. K
proof end;

theorem Th22: :: MATRIX14:22
for K being Field
for a being Element of K holds |(<*(0. K)*>,<*a*>)| = 0. K
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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
proof end;

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 )
proof end;

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 Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
proof end;

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 @)
proof end;

theorem :: 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 ~) @ )
proof end;

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
proof end;

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) ) )
proof end;

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 ) )
proof end;

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 )
proof end;

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
proof end;

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 ~ )
proof end;

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
proof end;

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 ) )
proof end;

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 ) )
proof end;

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 ) )
proof end;

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
proof end;

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;
proof end;
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 ) ) ) )
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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) ) )
proof end;

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) )
proof end;

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)
proof end;

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) ) )
proof end;

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 )
proof end;

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 ) )
proof end;

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)
proof end;

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) )
proof end;

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 )
proof end;