let n be Element of NAT ; :: thesis: 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
let K be Field; :: thesis: 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
let a be Element of K; :: thesis: 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
let P be Matrix of n,K; :: thesis: ( 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 ) implies P is invertible )
assume A1:
( 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 ) )
; :: thesis: P is invertible
defpred S1[ Nat, Nat, Element of K] means ( ( $1 = 1 implies ( ( $2 = 1 implies $3 = a ) & ( $2 <> 1 implies $3 = - (a * (P * 1,$2)) ) ) ) & ( $1 <> 1 implies for i0 being Element of NAT st i0 = $1 holds
$3 = (Base_FinSeq K,n,i0) . $2 ) );
A5:
for i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
for x1, x2 being Element of K st S1[i,j,x1] & S1[i,j,x2] holds
x1 = x2
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in [:(Seg n),(Seg n):] implies for x1, x2 being Element of K st S1[i,j,x1] & S1[i,j,x2] holds
x1 = x2 )
assume
[i,j] in [:(Seg n),(Seg n):]
;
:: thesis: for x1, x2 being Element of K st S1[i,j,x1] & S1[i,j,x2] holds
x1 = x2
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
thus
for
x1,
x2 being
Element of
K st
S1[
i,
j,
x1] &
S1[
i,
j,
x2] holds
x1 = x2
:: thesis: verum
end;
A6:
for i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
ex x being Element of K st S1[i,j,x]
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in [:(Seg n),(Seg n):] implies ex x being Element of K st S1[i,j,x] )
assume B1:
[i,j] in [:(Seg n),(Seg n):]
;
:: thesis: ex x being Element of K st S1[i,j,x]
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
(
i0 in Seg n &
j0 in Seg n )
by B1, ZFMISC_1:106;
then B1b:
( 1
<= i0 &
i0 <= n & 1
<= j0 &
j0 <= n )
by FINSEQ_1:3;
per cases
( i = 1 or i <> 1 )
;
suppose C0:
i <> 1
;
:: thesis: ex x being Element of K st S1[i,j,x]
len (Base_FinSeq K,n,i0) = n
by AA1100;
then
(Base_FinSeq K,n,i0) /. j0 = (Base_FinSeq K,n,i0) . j0
by B1b, FINSEQ_4:24;
then reconsider x1 =
(Base_FinSeq K,n,i0) . j0 as
Element of
K ;
( (
i = 1 implies ( (
j = 1 implies
x1 = a ) & (
j <> 1 implies
x1 = - (a * (P * 1,j)) ) ) ) & (
i <> 1 implies for
i1 being
Element of
NAT st
i1 = i holds
x1 = (Base_FinSeq K,n,i1) . j ) )
by C0;
hence
ex
x being
Element of
K st
S1[
i,
j,
x]
;
:: thesis: verum end;
end;
consider Q0 being Matrix of n,n,K such that
A7:
for i, j being Nat st [i,j] in Indices Q0 holds
S1[i,j,Q0 * i,j]
from MATRIX_1:sch 2(A5, A6);
A70:
Indices Q0 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A70a:
0 + 1 <= n
by A1, NAT_1:13;
A30:
1 in Seg n
by A70a, FINSEQ_1:3;
A30a:
[1,1] in Indices Q0
by A70a, MATRIX_1:38;
A10:
Q0 * 1,1 = a
by A7, A30a;
A11:
for j being Element of NAT st 1 < j & j <= n holds
Q0 * 1,j = - (a * (P * 1,j))
proof
let j be
Element of
NAT ;
:: thesis: ( 1 < j & j <= n implies Q0 * 1,j = - (a * (P * 1,j)) )
assume B1:
( 1
< j &
j <= n )
;
:: thesis: Q0 * 1,j = - (a * (P * 1,j))
[1,j] in Indices Q0
by B1, A70a, MATRIX_1:38;
hence
Q0 * 1,
j = - (a * (P * 1,j))
by B1, A7;
:: thesis: verum
end;
for i being Element of NAT st 1 < i & i <= n holds
Q0 . i = Base_FinSeq K,n,i
proof
let i be
Element of
NAT ;
:: thesis: ( 1 < i & i <= n implies Q0 . i = Base_FinSeq K,n,i )
assume B1:
( 1
< i &
i <= n )
;
:: thesis: Q0 . i = Base_FinSeq K,n,i
B2:
i in Seg n
by B1, FINSEQ_1:3;
B2a:
[i,1] in Indices Q0
by A30, A70, B2, ZFMISC_1:106;
consider p being
FinSequence of
K such that B3:
(
p = Q0 . i &
Q0 * i,1
= p . 1 )
by B2a, MATRIX_1:def 6;
B8:
(
len Q0 = n & ( for
p3 being
FinSequence of
K st
p3 in rng Q0 holds
len p3 = n ) )
by MATRIX_1:def 3;
B8a:
i in Seg (len Q0)
by B1, B8, FINSEQ_1:3;
B8b:
i in dom Q0
by B8a, FINSEQ_1:def 3;
B8c:
p in rng Q0
by B3, B8b, FUNCT_1:def 5;
B20:
len p = n
by B8c, MATRIX_1:def 3;
B21:
len (Base_FinSeq K,n,i) = n
by AA1100;
for
j being
Nat st 1
<= j &
j <= n holds
p . j = (Base_FinSeq K,n,i) . j
proof
let j be
Nat;
:: thesis: ( 1 <= j & j <= n implies p . j = (Base_FinSeq K,n,i) . j )
assume C0:
( 1
<= j &
j <= n )
;
:: thesis: p . j = (Base_FinSeq K,n,i) . j
C2:
[i,j] in Indices Q0
by B1, C0, MATRIX_1:38;
consider p2 being
FinSequence of
K such that B4:
(
p2 = Q0 . i &
Q0 * i,
j = p2 . j )
by C2, MATRIX_1:def 6;
thus
p . j = (Base_FinSeq K,n,i) . j
by A7, B1, C2, B3, B4;
:: thesis: verum
end;
hence
Q0 . i = Base_FinSeq K,
n,
i
by B20, B21, B3, FINSEQ_1:18;
:: thesis: verum
end;
hence
P is invertible
by AA3000, A1, A10, A11; :: thesis: verum