:: Invertibility of Matrices of Field Elements
:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem defines 0* MATRIX14:def 1 :
theorem Th1: :: MATRIX14:1
theorem Th2: :: MATRIX14:2
theorem Th3: :: MATRIX14:3
theorem Th4: :: MATRIX14:4
theorem Th5: :: MATRIX14:5
theorem Th6: :: MATRIX14:6
theorem Th7: :: MATRIX14:7
theorem Th8: :: MATRIX14:8
theorem :: MATRIX14:9
theorem Th10: :: MATRIX14:10
theorem Th11: :: MATRIX14:11
theorem Th12: :: MATRIX14:12
theorem Th13: :: MATRIX14:13
theorem Th14: :: MATRIX14:14
theorem Th15: :: MATRIX14:15
theorem :: MATRIX14:16
theorem Th17: :: MATRIX14:17
theorem Th18: :: MATRIX14:18
theorem Th19: :: MATRIX14:19
theorem Th20: :: MATRIX14:20
theorem Th21: :: MATRIX14:21
theorem Th22: :: MATRIX14:22
:: deftheorem defines Base_FinSeq MATRIX14:def 2 :
theorem Th23: :: MATRIX14:23
theorem Th24: :: MATRIX14:24
theorem Th25: :: MATRIX14:25
theorem Th26: :: MATRIX14:26
theorem Th27: :: MATRIX14:27
theorem :: MATRIX14:28
theorem Th29: :: MATRIX14:29
theorem Th30: :: MATRIX14:30
theorem Th31: :: MATRIX14:31
theorem Th32: :: MATRIX14:32
theorem :: MATRIX14:33
theorem Th34: :: MATRIX14:34
theorem Th35: :: MATRIX14:35
theorem Th36: :: MATRIX14:36
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 ~ )
theorem Th38: :: MATRIX14:38
theorem Th39: :: MATRIX14:39
theorem Th40: :: MATRIX14:40
theorem Th41: :: MATRIX14:41
theorem Th42: :: MATRIX14:42
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;
end;
:: deftheorem defines SwapDiagonal MATRIX14:def 3 :
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 ) ) ) )
theorem Th44: :: MATRIX14:44
theorem Th45: :: MATRIX14:45
theorem Th46: :: MATRIX14:46
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
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 ) )
theorem Th49: :: MATRIX14:49
theorem Th50: :: MATRIX14:50
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 ) )
theorem Th52: :: MATRIX14:52
theorem Th53: :: MATRIX14:53
theorem Th54: :: MATRIX14:54
theorem Th55: :: MATRIX14:55
theorem :: MATRIX14:56