:: Determinant and Inverse of Matrices of Real Elements
:: by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Copyright (c) 2007-2019 Association of Mizar Users

Lm1: for F1, F2 being FinSequence of REAL
for j being Nat st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)

proof end;

theorem Th1: :: MATRIXR2:1
for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds
( x = - y & y = - x )
proof end;

Lm2: for D being non empty set
for i being Nat
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i

proof end;

theorem Th2: :: MATRIXR2:2
for D being non empty set
for i, j being Nat
for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j
proof end;

theorem Th3: :: MATRIXR2:3
for i, j being Nat
for a being Real
for A being Matrix of REAL st [i,j] in Indices A holds
(a * A) * (i,j) = a * (A * (i,j))
proof end;

theorem :: MATRIXR2:4
for n being Nat
for A, B being Matrix of n,REAL holds
( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
proof end;

theorem Th5: :: MATRIXR2:5
for a being Real
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
proof end;

theorem Th6: :: MATRIXR2:6
for A, B being Matrix of REAL st len A = len B & width A = width B 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)) ) )
proof end;

definition
let n be Nat;
let A, B be Matrix of n,REAL;
:: original: *
redefine func A * B -> Matrix of n,REAL;
coherence
A * B is Matrix of n,REAL
;
end;

theorem Th7: :: MATRIXR2:7
for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
A + (B - B) = A
proof end;

theorem :: MATRIXR2:8
for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
(A + B) - B = A
proof end;

Lm3: for i, j being Nat
for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))

proof end;

theorem Th9: :: MATRIXR2:9
for A being Matrix of REAL holds (- 1) * A = - A
proof end;

theorem Th10: :: MATRIXR2:10
for A being Matrix of REAL
for i, j being Nat st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
proof end;

theorem :: MATRIXR2:11
for a, b being Real
for A being Matrix of REAL holds (a * b) * A = a * (b * A)
proof end;

theorem Th12: :: MATRIXR2:12
for a, b being Real
for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
proof end;

theorem :: MATRIXR2:13
for a, b being Real
for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A)
proof end;

theorem Th14: :: MATRIXR2:14
for n being Nat
for K being Field
for A being Matrix of K st n > 0 & len A > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,())
proof end;

theorem Th15: :: MATRIXR2:15
for K being Field
for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds
(- C) * A = - (C * A)
proof end;

theorem Th16: :: MATRIXR2:16
for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B - C) * A = (B * A) - (C * A)
proof end;

theorem :: MATRIXR2:17
for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds
(A - B) * C = (A * C) - (B * C) by Th16;

theorem Th18: :: MATRIXR2:18
for K being Field
for m being Nat
for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. (K,(),m)) = 0. (K,(len A),m)
proof end;

theorem Th19: :: MATRIXR2:19
for K being Field
for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds
A * (- C) = - (A * C)
proof end;

theorem Th20: :: MATRIXR2:20
for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds
A * (B - C) = (A * B) - (A * C)
proof end;

theorem :: MATRIXR2:21
for A, B, C being Matrix of REAL st len A = len B & width A = width B & width C = len A & len C > 0 & len A > 0 holds
C * (A - B) = (C * A) - (C * B) by Th20;

theorem Th22: :: MATRIXR2:22
for A, B, C being Matrix of REAL st len A = len B & width A = width B & 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
proof end;

theorem Th23: :: MATRIXR2:23
for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
LineVec2Mx (x1 - x2) = () - ()
proof end;

theorem Th24: :: MATRIXR2:24
for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds
ColVec2Mx (x1 - x2) = () - ()
proof end;

theorem Th25: :: MATRIXR2:25
for A, B being Matrix of REAL st len A = len B & 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))
proof end;

theorem Th26: :: MATRIXR2:26
for A, B being Matrix of REAL st len A = len B & width A = width B holds
for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
proof end;

theorem :: MATRIXR2:27
for k, n, m, l being Nat
for A being Matrix of n,k,REAL
for B being Matrix of k,m,REAL
for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
proof end;

theorem Th28: :: MATRIXR2:28
for n being Nat
for A, B, C being Matrix of n,REAL holds (A * B) * C = A * (B * C)
proof end;

theorem Th29: :: MATRIXR2:29
for D being non empty set
for n being Nat
for A being Matrix of n,D holds (A @) @ = A
proof end;

theorem Th30: :: MATRIXR2:30
for n being Nat
for A, B being Matrix of n,REAL holds (A * B) @ = (B @) * (A @)
proof end;

theorem Th31: :: MATRIXR2:31
for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix (n,m)
proof end;

definition
let n be Nat;
let A be Matrix of n,REAL;
:: original: MXR2MXF
redefine func MXR2MXF A -> Matrix of n,F_Real;
coherence
MXR2MXF A is Matrix of n,F_Real
;
end;

definition
let n be Nat;
let A be Matrix of n,REAL;
func Det A -> Real equals :: MATRIXR2:def 1
Det ();
coherence
Det () is Real
;
end;

:: deftheorem defines Det MATRIXR2:def 1 :
for n being Nat
for A being Matrix of n,REAL holds Det A = Det ();

