:: Determinant and Inverse of Matrices of Real Elements
:: by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Received July 17, 2007
:: Copyright (c) 2007 Association of Mizar Users
Lm1:
for F1, F2 being FinSequence of REAL
for j being Element of NAT st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
theorem Th1: :: MATRIXR2:1
Lm2:
for D being non empty set
for i being Element of NAT
for A being Matrix of D st 1 <= i & i <= len A holds
Line A,i = A . i
theorem Th2: :: MATRIXR2:2
theorem Th3: :: MATRIXR2:3
theorem Th4: :: MATRIXR2:4
theorem Th5: :: MATRIXR2:5
theorem Th6: :: MATRIXR2:6
theorem Th7: :: MATRIXR2:7
theorem :: MATRIXR2:8
Lm3:
for i, j being Element of NAT
for A being Matrix of REAL st len (- A) = len A & width (- A) = width A & [i,j] in Indices A holds
(- A) * i,j = - (A * i,j)
theorem Th9: :: MATRIXR2:9
theorem Th10: :: MATRIXR2:10
theorem :: MATRIXR2:11
theorem Th12: :: MATRIXR2:12
theorem :: MATRIXR2:13
theorem Th14: :: MATRIXR2:14
theorem Th15: :: MATRIXR2:15
theorem Th16: :: MATRIXR2:16
theorem :: MATRIXR2:17
theorem Th18: :: MATRIXR2:18
theorem Th19: :: MATRIXR2:19
theorem Th20: :: MATRIXR2:20
theorem :: MATRIXR2:21
theorem Th22: :: MATRIXR2:22
theorem Th23: :: MATRIXR2:23
theorem Th24: :: MATRIXR2:24
theorem Th25: :: MATRIXR2:25
theorem Th26: :: MATRIXR2:26
theorem :: MATRIXR2:27
theorem Th28: :: MATRIXR2:28
theorem Th29: :: MATRIXR2:29
theorem Th30: :: MATRIXR2:30
theorem Th31: :: MATRIXR2:31
:: deftheorem defines Det MATRIXR2:def 1 :
theorem :: MATRIXR2:32
theorem Th33: :: MATRIXR2:33
theorem Th34: :: MATRIXR2:34
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
theorem Th36: :: MATRIXR2:36
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)*>*>
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))
theorem :: MATRIXR2:39
Lm4:
idseq 0 is Permutation of (Seg 0 )
by FINSEQ_2:65;
theorem Th40: :: MATRIXR2:40
theorem Th41: :: MATRIXR2:41
theorem :: MATRIXR2:42
theorem Th43: :: MATRIXR2:43
theorem :: MATRIXR2:44
theorem Th45: :: MATRIXR2:45
theorem Th46: :: MATRIXR2:46
theorem :: MATRIXR2:47
theorem :: MATRIXR2:48
theorem :: MATRIXR2:49
theorem :: MATRIXR2:50
theorem :: MATRIXR2:51
theorem :: MATRIXR2:52
theorem :: MATRIXR2:53
theorem :: MATRIXR2:54
theorem :: MATRIXR2:55
theorem Th56: :: MATRIXR2:56
theorem Th57: :: MATRIXR2:57
theorem Th58: :: MATRIXR2:58
theorem Th59: :: MATRIXR2:59
theorem :: MATRIXR2:60
for
n,
m,
k being
Element of
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
Element of
NAT st
[i,j] in Indices (B * A) holds
(B * A) * i,
j = ((Line B,i) * A) . j
theorem Th61: :: MATRIXR2:61
theorem :: MATRIXR2:62
:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :
theorem Th63: :: MATRIXR2:63
theorem Th64: :: MATRIXR2:64
theorem Th65: :: MATRIXR2:65
theorem :: MATRIXR2:66
theorem Th67: :: MATRIXR2:67
theorem Th68: :: MATRIXR2:68
theorem :: MATRIXR2:69
theorem Th70: :: MATRIXR2:70
theorem Th71: :: MATRIXR2:71
theorem Th72: :: MATRIXR2:72
:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :
theorem :: MATRIXR2:73
:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
theorem Th74: :: MATRIXR2:74
theorem Th75: :: MATRIXR2:75
theorem Th76: :: MATRIXR2:76
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*> )
theorem Th78: :: MATRIXR2:78
:: deftheorem Def5 defines invertible MATRIXR2:def 5 :
:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
theorem :: MATRIXR2:79
theorem Th80: :: MATRIXR2:80
theorem :: MATRIXR2:81
theorem :: MATRIXR2:82
theorem :: MATRIXR2:83
theorem :: MATRIXR2:84
theorem :: MATRIXR2:85
theorem Th86: :: MATRIXR2:86
theorem Th87: :: MATRIXR2:87
theorem Th88: :: MATRIXR2:88
theorem Th89: :: MATRIXR2:89
theorem :: MATRIXR2:90
theorem :: MATRIXR2:91
theorem :: MATRIXR2:92
theorem Th93: :: MATRIXR2:93
theorem :: MATRIXR2:94
theorem Th95: :: MATRIXR2:95
theorem Th96: :: MATRIXR2:96
theorem :: MATRIXR2:97