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 that
A1: n > 0 and
A2: ( 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 ) );
A3: 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] )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume [i,j] in [:(Seg n),(Seg n):] ; :: thesis: ex x being Element of K st S1[i,j,x]
then j0 in Seg n by ZFMISC_1:87;
then A4: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;
per cases ( i = 1 or i <> 1 ) ;
suppose A5: i = 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
now :: thesis: ( ( j = 1 & ( i = 1 implies ( ( j = 1 implies a = a ) & ( j <> 1 implies a = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
a = (Base_FinSeq (K,n,i1)) . j ) ) or ( j <> 1 & ( i = 1 implies ( ( j = 1 implies - (a * (P * (1,j))) = a ) & ( j <> 1 implies - (a * (P * (1,j))) = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
- (a * (P * (1,j))) = (Base_FinSeq (K,n,i1)) . j ) ) )
per cases ( j = 1 or j <> 1 ) ;
case A6: j = 1 ; :: thesis: ( ( i = 1 implies ( ( j = 1 implies a = a ) & ( j <> 1 implies a = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
a = (Base_FinSeq (K,n,i1)) . j ) )
set x1 = a;
thus ( ( i = 1 implies ( ( j = 1 implies a = a ) & ( j <> 1 implies a = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
a = (Base_FinSeq (K,n,i1)) . j ) ) by A5, A6; :: thesis: verum
end;
case A7: j <> 1 ; :: thesis: ( ( i = 1 implies ( ( j = 1 implies - (a * (P * (1,j))) = a ) & ( j <> 1 implies - (a * (P * (1,j))) = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
- (a * (P * (1,j))) = (Base_FinSeq (K,n,i1)) . j ) )
set x1 = - (a * (P * (1,j)));
thus ( ( i = 1 implies ( ( j = 1 implies - (a * (P * (1,j))) = a ) & ( j <> 1 implies - (a * (P * (1,j))) = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
- (a * (P * (1,j))) = (Base_FinSeq (K,n,i1)) . j ) ) by A5, A7; :: thesis: verum
end;
end;
end;
hence ex x being Element of K st S1[i,j,x] ; :: thesis: verum
end;
suppose A8: i <> 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
len (Base_FinSeq (K,n,i0)) = n by Th23;
then (Base_FinSeq (K,n,i0)) /. j0 = (Base_FinSeq (K,n,i0)) . j0 by A4, FINSEQ_4:15;
then reconsider x1 = (Base_FinSeq (K,n,i0)) . j0 as Element of K ;
( i <> 1 implies for i1 being Element of NAT st i1 = i holds
x1 = (Base_FinSeq (K,n,i1)) . j ) ;
hence ex x being Element of K st S1[i,j,x] by A8; :: thesis: verum
end;
end;
end;
consider Q0 being Matrix of n,n,K such that
A9: for i, j being Nat st [i,j] in Indices Q0 holds
S1[i,j,Q0 * (i,j)] from MATRIX_0:sch 2(A3);
 A10: 0 + 1 <= n by A1, NAT_1:13;
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 that
A12: 1 < j and
A13: j <= n ; :: thesis: Q0 * (1,j) = - (a * (P * (1,j)))
[1,j] in Indices Q0 by A10, A12, A13, MATRIX_0:31;
hence Q0 * (1,j) = - (a * (P * (1,j))) by A9, A12; :: thesis: verum
end;
A14: ( Indices Q0 = [:(Seg n),(Seg n):] & 1 in Seg n ) by A10, FINSEQ_1:1, MATRIX_0:24;
A15: 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 that
A16: 1 < i and
A17: i <= n ; :: thesis: Q0 . i = Base_FinSeq (K,n,i)
i in Seg n by A16, A17, FINSEQ_1:1;
then [i,1] in Indices Q0 by A14, ZFMISC_1:87;
then consider p being FinSequence of K such that
A18: p = Q0 . i and
Q0 * (i,1) = p . 1 by MATRIX_0:def 5;
A19: 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 ( 1 <= j & j <= n ) ; :: thesis: p . j = (Base_FinSeq (K,n,i)) . j
then A20: [i,j] in Indices Q0 by A16, A17, MATRIX_0:31;
then ex p2 being FinSequence of K st
( p2 = Q0 . i & Q0 * (i,j) = p2 . j ) by MATRIX_0:def 5;
hence p . j = (Base_FinSeq (K,n,i)) . j by A9, A16, A18, A20; :: thesis: verum
end;
len Q0 = n by MATRIX_0:def 2;
then i in Seg (len Q0) by A16, A17, FINSEQ_1:1;
then i in dom Q0 by FINSEQ_1:def 3;
then p in rng Q0 by A18, FUNCT_1:def 3;
then A21: len p = n by MATRIX_0:def 2;
len (Base_FinSeq (K,n,i)) = n by Th23;
hence Q0 . i = Base_FinSeq (K,n,i) by A18, A21, A19, FINSEQ_1:14; :: thesis: verum
end;
[1,1] in Indices Q0 by A10, MATRIX_0:31;
then Q0 * (1,1) = a by A9;
hence P is invertible by A1, A2, A11, A15, Th37; :: thesis: verum