:: 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 BB100: :: MATRIX14:1
theorem Th6: :: MATRIX14:2
theorem Th7: :: MATRIX14:3
theorem FV73: :: MATRIX14:4
theorem BB120: :: MATRIX14:5
theorem BB200: :: MATRIX14:6
theorem BB240: :: MATRIX14:7
theorem BB243: :: MATRIX14:8
theorem :: MATRIX14:9
theorem BB246: :: MATRIX14:10
theorem BB248: :: MATRIX14:11
theorem BB250: :: MATRIX14:12
theorem Th2: :: MATRIX14:13
theorem MR103: :: MATRIX14:14
theorem AA4350: :: MATRIX14:15
theorem :: MATRIX14:16
theorem AA41: :: MATRIX14:17
theorem AA4140: :: MATRIX14:18
theorem AA4145: :: MATRIX14:19
theorem Th17: :: MATRIX14:20
theorem Th18: :: MATRIX14:21
theorem BB270: :: MATRIX14:22
:: deftheorem defines Base_FinSeq MATRIX14:def 2 :
theorem AA1100: :: MATRIX14:23
theorem AA1110: :: MATRIX14:24
theorem AA1120: :: MATRIX14:25
theorem AA1200: :: MATRIX14:26
theorem BB300: :: MATRIX14:27
theorem :: MATRIX14:28
theorem BB370: :: MATRIX14:29
theorem AA44: :: MATRIX14:30
theorem BB400: :: MATRIX14:31
theorem AA2626: :: MATRIX14:32
theorem :: MATRIX14:33
theorem AA2626b: :: MATRIX14:34
theorem AA2627: :: MATRIX14:35
theorem AA2629: :: MATRIX14:36
theorem AA3000: :: 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 AA3010: :: MATRIX14:38
theorem AA3020: :: MATRIX14:39
theorem AA3030: :: MATRIX14:40
theorem AA3040: :: MATRIX14:41
theorem AA330: :: 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 XA: :: 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 XB: :: MATRIX14:44
theorem XC: :: MATRIX14:45
theorem AA4000: :: MATRIX14:46
theorem AA400X: :: 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 AA4100: :: 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 AA4150: :: MATRIX14:49
theorem AA4160: :: MATRIX14:50
theorem AA4170: :: 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 AA4190: :: MATRIX14:52
theorem AA4200: :: MATRIX14:53
theorem AA4500: :: MATRIX14:54
theorem AA4600: :: MATRIX14:55
theorem :: MATRIX14:56