theorem :: MATRIXR2:32
for A being Matrix of 2,REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))
proof end;

theorem Th33: :: MATRIXR2:33
for n being Nat
for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds
<*s1,s2,s3*> is tabular
proof end;

theorem Th34: :: MATRIXR2:34
for D being non empty set
for n being Nat
for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
proof end;

theorem Th35: :: MATRIXR2:35
for D being non empty set
for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
proof end;

theorem Th36: :: MATRIXR2:36
for D being non empty set
for n being Nat
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
proof end;

theorem Th37: :: MATRIXR2:37
for D being non empty set
for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>
proof end;

theorem :: MATRIXR2:38
for A being Matrix of 3,REAL holds Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))
proof end;

theorem :: MATRIXR2:39
for f being Permutation of () holds f = <*> NAT ;

Lm4: idseq 0 is Permutation of ()
by FINSEQ_2:55;

theorem Th40: :: MATRIXR2:40
proof end;

theorem Th41: :: MATRIXR2:41
for K being Ring
for A being Matrix of 0 ,K holds Det A = 1. K
proof end;

theorem :: MATRIXR2:42
for A being Matrix of 0 ,REAL holds Det A = 1
proof end;

:: Removing condition n>=1 from MATRIX7:37
theorem Th43: :: MATRIXR2:43
for K being Field
for n being Nat
for A being Matrix of n,K holds Det A = Det (A @)
proof end;

theorem :: MATRIXR2:44
for n being Nat
for A being Matrix of n,REAL holds Det A = Det (A @) by Th43;

:: Removing condition n>0 from MATRIX11:62
theorem Th45: :: MATRIXR2:45
for n being Nat
for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
proof end;

theorem Th46: :: MATRIXR2:46
for n being Nat
for A, B being Matrix of n,REAL holds Det (A * B) = (Det A) * (Det B)
proof end;

theorem :: MATRIXR2:47
for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds
(x - y) * A = (x * A) - (y * A)
proof end;

theorem :: MATRIXR2:48
for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds
A * (x - y) = (A * x) - (A * y)
proof end;

theorem :: MATRIXR2:49
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(- x) * A = - (x * A)
proof end;

theorem :: MATRIXR2:50
for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len x > 0 holds
A * (- x) = - (A * x)
proof end;

theorem :: MATRIXR2:51
for x being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len x > 0 holds
x * (- A) = - (x * A)
proof end;

theorem :: MATRIXR2:52
for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds
(- A) * x = - (A * x)
proof end;

theorem :: MATRIXR2:53
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)
proof end;

theorem :: MATRIXR2:54
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds
x * (A - B) = (x * A) - (x * B)
proof end;

theorem :: MATRIXR2:55
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)
proof end;

theorem Th56: :: MATRIXR2:56
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x holds
() * A = LineVec2Mx (x * A)
proof end;

theorem Th57: :: MATRIXR2:57
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & width A = len B holds
x * (A * B) = (x * A) * B
proof end;

theorem Th58: :: MATRIXR2:58
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * () = ColVec2Mx (A * x)
proof end;

theorem Th59: :: MATRIXR2:59
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds
(A * B) * x = A * (B * x)
proof end;

theorem :: MATRIXR2:60
for k, n, m being Nat
for B being Matrix of n,m,REAL
for A being Matrix of m,k,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
proof end;

theorem Th61: :: MATRIXR2:61
for n being Nat
for A, B being Matrix of n,REAL
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
proof end;

theorem :: MATRIXR2:62
for n being Nat
for A, B being Matrix of n,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i
proof end;

definition
let n be Nat;
func 1_Rmatrix n -> Matrix of n,REAL equals :: MATRIXR2:def 2
MXF2MXR (1. (F_Real,n));
correctness
coherence
MXF2MXR (1. (F_Real,n)) is Matrix of n,REAL
;
;
end;

:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :
for n being Nat holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));

theorem Th63: :: MATRIXR2:63
for n being Nat holds
( ( for i being Nat st [i,i] in Indices () holds
() * (i,i) = 1 ) & ( for i, j being Nat st [i,j] in Indices () & i <> j holds
() * (i,j) = 0 ) )
proof end;

theorem Th64: :: MATRIXR2:64
for n being Nat holds () @ = 1_Rmatrix n
proof end;

