let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st n > 0 & A * 1,1 <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (A * P) * 1,1 = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * 1,j = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P) * i,1 = 0. K ) )
let K be Field; :: thesis: for A being Matrix of n,K st n > 0 & A * 1,1 <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (A * P) * 1,1 = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * 1,j = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P) * i,1 = 0. K ) )
let A be Matrix of n,K; :: thesis: ( n > 0 & A * 1,1 <> 0. K implies ex P being Matrix of n,K st
( P is invertible & (A * P) * 1,1 = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * 1,j = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P) * i,1 = 0. K ) ) )
assume A1: ( n > 0 & A * 1,1 <> 0. K ) ; :: thesis: ex P being Matrix of n,K st
( P is invertible & (A * P) * 1,1 = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * 1,j = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P) * i,1 = 0. K ) )
set a = A * 1,1;
defpred S1[ Nat, Nat, Element of K] means ( ( $1 = 1 implies ( ( $2 = 1 implies $3 = (A * 1,1) " ) & ( $2 <> 1 implies $3 = - (((A * 1,1) " ) * (A * 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;
let x1, x2 be Element of K; :: thesis: ( S1[i,j,x1] & S1[i,j,x2] implies x1 = x2 )
assume B1: ( S1[i,j,x1] & S1[i,j,x2] ) ; :: thesis: x1 = x2
per cases ( i = 1 or i <> 1 ) ;
suppose i = 1 ; :: thesis: x1 = x2
hence x1 = x2 by B1; :: thesis: verum
end;
suppose i <> 1 ; :: thesis: x1 = x2
then ( x1 = (Base_FinSeq K,n,i0) . j & x2 = (Base_FinSeq K,n,i0) . j ) by B1;
hence x1 = x2 ; :: thesis: verum
end;
end;
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;
B1a: ( i0 in Seg n & j0 in Seg n ) by B1, ZFMISC_1:106;
B1b: ( 1 <= i0 & i0 <= n & 1 <= j0 & j0 <= n ) by B1a, 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]
per cases ( j = 1 or j <> 1 ) ;
suppose D0: j = 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
set x1 = (A * 1,1) " ;
thus ex x being Element of K st S1[i,j,x] by C0, D0; :: thesis: verum
end;
suppose D0: j <> 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
set x1 = - (((A * 1,1) " ) * (A * 1,j));
thus ex x being Element of K st S1[i,j,x] by C0, D0; :: thesis: verum
end;
end;
end;
suppose C0: i <> 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
set x1 = (Base_FinSeq K,n,i0) /. j0;
C7: len (Base_FinSeq K,n,i0) = n by AA1100;
for i1 being Element of NAT st i1 = i holds
(Base_FinSeq K,n,i0) /. j0 = (Base_FinSeq K,n,i1) . j by B1b, C7, FINSEQ_4:24;
hence ex x being Element of K st S1[i,j,x] by C0; :: thesis: verum
end;
end;
end;
consider P0 being Matrix of n,n,K such that
A7: for i, j being Nat st [i,j] in Indices P0 holds
S1[i,j,P0 * i,j] from MATRIX_1:sch 2(A5, A6);
 A40: 0 + 1 <= n by A1, NAT_1:13;
A72a: [1,1] in Indices P0 by A40, MATRIX_1:38;
A12: P0 * 1,1 = (A * 1,1) " by A7, A72a;
A91: for i being Element of NAT st 1 < i & i <= n holds
P0 . i = Base_FinSeq K,n,i
proof
let i be Element of NAT ; :: thesis: ( 1 < i & i <= n implies P0 . i = Base_FinSeq K,n,i )
assume B1: ( 1 < i & i <= n ) ; :: thesis: P0 . i = Base_FinSeq K,n,i
B2a: [i,1] in Indices P0 by B1, A40, MATRIX_1:38;
consider p being FinSequence of K such that
B3: ( p = P0 . i & P0 * i,1 = p . 1 ) by B2a, MATRIX_1:def 6;
B8: ( len P0 = n & ( for p3 being FinSequence of K st p3 in rng P0 holds
len p3 = n ) ) by MATRIX_1:def 3;
B9: i in Seg (len P0) by B1, B8, FINSEQ_1:3;
B10: i in dom P0 by B9, FINSEQ_1:def 3;
B11: p in rng P0 by B3, B10, FUNCT_1:def 5;
B20: len p = n by B11, 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 P0 by C0, B1, MATRIX_1:38;
consider p2 being FinSequence of K such that
B4: ( p2 = P0 . i & P0 * 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 P0 . i = Base_FinSeq K,n,i by B20, B21, B3, FINSEQ_1:18; :: thesis: verum
end;
then A71: P0 is invertible by A1, AA3010, A12;
A2d: ( len P0 = n & width P0 = n ) by MATRIX_1:25;
A2a: ( len A = n & width A = n ) by MATRIX_1:25;
A2: len (Line A,1) = n by A2a, MATRIX_1:def 8;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A20: len (Col P0,1) = len P0 by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
A21: len (((A * 1,1) " ) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
A11: 1 in Seg (len P0) by A2d, A40, FINSEQ_1:3;
A8d: Indices P0 = [:(Seg n),(Seg n):] by MATRIX_1:25;
B4e: len (((A * 1,1) " ) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
for k being Nat st 1 <= k & k <= n holds
(Col P0,1) . k = (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col P0,1) . k = (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k )
assume B1: ( 1 <= k & k <= n ) ; :: thesis: (Col P0,1) . k = (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k
then k in Seg n by FINSEQ_1:3;
then B3: k in dom P0 by A2d, FINSEQ_1:def 3;
k in Seg n by B1, FINSEQ_1:3;
then C10d: k in dom (((A * 1,1) " ) * (Base_FinSeq K,n,1)) by B4e, FINSEQ_1:def 3;
1 <= n by B1, XXREAL_0:2;
then B11: 1 in dom P0 by A2d, FINSEQ_3:27;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by B1, A2b, FINSEQ_4:24;
A13a: 1 <= n by B1, XXREAL_0:2;
B5: now
assume C0: k <> 1 ; :: thesis: (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k = 0. K
thus (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k = ((A * 1,1) " ) * ((Base_FinSeq K,n,1) /. k) by C10d, A13, FVSUM_1:62
.= ((A * 1,1) " ) * (0. K) by A13, AA1120, B1, C0, A13a
.= 0. K by VECTSP_1:36 ; :: thesis: verum
end;
B6: now
assume C0: k = 1 ; :: thesis: (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k = (A * 1,1) "
thus (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k = ((A * 1,1) " ) * ((Base_FinSeq K,n,1) /. 1) by C10d, A13, C0, FVSUM_1:62
.= ((A * 1,1) " ) * (1. K) by AA1110, C0, B1, A13
.= (A * 1,1) " by VECTSP_1:def 16 ; :: thesis: verum
end;
now
assume B20: k <> 1 ; :: thesis: (Col P0,1) . k = 0. K
B: k in NAT by ORDINAL1:def 13;
B19: 1 < k by B1, B20, XXREAL_0:1;
B19a: k in Seg n by B1, FINSEQ_1:3;
B19b: [k,1] in Indices P0 by A8d, A11, A2d, B19a, ZFMISC_1:106;
consider p being FinSequence of K such that
C3: ( p = P0 . k & P0 * k,1 = p . 1 ) by B19b, MATRIX_1:def 6;
P0 * k,1 = (Base_FinSeq K,n,k) . 1 by C3, B19, B1, A91, B
.= 0. K by B20, B1, A40, AA1120 ;
hence (Col P0,1) . k = 0. K by B3, MATRIX_1:def 9; :: thesis: verum
end;
hence (Col P0,1) . k = (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k by B5, B6, B11, A12, MATRIX_1:def 9; :: thesis: verum
end;
then A3: Col P0,1 = ((A * 1,1) " ) * (Base_FinSeq K,n,1) by A20, A21, FINSEQ_1:18;
A4: 0 + 1 <= n by A1, NAT_1:13;
then A10: 1 in Seg (width A) by A2a, FINSEQ_1:3;
A11: 1 in Seg (len A) by A2a, A4, FINSEQ_1:3;
K1: 1 in dom A by A11, FINSEQ_1:def 3;
K3: len (((A * 1,1) " ) * (Line A,1)) = len (Line A,1) by MATRIXR1:16
.= n by A2a, MATRIX_1:def 8 ;
K4: 1 in dom (Line A,1) by A11, A2a, A2, FINSEQ_1:def 3;
A8: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:25;
A12b: [1,1] in Indices A by A4, MATRIX_1:38;
Indices (A * P0) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A72: (A * P0) * 1,1 = |((Line A,1),(Col P0,1))| by A12b, A8, A2d, A2a, MATRIX_3:def 4
.= ((A * 1,1) " ) * |((Line A,1),(Base_FinSeq K,n,1))| by A3, BB246, A2, A2b
.= ((A * 1,1) " ) * ((Line A,1) /. 1) by AA2627, A2, A4
.= (((A * 1,1) " ) * (Line A,1)) /. 1 by K4, POLYNOM1:def 2
.= (((A * 1,1) " ) * (Line A,1)) . 1 by K3, A4, FINSEQ_4:24
.= ((A * 1,1) " ) * (A * 1,1) by K1, A10, MATRIX12:3
.= 1. K by A1, VECTSP_1:def 22 ;
A73: for j being Element of NAT st 1 < j & j <= n holds
(A * P0) * 1,j = 0. K
proof
let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (A * P0) * 1,j = 0. K )
assume B1: ( 1 < j & j <= n ) ; :: thesis: (A * P0) * 1,j = 0. K
then B20: j in Seg n by FINSEQ_1:3;
A22: [1,j] in Indices (A * P0) by B1, A40, MATRIX_1:38;
A22b: [1,j] in Indices P0 by B1, A40, MATRIX_1:38;
B3: len (Col P0,j) = len P0 by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4: len (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) = len ((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)) by BB200
.= len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B4d: len ((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
B5b: len (Base_FinSeq K,n,j) = n by AA1100;
then B5: len ((- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j)) = n by B4, Th6;
reconsider p = Col P0,j, q = (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) as FinSequence of K ;
for k being Nat st 1 <= k & k <= n holds
p . k = q . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
A4: 0 + 1 <= n by C0, NAT_1:13;
k in Seg n by C0, FINSEQ_1:3;
then C10b: k in dom ((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)) by B4d, FINSEQ_1:def 3;
C10a: len ((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
C12: k in dom P0 by C0, A2d, FINSEQ_3:27;
C2: p . k = P0 * k,j by C12, MATRIX_1:def 9;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) . k = ((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)) . k by BB200
.= (- (((A * 1,1) " ) * (A * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C10b, A13, FVSUM_1:62 ;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;
suppose D0: 1 = k ; :: thesis: p . k = q . k
then D2: p . k = - (((A * 1,1) " ) * (A * 1,j)) by A7, B1, A22b, C2;
K3: ( 1 <= k & k <= len (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) ) by C0, C10a, BB200;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by D0, B1, AA1120, C0 ;
D1: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- (((A * 1,1) " ) * (A * 1,j))) * ((Base_FinSeq K,n,1) /. k) by C4, K3, FINSEQ_4:24
.= (- (((A * 1,1) " ) * (A * 1,j))) * (1. K) by D0, AA1110, C0, E1
.= - (((A * 1,1) " ) * (A * 1,j)) by VECTSP_1:def 16 ;
q . k = (- (((A * 1,1) " ) * (A * 1,j))) + (0. K) by D1, BB120, B4, B5b, C0, K1;
hence p . k = q . k by D2, RLVECT_1:10; :: thesis: verum
end;
suppose D0: 1 < k ; :: thesis: p . k = q . k
D1: [k,j] in Indices P0 by B1, C0, MATRIX_1:38;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . j by A7, D0, D1, B, C2;
per cases ( k <> j or k = j ) ;
suppose E0: k <> j ; :: thesis: p . k = q . k
then E2: p . k = 0. K by D2, AA1120, B1, C0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 0. K by B1, AA1120, C0, E0 ;
K2: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (((A * 1,1) " ) * (A * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (0. K) by E3, BB120, B4, B5b, C0, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum
end;
suppose E0: k = j ; :: thesis: p . k = q . k
E2: p . k = 1. K by D2, AA1110, C0, E0;
A3a: len (Base_FinSeq K,n,1) = n by AA1100;
E1: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A3a, FINSEQ_4:24;
K1: (Base_FinSeq K,n,j) /. k = (Base_FinSeq K,n,j) . k by B5b, C0, FINSEQ_4:24
.= 1. K by AA1110, C0, E0 ;
K2: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) /. k = (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) . k by B4, C0, FINSEQ_4:24;
E3: (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) . k = (- (((A * 1,1) " ) * (A * 1,j))) * (0. K) by D0, AA1120, A4, C0, E1, C4
.= 0. K by VECTSP_1:36 ;
q . k = (0. K) + (1. K) by BB120, B4, B5b, C0, E3, K1, K2;
hence p . k = q . k by E2, RLVECT_1:10; :: thesis: verum
end;
end;
end;
end;
end;
then B7: Col P0,j = (- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))) + (Base_FinSeq K,n,j) by B3, B5, FINSEQ_1:18;
A2a: ( len A = n & width A = n ) by MATRIX_1:25;
K2: len (Line A,1) = n by A2a, MATRIX_1:def 8;
K3: (Line A,1) /. j = (Line A,1) . j by K2, B1, FINSEQ_4:24
.= A * 1,j by B20, A2a, MATRIX_1:def 8 ;
K0: (Line A,1) /. 1 = (Line A,1) . 1 by K2, A4, FINSEQ_4:24
.= A * 1,1 by A10, MATRIX_1:def 8 ;
(A * P0) * 1,j = |((Line A,1),(Col P0,j))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line A,1),(- ((((A * 1,1) " ) * (A * 1,j)) * (Base_FinSeq K,n,1))))| + |((Line A,1),(Base_FinSeq K,n,j))| by BB248, B4, A2, B7, B5b
.= |((Line A,1),((- (((A * 1,1) " ) * (A * 1,j))) * (Base_FinSeq K,n,1)))| + |((Line A,1),(Base_FinSeq K,n,j))| by BB200
.= ((- (((A * 1,1) " ) * (A * 1,j))) * |((Line A,1),(Base_FinSeq K,n,1))|) + |((Line A,1),(Base_FinSeq K,n,j))| by BB246, A2, A2b
.= ((- (((A * 1,1) " ) * (A * 1,j))) * (A * 1,1)) + |((Line A,1),(Base_FinSeq K,n,j))| by K0, AA2627, A2, A4
.= (- ((((A * 1,1) " ) * (A * 1,j)) * (A * 1,1))) + |((Line A,1),(Base_FinSeq K,n,j))| by VECTSP_1:41
.= (- ((A * 1,j) * (((A * 1,1) " ) * (A * 1,1)))) + |((Line A,1),(Base_FinSeq K,n,j))| by GROUP_1:def 4
.= (- ((A * 1,j) * (1. K))) + |((Line A,1),(Base_FinSeq K,n,j))| by A1, VECTSP_1:def 22
.= (- ((A * 1,j) * (1. K))) + ((Line A,1) /. j) by AA2627, B1, A2
.= (- (A * 1,j)) + (A * 1,j) by K3, VECTSP_1:def 16
.= 0. K by RLVECT_1:16 ;
hence (A * P0) * 1,j = 0. K ; :: thesis: verum
end;
for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P0) * i,1 = 0. K
proof
let i be Element of NAT ; :: thesis: ( 1 < i & i <= n & A * i,1 = 0. K implies (A * P0) * i,1 = 0. K )
assume B0: ( 1 < i & i <= n & A * i,1 = 0. K ) ; :: thesis: (A * P0) * i,1 = 0. K
set Q = A;
set P = P0;
B1: 1 <= n by B0, XXREAL_0:2;
A22: [i,1] in Indices (A * P0) by B0, B1, MATRIX_1:38;
B3: len (Col P0,1) = len P0 by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
B4b: len (((A * 1,1) " ) * (Base_FinSeq K,n,1)) = len (Base_FinSeq K,n,1) by MATRIXR1:16
.= n by AA1100 ;
reconsider p = Col P0,1, q = ((A * 1,1) " ) * (Base_FinSeq K,n,1) as FinSequence of K ;
F2: for k being Nat st 1 <= k & k <= n holds
p . k = q . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume C0: ( 1 <= k & k <= n ) ; :: thesis: p . k = q . k
C113: k in dom (((A * 1,1) " ) * (Base_FinSeq K,n,1)) by C0, B4b, FINSEQ_3:27;
C12: k in dom P0 by C0, A2d, FINSEQ_3:27;
C2: p . k = P0 * k,1 by C12, MATRIX_1:def 9;
A2b: len (Base_FinSeq K,n,1) = n by AA1100;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
C4: (((A * 1,1) " ) * (Base_FinSeq K,n,1)) . k = ((A * 1,1) " ) * ((Base_FinSeq K,n,1) /. k) by C113, A13, FVSUM_1:62;
per cases ( 1 = k or 1 < k ) by C0, XXREAL_0:1;
suppose D0: 1 = k ; :: thesis: p . k = q . k
q . k = ((A * 1,1) " ) * (1. K) by C4, D0, AA1110, C0, A13
.= (A * 1,1) " by VECTSP_1:def 16 ;
hence p . k = q . k by A7, A72a, C2, D0; :: thesis: verum
end;
suppose D0: 1 < k ; :: thesis: p . k = q . k
[k,1] in Indices P0 by B1, C0, MATRIX_1:38;
then consider p2 being FinSequence of K such that
D3: ( p2 = P0 . k & P0 * k,1 = p2 . 1 ) by MATRIX_1:def 6;
B: k in NAT by ORDINAL1:def 13;
D2: p . k = (Base_FinSeq K,n,k) . 1 by A91, D0, C0, D3, B, C2;
A13: (Base_FinSeq K,n,1) /. k = (Base_FinSeq K,n,1) . k by C0, A2b, FINSEQ_4:24;
A13a: 1 <= n by C0, XXREAL_0:2;
((A * 1,1) " ) * ((Base_FinSeq K,n,1) /. k) = ((A * 1,1) " ) * (0. K) by A13, AA1120, D0, C0, A13a
.= 0. K by VECTSP_1:36 ;
hence p . k = q . k by D0, D2, AA1120, B1, C0, C4; :: thesis: verum
end;
end;
end;
A2a: ( len A = n & width A = n ) by MATRIX_1:25;
K2: len (Line A,i) = n by A2a, MATRIX_1:def 8;
K0: (Line A,i) /. 1 = (Line A,i) . 1 by K2, A4, FINSEQ_4:24
.= A * i,1 by A10, MATRIX_1:def 8 ;
thus (A * P0) * i,1 = |((Line A,i),(Col P0,1))| by A2a, A2d, A22, MATRIX_3:def 4
.= |((Line A,i),(((A * 1,1) " ) * (Base_FinSeq K,n,1)))| by F2, B3, B4b, FINSEQ_1:18
.= ((A * 1,1) " ) * |((Line A,i),(Base_FinSeq K,n,1))| by BB246, K2, A2b
.= ((A * 1,1) " ) * (A * i,1) by K0, AA2627, K2, A4
.= 0. K by B0, VECTSP_1:36 ; :: thesis: verum
end;
hence ex P being Matrix of n,K st
( P is invertible & (A * P) * 1,1 = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * 1,j = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * i,1 = 0. K holds
(A * P) * i,1 = 0. K ) ) by A71, A72, A73; :: thesis: verum