theorem Th65: :: MATRIXR2:65
for n, m being Nat st n > 0 holds
(0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
proof end;

theorem :: MATRIXR2:66
for n, m being Nat
for a being Real st n > 0 holds
a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
proof end;

theorem Th67: :: MATRIXR2:67
for K being Field
for A being Matrix of K holds A * (1. (K,())) = A
proof end;

theorem Th68: :: MATRIXR2:68
for K being Field
for A being Matrix of K holds (1. (K,(len A))) * A = A
proof end;

theorem :: MATRIXR2:69
for n, m being Nat
for A being Matrix of REAL holds
( ( n = width A implies A * () = A ) & ( m = len A implies () * A = A ) ) by ;

theorem Th70: :: MATRIXR2:70
for n being Nat
for A being Matrix of n,REAL holds () * A = A
proof end;

theorem Th71: :: MATRIXR2:71
for n being Nat
for A being Matrix of n,REAL holds A * () = A
proof end;

theorem Th72: :: MATRIXR2:72
for n being Nat holds Det () = 1
proof end;

definition
let n be Nat;
func 0_Rmatrix n -> Matrix of n,REAL equals :: MATRIXR2:def 3
0_Rmatrix (n,n);
correctness
coherence
0_Rmatrix (n,n) is Matrix of n,REAL
;
;
end;

:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :
for n being Nat holds 0_Rmatrix n = 0_Rmatrix (n,n);

theorem :: MATRIXR2:73
for n being Nat st n > 0 holds
Det () = 0
proof end;

definition
let n, i be Nat;
func Base_FinSeq (n,i) -> FinSequence of REAL equals :: MATRIXR2:def 4
(n |-> 0) +* (i,1);
coherence
(n |-> 0) +* (i,1) is FinSequence of REAL
proof end;
end;

:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);

theorem Th74: :: MATRIXR2:74
for n, i being Nat holds len (Base_FinSeq (n,i)) = n
proof end;

theorem Th75: :: MATRIXR2:75
for n, i being Nat st 1 <= i & i <= n holds
(Base_FinSeq (n,i)) . i = 1
proof end;

theorem Th76: :: MATRIXR2:76
for n, i, j being Nat st 1 <= j & j <= n & i <> j holds
(Base_FinSeq (n,i)) . j = 0
proof end;

theorem :: MATRIXR2:77
( Base_FinSeq (1,1) = <*1*> & Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
proof end;

theorem Th78: :: MATRIXR2:78
for i, n being Nat st 1 <= i & i <= n holds
() . i = Base_FinSeq (n,i)
proof end;

definition
let n be Nat;
let A be Matrix of n,REAL;
attr A is invertible means :: MATRIXR2:def 5
ex B being Matrix of n,REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n );
end;

:: deftheorem defines invertible MATRIXR2:def 5 :
for n being Nat
for A being Matrix of n,REAL holds
( A is invertible iff ex B being Matrix of n,REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) );

definition
let n be Nat;
let A be Matrix of n,REAL;
assume A1: A is invertible ;
func Inv A -> Matrix of n,REAL means :Def6: :: MATRIXR2:def 6
( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n );
existence
ex b1 being Matrix of n,REAL st
( b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n )
by A1;
uniqueness
for b1, b2 being Matrix of n,REAL st b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n & b2 * A = 1_Rmatrix n & A * b2 = 1_Rmatrix n holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
for b3 being Matrix of n,REAL holds
( b3 = Inv A iff ( b3 * A = 1_Rmatrix n & A * b3 = 1_Rmatrix n ) );

registration
let n be Nat;
coherence
proof end;
end;

theorem :: MATRIXR2:79
for n being Nat holds Inv () = 1_Rmatrix n
proof end;

theorem Th80: :: MATRIXR2:80
for n being Nat
for A, B1, B2 being Matrix of n,REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds
( B1 = B2 & A is invertible )
proof end;

theorem :: MATRIXR2:81
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Det (Inv A) = (Det A) "
proof end;

theorem :: MATRIXR2:82
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Det A <> 0
proof end;

theorem :: MATRIXR2:83
for n being Nat
for A, B being Matrix of n,REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
proof end;

theorem :: MATRIXR2:84
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Inv (Inv A) = A
proof end;

theorem :: MATRIXR2:85
proof end;

theorem Th86: :: MATRIXR2:86
for n being Nat
for x being FinSequence of REAL st len x = n & n > 0 holds
() * x = x
proof end;

theorem Th87: :: MATRIXR2:87
for n being Nat
for x, y being FinSequence of REAL
for A being Matrix of n,REAL st A is invertible & len x = n & len y = n & n > 0 holds
( A * x = y iff x = (Inv A) * y )
proof end;

theorem Th88: :: MATRIXR2:88
for n being Nat
for x being FinSequence of REAL st len x = n holds
x * () = x
proof end;

theorem Th89: :: MATRIXR2:89
for n being Nat
for x, y being FinSequence of REAL
for A being Matrix of n,REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
proof end;

theorem :: MATRIXR2:90
for n being Nat
for A being Matrix of n,REAL st n > 0 & A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )
proof end;

theorem :: MATRIXR2:91
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
proof end;

theorem :: MATRIXR2:92
for n being Nat
for A being Matrix of n,REAL
for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Nat st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
proof end;

theorem Th93: :: MATRIXR2:93
for n being Nat
for A being Matrix of n,REAL st ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) holds
ex B being Matrix of n,REAL st B * A = 1_Rmatrix n
proof end;

theorem :: MATRIXR2:94
for n being Nat
for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
(A @) * x = x * A
proof end;

theorem Th95: :: MATRIXR2:95
for n being Nat
for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
x * (A @) = A * x
proof end;

theorem Th96: :: MATRIXR2:96
for n being Nat
for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) holds
ex B being Matrix of n,REAL st A * B = 1_Rmatrix n
proof end;

theorem :: MATRIXR2:97
for n being Nat
for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds
A is invertible
proof end;