let n be Element of NAT ; for K being Field
for A, B being Matrix of n,K st B * A = 1. (K,n) holds
ex B2 being Matrix of n,K st A * B2 = 1. (K,n)
let K be Field; for A, B being Matrix of n,K st B * A = 1. (K,n) holds
ex B2 being Matrix of n,K st A * B2 = 1. (K,n)
let A, B be Matrix of n,K; ( B * A = 1. (K,n) implies ex B2 being Matrix of n,K st A * B2 = 1. (K,n) )
thus
( B * A = 1. (K,n) implies ex B2 being Matrix of n,K st A * B2 = 1. (K,n) )
verumproof
defpred S1[
Nat]
means for
D,
B3 being
Matrix of $1,
K st
B3 * D = 1. (
K,$1) holds
ex
B4 being
Matrix of $1,
K st
D * B4 = 1. (
K,$1);
assume A1:
B * A = 1. (
K,
n)
;
ex B2 being Matrix of n,K st A * B2 = 1. (K,n)
A2:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
for
A2,
B3 being
Matrix of
k + 1,
K st
B3 * A2 = 1. (
K,
(k + 1)) holds
ex
B4 being
Matrix of
k + 1,
K st
A2 * B4 = 1. (
K,
(k + 1))
proof
let A2,
B2 be
Matrix of
k + 1,
K;
( B2 * A2 = 1. (K,(k + 1)) implies ex B4 being Matrix of k + 1,K st A2 * B4 = 1. (K,(k + 1)) )
A4:
Indices (1. (K,(k + 1))) = [:(Seg (k + 1)),(Seg (k + 1)):]
by MATRIX_0:24;
assume A5:
B2 * A2 = 1. (
K,
(k + 1))
;
ex B4 being Matrix of k + 1,K st A2 * B4 = 1. (K,(k + 1))
then A6:
(Det B2) * (Det A2) = Det (1. (K,(k + 1)))
by MATRIXR2:45;
then consider B,
C being
Matrix of
k + 1,
K such that A8:
B is
invertible
and A9:
C is
invertible
and A10:
((B * A2) * C) * (1,1)
= 1. K
and A11:
for
i being
Element of
NAT st 1
< i &
i <= k + 1 holds
((B * A2) * C) * (
i,1)
= 0. K
and A12:
for
j being
Element of
NAT st 1
< j &
j <= k + 1 holds
((B * A2) * C) * (1,
j)
= 0. K
by Th53;
set A3 =
(B * A2) * C;
set B3 =
((C ~) * B2) * (B ~);
A13:
width (((C ~) * B2) * (B ~)) = k + 1
by MATRIX_0:24;
A14:
width ((B * A2) * C) = k + 1
by MATRIX_0:24;
A15:
for
j being
Nat st 1
<= j &
j <= len (Line (((B * A2) * C),1)) holds
(Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
proof
let j be
Nat;
( 1 <= j & j <= len (Line (((B * A2) * C),1)) implies (Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j )
assume that A16:
1
<= j
and A17:
j <= len (Line (((B * A2) * C),1))
;
(Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
A18:
j <= k + 1
by A14, A17, MATRIX_0:def 7;
len (Line (((B * A2) * C),1)) = width ((B * A2) * C)
by MATRIX_0:def 7;
then A19:
j in Seg (width ((B * A2) * C))
by A16, A17, FINSEQ_1:1;
per cases
( 1 = j or 1 < j )
by A16, XXREAL_0:1;
suppose A21:
1
< j
;
(Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . jA22:
j in NAT
by ORDINAL1:def 12;
(Line (((B * A2) * C),1)) . j =
((B * A2) * C) * (1,
j)
by A19, MATRIX_0:def 7
.=
0. K
by A12, A18, A21, A22
;
hence
(Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
by A18, A21, Th25;
verum end; end;
end;
A23:
len <*(0. K)*> = 1
by FINSEQ_1:40;
deffunc H1(
Nat,
Nat)
-> Element of the
carrier of
K =
((B * A2) * C) * (
($1 + 1),
($2 + 1));
A24:
len (A2 * C) = k + 1
by MATRIX_0:24;
consider F being
Matrix of
k,
k,
K such that A25:
for
i,
j being
Nat st
[i,j] in Indices F holds
F * (
i,
j)
= H1(
i,
j)
from MATRIX_0:sch 1();
A26:
len F = k
by MATRIX_0:24;
deffunc H2(
Nat,
Nat)
-> Element of the
carrier of
K =
(((C ~) * B2) * (B ~)) * (
($1 + 1),
($2 + 1));
A27:
len C = k + 1
by MATRIX_0:24;
consider G being
Matrix of
k,
k,
K such that A28:
for
i,
j being
Nat st
[i,j] in Indices G holds
G * (
i,
j)
= H2(
i,
j)
from MATRIX_0:sch 1();
A29:
len ((B * A2) * C) = k + 1
by MATRIX_0:24;
A30:
(((C ~) * B2) * (B ~)) * ((B * A2) * C) =
(((C ~) * B2) * (B ~)) * (B * (A2 * C))
by Th17
.=
((((Inv C) * B2) * (Inv B)) * B) * (A2 * C)
by Th17
.=
(((Inv C) * B2) * ((Inv B) * B)) * (A2 * C)
by Th17
.=
(((Inv C) * B2) * (1. (K,(k + 1)))) * (A2 * C)
by A8, Th18
.=
((Inv C) * B2) * ((1. (K,(k + 1))) * (A2 * C))
by Th17
.=
((Inv C) * B2) * (A2 * C)
by A24, MATRIXR2:68
.=
(((Inv C) * B2) * A2) * C
by Th17
.=
((Inv C) * (1. (K,(k + 1)))) * C
by A5, Th17
.=
(Inv C) * ((1. (K,(k + 1))) * C)
by Th17
.=
(Inv C) * C
by A27, MATRIXR2:68
.=
1. (
K,
(k + 1))
by A9, Th18
;
A31:
for
i being
Nat st 1
< i &
i <= k + 1 holds
(((C ~) * B2) * (B ~)) * (
i,1)
= (1. (K,(k + 1))) * (
i,1)
proof
A32:
len (Base_FinSeq (K,(k + 1),1)) = k + 1
by Th23;
let i be
Nat;
( 1 < i & i <= k + 1 implies (((C ~) * B2) * (B ~)) * (i,1) = (1. (K,(k + 1))) * (i,1) )
A33:
len (Col (((B * A2) * C),1)) =
len ((B * A2) * C)
by MATRIX_0:def 8
.=
k + 1
by MATRIX_0:24
;
A34:
len ((B * A2) * C) = k + 1
by MATRIX_0:24;
A35:
for
k2 being
Nat st 1
<= k2 &
k2 <= len (Col (((B * A2) * C),1)) holds
(Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2
proof
let k2 be
Nat;
( 1 <= k2 & k2 <= len (Col (((B * A2) * C),1)) implies (Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2 )
assume that A36:
1
<= k2
and A37:
k2 <= len (Col (((B * A2) * C),1))
;
(Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2
A38:
k2 in NAT
by ORDINAL1:def 12;
k2 in Seg (len ((B * A2) * C))
by A34, A33, A36, A37, FINSEQ_1:1;
then
k2 in dom ((B * A2) * C)
by FINSEQ_1:def 3;
hence
(Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2
by A39, MATRIX_0:def 8;
verum
end;
A41:
len (Line ((((C ~) * B2) * (B ~)),i)) =
width (((C ~) * B2) * (B ~))
by MATRIX_0:def 7
.=
k + 1
by MATRIX_0:24
;
assume A42:
( 1
< i &
i <= k + 1 )
;
(((C ~) * B2) * (B ~)) * (i,1) = (1. (K,(k + 1))) * (i,1)
then A43:
1
<= k + 1
by XXREAL_0:2;
A44:
width (((C ~) * B2) * (B ~)) = k + 1
by MATRIX_0:24;
then A45:
1
in Seg (width (((C ~) * B2) * (B ~)))
by A43, FINSEQ_1:1;
[i,1] in Indices ((((C ~) * B2) * (B ~)) * ((B * A2) * C))
by A42, A43, MATRIX_0:31;
then ((((C ~) * B2) * (B ~)) * ((B * A2) * C)) * (
i,1) =
|((Line ((((C ~) * B2) * (B ~)),i)),(Col (((B * A2) * C),1)))|
by A44, A34, MATRIX_3:def 4
.=
|((Line ((((C ~) * B2) * (B ~)),i)),(Base_FinSeq (K,(k + 1),1)))|
by A33, A32, A35, FINSEQ_1:14
.=
(Line ((((C ~) * B2) * (B ~)),i)) . 1
by A43, A41, Th35
.=
(((C ~) * B2) * (B ~)) * (
i,1)
by A45, MATRIX_0:def 7
;
hence
(((C ~) * B2) * (B ~)) * (
i,1)
= (1. (K,(k + 1))) * (
i,1)
by A30;
verum
end;
A46:
k in NAT
by ORDINAL1:def 12;
for
i,
j being
Nat st 1
<= i &
i <= k & 1
<= j &
j <= k holds
(G * F) * (
i,
j)
= IFEQ (
i,
j,
(1. K),
(0. K))
proof
let i,
j be
Nat;
( 1 <= i & i <= k & 1 <= j & j <= k implies (G * F) * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
assume that A47:
1
<= i
and A48:
i <= k
and A49:
1
<= j
and A50:
j <= k
;
(G * F) * (i,j) = IFEQ (i,j,(1. K),(0. K))
A51:
[i,j] in Indices (G * F)
by A47, A48, A49, A50, MATRIX_0:31;
A52:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2
proof
(
j + 1
<= k + 1 & 1
< j + 1 )
by A49, A50, NAT_1:13, XREAL_1:7;
then A53:
((B * A2) * C) * (1,
(j + 1))
= 0. K
by A12;
let k2 be
Nat;
( k2 in dom <*(0. K)*> implies (Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2 )
assume
k2 in dom <*(0. K)*>
;
(Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2
then
k2 in Seg (len <*(0. K)*>)
by FINSEQ_1:def 3;
then
k2 in {1}
by FINSEQ_1:2, FINSEQ_1:40;
then A54:
k2 = 1
by TARSKI:def 1;
1
<= k + 1
by NAT_1:11;
then
k2 in Seg (len ((B * A2) * C))
by A29, A54, FINSEQ_1:1;
then
k2 in dom ((B * A2) * C)
by FINSEQ_1:def 3;
then
(Col (((B * A2) * C),(j + 1))) . k2 = 0. K
by A54, A53, MATRIX_0:def 8;
hence
(Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2
by A54, FINSEQ_1:40;
verum
end;
A55:
len (Col (F,j)) =
len F
by MATRIX_0:def 8
.=
k
by MATRIX_0:24
;
A56:
i + 1
<= k + 1
by A48, XREAL_1:7;
A57:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2
proof
let k2 be
Nat;
( k2 in dom <*(0. K)*> implies (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2 )
A58:
1
< i + 1
by A47, NAT_1:13;
1
<= 1
+ k
by NAT_1:11;
then A59:
[(i + 1),1] in Indices (1. (K,(k + 1)))
by A56, A58, MATRIX_0:31;
A60:
(((C ~) * B2) * (B ~)) * (
(i + 1),1) =
(1. (K,(k + 1))) * (
(i + 1),1)
by A31, A56, A58
.=
0. K
by A58, A59, MATRIX_1:def 3
;
assume
k2 in dom <*(0. K)*>
;
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2
then
k2 in Seg (len <*(0. K)*>)
by FINSEQ_1:def 3;
then
k2 in {1}
by FINSEQ_1:2, FINSEQ_1:40;
then A61:
k2 = 1
by TARSKI:def 1;
1
<= k + 1
by NAT_1:11;
then
k2 in Seg (width (((C ~) * B2) * (B ~)))
by A13, A61, FINSEQ_1:1;
then
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = 0. K
by A61, A60, MATRIX_0:def 7;
hence
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2
by A61, FINSEQ_1:40;
verum
end;
A62:
for
k2 being
Nat st
k2 in dom (Col (F,j)) holds
(Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2
proof
reconsider j0 =
j + 1 as
Element of
NAT ;
let k2 be
Nat;
( k2 in dom (Col (F,j)) implies (Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2 )
A63:
len (Col (F,(j0 -' 1))) = len F
by MATRIX_0:def 8;
A64:
j0 -' 1
= j
by NAT_D:34;
assume A65:
k2 in dom (Col (F,j))
;
(Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2
then A66:
k2 in Seg (len (Col (F,(j0 -' 1))))
by A64, FINSEQ_1:def 3;
then A67:
k2 <= k
by A26, A63, FINSEQ_1:1;
then
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by NAT_1:11, XREAL_1:7;
then A68:
k2 + 1
in dom ((B * A2) * C)
by A29, FINSEQ_3:25;
1
<= k2
by A66, FINSEQ_1:1;
then
[k2,j] in Indices F
by A49, A50, A67, MATRIX_0:31;
then
[k2,(j0 -' 1)] in Indices F
by NAT_D:34;
then A69:
((B * A2) * C) * (
(k2 + 1),
((j0 -' 1) + 1))
= F * (
k2,
(j0 -' 1))
by A25;
k2 in Seg k
by A26, A65, A63, A64, FINSEQ_1:def 3;
then
k2 in dom F
by A26, FINSEQ_1:def 3;
then
((B * A2) * C) * (
(k2 + 1),
((j0 -' 1) + 1))
= (Col (F,(j0 -' 1))) . k2
by A69, MATRIX_0:def 8;
hence
(Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2
by A23, A64, A68, MATRIX_0:def 8;
verum
end;
A70:
len (Line (G,i)) =
width G
by MATRIX_0:def 7
.=
k
by MATRIX_0:24
;
A71:
k + 1
= (len <*(0. K)*>) + k
by FINSEQ_1:39;
A72:
for
k2 being
Nat st
k2 in dom (Line (G,i)) holds
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2
proof
let k2 be
Nat;
( k2 in dom (Line (G,i)) implies (Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2 )
A73:
(
width (((C ~) * B2) * (B ~)) = k + 1 & 1
<= k2 + 1 )
by MATRIX_0:24, NAT_1:11;
assume A74:
k2 in dom (Line (G,i))
;
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2
then A75:
k2 in Seg (len (Line (G,i)))
by FINSEQ_1:def 3;
A76:
len (Line (G,i)) =
width G
by MATRIX_0:def 7
.=
k
by MATRIX_0:24
;
then A77:
k2 <= k
by A75, FINSEQ_1:1;
1
<= k2
by A75, FINSEQ_1:1;
then
[i,k2] in Indices G
by A47, A48, A77, MATRIX_0:31;
then A78:
(((C ~) * B2) * (B ~)) * (
(i + 1),
(k2 + 1))
= G * (
i,
k2)
by A28;
k2 in Seg k
by A74, A76, FINSEQ_1:def 3;
then
k2 in Seg (width G)
by MATRIX_0:24;
then A79:
(((C ~) * B2) * (B ~)) * (
(i + 1),
(k2 + 1))
= (Line (G,i)) . k2
by A78, MATRIX_0:def 7;
k2 + 1
<= k + 1
by A77, XREAL_1:7;
then
k2 + 1
in Seg (width (((C ~) * B2) * (B ~)))
by A73, FINSEQ_1:1;
then
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . (k2 + 1) = (Line (G,i)) . k2
by A79, MATRIX_0:def 7;
hence
(Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2
by FINSEQ_1:40;
verum
end;
A80:
width G = k
by MATRIX_0:24;
(
len (Line ((((C ~) * B2) * (B ~)),(i + 1))) = width (((C ~) * B2) * (B ~)) &
len (Line (G,i)) = width G )
by MATRIX_0:def 7;
then
dom (Line ((((C ~) * B2) * (B ~)),(i + 1))) = Seg ((len <*(0. K)*>) + (len (Line (G,i))))
by A13, A80, A71, FINSEQ_1:def 3;
then A81:
<*(0. K)*> ^ (Line (G,i)) = Line (
(((C ~) * B2) * (B ~)),
(i + 1))
by A57, A72, FINSEQ_1:def 7;
A82:
( 1
<= i + 1 & 1
<= j + 1 )
by NAT_1:11;
A83:
j + 1
<= k + 1
by A50, XREAL_1:7;
A84:
now (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))per cases
( i = j or i <> j )
;
suppose A85:
i = j
;
(1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))
[(i + 1),(j + 1)] in Indices (1. (K,(k + 1)))
by A82, A56, A83, MATRIX_0:31;
then
(1. (K,(k + 1))) * (
(i + 1),
(j + 1))
= 1. K
by A85, MATRIX_1:def 3;
hence
(1. (K,(k + 1))) * (
(i + 1),
(j + 1))
= IFEQ (
i,
j,
(1. K),
(0. K))
by A85, FUNCOP_1:def 8;
verum end; suppose A86:
i <> j
;
(1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))
[(i + 1),(j + 1)] in Indices (1. (K,(k + 1)))
by A82, A56, A83, MATRIX_0:31;
then
(
i + 1
<> j + 1 implies
(1. (K,(k + 1))) * (
(i + 1),
(j + 1))
= 0. K )
by MATRIX_1:def 3;
hence
(1. (K,(k + 1))) * (
(i + 1),
(j + 1))
= IFEQ (
i,
j,
(1. K),
(0. K))
by A86, FUNCOP_1:def 8;
verum end; end; end;
(
len (Col (((B * A2) * C),(j + 1))) = len ((B * A2) * C) &
len (Col (F,j)) = len F )
by MATRIX_0:def 8;
then
dom (Col (((B * A2) * C),(j + 1))) = Seg ((len <*(0. K)*>) + (len (Col (F,j))))
by A29, A26, A71, FINSEQ_1:def 3;
then A87:
<*(0. K)*> ^ (Col (F,j)) = Col (
((B * A2) * C),
(j + 1))
by A52, A62, FINSEQ_1:def 7;
[(i + 1),(j + 1)] in Indices ((((C ~) * B2) * (B ~)) * ((B * A2) * C))
by A82, A56, A83, MATRIX_0:31;
then ((((C ~) * B2) * (B ~)) * ((B * A2) * C)) * (
(i + 1),
(j + 1)) =
|((Line ((((C ~) * B2) * (B ~)),(i + 1))),(Col (((B * A2) * C),(j + 1))))|
by A13, A29, MATRIX_3:def 4
.=
|(<*(0. K)*>,<*(0. K)*>)| + |((Line (G,i)),(Col (F,j)))|
by A23, A81, A87, A70, A55, Th12
.=
(0. K) + |((Line (G,i)),(Col (F,j)))|
by Th22
.=
|((Line (G,i)),(Col (F,j)))|
by RLVECT_1:4
;
hence
(G * F) * (
i,
j)
= IFEQ (
i,
j,
(1. K),
(0. K))
by A30, A26, A51, A80, A84, MATRIX_3:def 4;
verum
end;
then
G * F = 1. (
K,
k)
by Th29, A46;
then consider G2 being
Matrix of
k,
K such that A88:
F * G2 = 1. (
K,
k)
by A3;
deffunc H3(
Nat,
Nat)
-> Element of the
carrier of
K =
IFEQ ($1,1,
(IFEQ ($2,1,(1. K),(0. K))),
(IFEQ ($2,1,(0. K),(G2 * (($1 -' 1),($2 -' 1))))));
A89:
len G2 = k
by MATRIX_0:24;
consider B4 being
Matrix of
k + 1,
k + 1,
K such that A90:
for
i,
j being
Nat st
[i,j] in Indices B4 holds
B4 * (
i,
j)
= H3(
i,
j)
from MATRIX_0:sch 1();
A91:
len B4 = k + 1
by MATRIX_0:24;
A92:
width B4 = k + 1
by MATRIX_0:24;
A93:
for
j being
Nat st 1
<= j &
j <= len (Col (B4,1)) holds
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
proof
let j be
Nat;
( 1 <= j & j <= len (Col (B4,1)) implies (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j )
assume that A94:
1
<= j
and A95:
j <= len (Col (B4,1))
;
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
A96:
j <= k + 1
by A91, A95, MATRIX_0:def 8;
then
1
<= k + 1
by A94, XXREAL_0:2;
then A97:
[j,1] in Indices B4
by A94, A96, MATRIX_0:31;
len (Col (B4,1)) = len B4
by MATRIX_0:def 8;
then
j in Seg (width B4)
by A91, A92, A94, A95, FINSEQ_1:1;
then A98:
j in dom B4
by A91, A92, FINSEQ_1:def 3;
per cases
( 1 = j or 1 < j )
by A94, XXREAL_0:1;
suppose A99:
1
= j
;
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j(Col (B4,1)) . j =
B4 * (
j,1)
by A98, MATRIX_0:def 8
.=
IFEQ (
j,1,
(IFEQ (1,1,(1. K),(0. K))),
(IFEQ (1,1,(0. K),(G2 * ((j -' 1),(1 -' 1))))))
by A90, A97
.=
IFEQ (1,1,
(1. K),
(0. K))
by A99, FUNCOP_1:def 8
.=
1. K
by FUNCOP_1:def 8
;
hence
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
by A96, A99, Th24;
verum end; suppose A100:
1
< j
;
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j(Col (B4,1)) . j =
B4 * (
j,1)
by A98, MATRIX_0:def 8
.=
IFEQ (
j,1,
(IFEQ (1,1,(1. K),(0. K))),
(IFEQ (1,1,(0. K),(G2 * ((j -' 1),(1 -' 1))))))
by A90, A97
.=
IFEQ (1,1,
(0. K),
(G2 * ((j -' 1),(1 -' 1))))
by A100, FUNCOP_1:def 8
.=
0. K
by FUNCOP_1:def 8
;
hence
(Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
by A96, A100, Th25;
verum end; end;
end;
A101:
width (((B * A2) * C) * B4) = k + 1
by MATRIX_0:24;
A102:
Indices (((B * A2) * C) * B4) = [:(Seg (k + 1)),(Seg (k + 1)):]
by MATRIX_0:24;
len (Line (((B * A2) * C),1)) =
width ((B * A2) * C)
by MATRIX_0:def 7
.=
k + 1
by MATRIX_0:24
;
then A103:
len (Line (((B * A2) * C),1)) = len (Base_FinSeq (K,(k + 1),1))
by Th23;
then A104:
Line (
((B * A2) * C),1)
= Base_FinSeq (
K,
(k + 1),1)
by A15, FINSEQ_1:14;
A105:
width F = k
by MATRIX_0:24;
A106:
1
<= k + 1
by NAT_1:11;
len (Col (B4,1)) =
len B4
by MATRIX_0:def 8
.=
k + 1
by MATRIX_0:24
;
then A107:
len (Col (B4,1)) = len (Base_FinSeq (K,(k + 1),1))
by Th23;
then A108:
Col (
B4,1)
= Base_FinSeq (
K,
(k + 1),1)
by A93, FINSEQ_1:14;
for
i,
j being
Nat st
[i,j] in Indices (((B * A2) * C) * B4) holds
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
proof
let i,
j be
Nat;
( [i,j] in Indices (((B * A2) * C) * B4) implies (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) )
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 12;
A109:
len (Line (F,(i -' 1))) =
width F
by MATRIX_0:def 7
.=
k
by MATRIX_0:24
;
A110:
len (Col (G2,(j -' 1))) =
len G2
by MATRIX_0:def 8
.=
k
by MATRIX_0:24
;
A111:
len (Line (((B * A2) * C),i)) =
width ((B * A2) * C)
by MATRIX_0:def 7
.=
k + 1
by MATRIX_0:24
;
A112:
len (Col (B4,j)) =
len B4
by MATRIX_0:def 8
.=
k + 1
by MATRIX_0:24
;
assume A113:
[i,j] in Indices (((B * A2) * C) * B4)
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)
then A114:
[i,j] in [:(Seg (k + 1)),(Seg (k + 1)):]
by MATRIX_0:24;
then A115:
[i,j] in Indices (1. (K,(k + 1)))
by MATRIX_0:24;
A116:
i in Seg (k + 1)
by A102, A113, ZFMISC_1:87;
then A117:
1
<= i
by FINSEQ_1:1;
A118:
i <= k + 1
by A116, FINSEQ_1:1;
A119:
j in Seg (k + 1)
by A101, A113, ZFMISC_1:87;
then A120:
1
<= j
by FINSEQ_1:1;
A121:
len B4 = k + 1
by MATRIX_0:24;
A122:
width ((B * A2) * C) = k + 1
by MATRIX_0:24;
A123:
j <= k + 1
by A119, FINSEQ_1:1;
A124:
[i,j] in Indices B4
by A102, A113, MATRIX_0:24;
now (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)per cases
( i = 1 or 1 < i )
by A117, XXREAL_0:1;
suppose A125:
i = 1
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)now (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)per cases
( j = 1 or j > 1 )
by A120, XXREAL_0:1;
suppose A126:
j = 1
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)(((B * A2) * C) * B4) * (
i,
j) =
|((Line (((B * A2) * C),i0)),(Col (B4,j0)))|
by A113, A121, A122, MATRIX_3:def 4
.=
1. K
by A104, A108, A106, A125, A126, Th36
;
hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
by A115, A125, A126, MATRIX_1:def 3;
verum end; suppose A127:
j > 1
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)
1
<= len B4
by A106, MATRIX_0:24;
then A128:
1
in dom B4
by FINSEQ_3:25;
(((B * A2) * C) * B4) * (
i,
j) =
|((Line (((B * A2) * C),i0)),(Col (B4,j0)))|
by A113, A121, A122, MATRIX_3:def 4
.=
|((Base_FinSeq (K,(k + 1),1)),(Col (B4,j0)))|
by A103, A15, A125, FINSEQ_1:14
.=
|((Col (B4,j0)),(Base_FinSeq (K,(k + 1),1)))|
by FVSUM_1:90
.=
(Col (B4,j0)) . 1
by A106, A112, Th35
.=
B4 * (1,
j)
by A128, MATRIX_0:def 8
.=
IFEQ (
i,1,
(IFEQ (j,1,(1. K),(0. K))),
(IFEQ (j,1,(0. K),(G2 * ((i -' 1),(j -' 1))))))
by A90, A124, A125
.=
IFEQ (
j,1,
(1. K),
(0. K))
by A125, FUNCOP_1:def 8
.=
0. K
by A127, FUNCOP_1:def 8
;
hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
by A4, A114, A125, A127, MATRIX_1:def 3;
verum end; end; end; hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
;
verum end; suppose A129:
1
< i
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)then A130:
1
+ 1
<= i
by NAT_1:13;
now (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)per cases
( j = 1 or j > 1 )
by A120, XXREAL_0:1;
suppose A131:
j = 1
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)A132:
1
in Seg (width ((B * A2) * C))
by A14, A106, FINSEQ_1:1;
A133:
len (Line (((B * A2) * C),i)) =
width ((B * A2) * C)
by MATRIX_0:def 7
.=
k + 1
by MATRIX_0:24
;
(((B * A2) * C) * B4) * (
i,
j) =
|((Line (((B * A2) * C),i0)),(Col (B4,j0)))|
by A113, A121, A122, MATRIX_3:def 4
.=
|((Line (((B * A2) * C),i)),(Base_FinSeq (K,(k + 1),1)))|
by A107, A93, A131, FINSEQ_1:14
.=
(Line (((B * A2) * C),i)) . 1
by A106, A133, Th35
.=
((B * A2) * C) * (
i0,1)
by A132, MATRIX_0:def 7
.=
0. K
by A11, A118, A129
;
hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
by A115, A129, A131, MATRIX_1:def 3;
verum end; suppose A134:
j > 1
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)then
1
+ 1
<= j
by NAT_1:13;
then A135:
1
<= j - 1
by XREAL_1:19;
A136:
i -' 1
= i - 1
by A129, XREAL_1:233;
then A137:
i -' 1
<= k
by A118, XREAL_1:20;
A138:
1
<= i - 1
by A130, XREAL_1:19;
then A139:
i -' 1
in Seg k
by A136, A137, FINSEQ_1:1;
A140:
len (Line (F,(i -' 1))) =
width F
by MATRIX_0:def 7
.=
k
by MATRIX_0:24
;
A141:
for
k2 being
Nat st
k2 in dom (Line (F,(i -' 1))) holds
(Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2
proof
let k2 be
Nat;
( k2 in dom (Line (F,(i -' 1))) implies (Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2 )
assume A142:
k2 in dom (Line (F,(i -' 1)))
;
(Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2
then A143:
k2 in Seg (len (Line (F,(i -' 1))))
by FINSEQ_1:def 3;
then A144:
k2 <= k
by A140, FINSEQ_1:1;
then
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by NAT_1:11, XREAL_1:7;
then A145:
k2 + 1
in Seg (width ((B * A2) * C))
by A122, FINSEQ_1:1;
1
<= k2
by A143, FINSEQ_1:1;
then
[(i -' 1),k2] in Indices F
by A136, A138, A137, A144, MATRIX_0:31;
then A146:
((B * A2) * C) * (
((i -' 1) + 1),
(k2 + 1))
= F * (
(i -' 1),
k2)
by A25;
k2 in Seg (width F)
by A105, A140, A142, FINSEQ_1:def 3;
then
((B * A2) * C) * (
((i -' 1) + 1),
(k2 + 1))
= (Line (F,(i -' 1))) . k2
by A146, MATRIX_0:def 7;
then
(Line (((B * A2) * C),((i -' 1) + 1))) . (k2 + 1) = (Line (F,(i -' 1))) . k2
by A145, MATRIX_0:def 7;
hence
(Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2
by FINSEQ_1:40;
verum
end; A147:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2
proof
let k2 be
Nat;
( k2 in dom <*(0. K)*> implies (Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2 )
assume
k2 in dom <*(0. K)*>
;
(Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2
then
k2 in Seg (len <*(0. K)*>)
by FINSEQ_1:def 3;
then
k2 in {1}
by FINSEQ_1:2, FINSEQ_1:40;
then A148:
k2 = 1
by TARSKI:def 1;
A149:
((B * A2) * C) * (
i0,1)
= 0. K
by A11, A118, A129;
1
<= k + 1
by NAT_1:11;
then
k2 in Seg (width ((B * A2) * C))
by A122, A148, FINSEQ_1:1;
then
(Line (((B * A2) * C),i)) . k2 = 0. K
by A148, A149, MATRIX_0:def 7;
hence
(Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2
by A136, A148, FINSEQ_1:40;
verum
end; dom (Line (((B * A2) * C),((i -' 1) + 1))) =
Seg (k + 1)
by A111, A136, FINSEQ_1:def 3
.=
Seg ((len <*(0. K)*>) + (len (Line (F,(i -' 1)))))
by A140, FINSEQ_1:39
;
then A150:
<*(0. K)*> ^ (Line (F,(i -' 1))) = Line (
((B * A2) * C),
((i -' 1) + 1))
by A147, A141, FINSEQ_1:def 7;
A151:
(j -' 1) + 1 =
(j - 1) + 1
by A134, XREAL_1:233
.=
j
;
A152:
j -' 1
= j - 1
by A134, XREAL_1:233;
then
j -' 1
<= k
by A123, XREAL_1:20;
then
j -' 1
in Seg k
by A152, A135, FINSEQ_1:1;
then A153:
[(i -' 1),(j -' 1)] in [:(Seg k),(Seg k):]
by A139, ZFMISC_1:87;
then A154:
[(i -' 1),(j -' 1)] in Indices (F * G2)
by MATRIX_0:24;
A155:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2
proof
1
<= 1
+ k
by NAT_1:11;
then
[1,j] in Indices B4
by A120, A123, MATRIX_0:31;
then
B4 * (1,
j)
= IFEQ (1,1,
(IFEQ (j,1,(1. K),(0. K))),
(IFEQ (j,1,(0. K),(G2 * ((1 -' 1),(j -' 1))))))
by A90;
then A156:
B4 * (1,
j) =
IFEQ (
j,1,
(1. K),
(0. K))
by FUNCOP_1:def 8
.=
0. K
by A134, FUNCOP_1:def 8
;
let k2 be
Nat;
( k2 in dom <*(0. K)*> implies (Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2 )
assume
k2 in dom <*(0. K)*>
;
(Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2
then
k2 in Seg (len <*(0. K)*>)
by FINSEQ_1:def 3;
then
k2 in {1}
by FINSEQ_1:2, FINSEQ_1:40;
then A157:
k2 = 1
by TARSKI:def 1;
1
<= k + 1
by NAT_1:11;
then
k2 in Seg (len B4)
by A121, A157, FINSEQ_1:1;
then
k2 in dom B4
by FINSEQ_1:def 3;
then
(Col (B4,j)) . k2 = 0. K
by A157, A156, MATRIX_0:def 8;
hence
(Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2
by A152, A157, FINSEQ_1:40;
verum
end; A158:
len (Col (G2,(j -' 1))) =
len G2
by MATRIX_0:def 8
.=
k
by MATRIX_0:24
;
A159:
for
k2 being
Nat st
k2 in dom (Col (G2,(j -' 1))) holds
(Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2
proof
let k2 be
Nat;
( k2 in dom (Col (G2,(j -' 1))) implies (Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2 )
assume A160:
k2 in dom (Col (G2,(j -' 1)))
;
(Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2
then
1
<= k2
by FINSEQ_3:25;
then A161:
1
< k2 + 1
by NAT_1:13;
k2 in Seg k
by A158, A160, FINSEQ_1:def 3;
then A162:
k2 in dom G2
by A89, FINSEQ_1:def 3;
k2 <= k
by A158, A160, FINSEQ_3:25;
then A163:
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by NAT_1:11, XREAL_1:7;
then
[(k2 + 1),j] in Indices B4
by A120, A123, MATRIX_0:31;
then
B4 * (
(k2 + 1),
j)
= IFEQ (
(k2 + 1),1,
(IFEQ (j,1,(1. K),(0. K))),
(IFEQ (j,1,(0. K),(G2 * (((k2 + 1) -' 1),(j -' 1))))))
by A90;
then B4 * (
(k2 + 1),
j) =
IFEQ (
j,1,
(0. K),
(G2 * (((k2 + 1) -' 1),(j -' 1))))
by A161, FUNCOP_1:def 8
.=
G2 * (
((k2 + 1) -' 1),
(j -' 1))
by A134, FUNCOP_1:def 8
.=
G2 * (
k2,
(j -' 1))
by NAT_D:34
;
then A164:
B4 * (
(k2 + 1),
((j -' 1) + 1))
= (Col (G2,(j -' 1))) . k2
by A152, A162, MATRIX_0:def 8;
k2 + 1
in dom B4
by A121, A163, FINSEQ_3:25;
then
(Col (B4,((j -' 1) + 1))) . (k2 + 1) = (Col (G2,(j -' 1))) . k2
by A164, MATRIX_0:def 8;
hence
(Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2
by FINSEQ_1:40;
verum
end; dom (Col (B4,((j -' 1) + 1))) =
Seg (len (Col (B4,((j -' 1) + 1))))
by FINSEQ_1:def 3
.=
Seg ((len <*(0. K)*>) + (len (Col (G2,(j -' 1)))))
by A112, A152, A158, FINSEQ_1:39
;
then A165:
<*(0. K)*> ^ (Col (G2,(j -' 1))) = Col (
B4,
((j -' 1) + 1))
by A155, A159, FINSEQ_1:def 7;
(i -' 1) + 1 =
(i - 1) + 1
by A129, XREAL_1:233
.=
i
;
then A166:
(((B * A2) * C) * B4) * (
i,
j) =
|((Line (((B * A2) * C),((i -' 1) + 1))),(Col (B4,((j -' 1) + 1))))|
by A113, A121, A122, A151, MATRIX_3:def 4
.=
|(<*(0. K)*>,<*(0. K)*>)| + |((Line (F,(i -' 1))),(Col (G2,(j -' 1))))|
by A23, A109, A110, A150, A165, Th12
.=
(0. K) + |((Line (F,(i -' 1))),(Col (G2,(j -' 1))))|
by Th22
.=
(0. K) + ((F * G2) * ((i -' 1),(j -' 1)))
by A105, A89, A154, MATRIX_3:def 4
.=
(1. (K,k)) * (
(i -' 1),
(j -' 1))
by A88, RLVECT_1:4
;
A167:
[(i -' 1),(j -' 1)] in Indices (1. (K,k))
by A153, MATRIX_0:24;
now (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)per cases
( i = j or i <> j )
;
suppose A169:
i <> j
;
(((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)then
i - 1
<> j - 1
;
then
i0 -' 1
<> j0 -' 1
by A129, A152, XREAL_1:233;
then
(1. (K,k)) * (
(i0 -' 1),
(j0 -' 1))
= 0. K
by A167, MATRIX_1:def 3;
hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
by A115, A166, A169, MATRIX_1:def 3;
verum end; end; end; hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
;
verum end; end; end; hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
;
verum end; end; end;
hence
(((B * A2) * C) * B4) * (
i,
j)
= (1. (K,(k + 1))) * (
i,
j)
;
verum
end;
then
(
width (Inv B) = k + 1 &
((B * A2) * C) * B4 = 1. (
K,
(k + 1)) )
by MATRIX_0:24, MATRIX_0:27;
then
(Inv B) * (((B * A2) * C) * B4) = Inv B
by MATRIXR2:67;
then
((Inv B) * (((B * A2) * C) * B4)) * B = 1. (
K,
(k + 1))
by A8, Th18;
then
((Inv B) * ((B * A2) * (C * B4))) * B = 1. (
K,
(k + 1))
by Th17;
then
((Inv B) * (B * (A2 * (C * B4)))) * B = 1. (
K,
(k + 1))
by Th17;
then
(((Inv B) * B) * (A2 * (C * B4))) * B = 1. (
K,
(k + 1))
by Th17;
then
(
len (A2 * (C * B4)) = k + 1 &
((1. (K,(k + 1))) * (A2 * (C * B4))) * B = 1. (
K,
(k + 1)) )
by A8, Th18, MATRIX_0:24;
then
(A2 * (C * B4)) * B = 1. (
K,
(k + 1))
by MATRIXR2:68;
then
A2 * ((C * B4) * B) = 1. (
K,
(k + 1))
by Th17;
hence
ex
B4 being
Matrix of
k + 1,
K st
A2 * B4 = 1. (
K,
(k + 1))
;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for
D,
B0 being
Matrix of
0 ,
K st
B0 * D = 1. (
K,
0) holds
ex
B1 being
Matrix of
0 ,
K st
D * B1 = 1. (
K,
0)
proof
let D,
B0 be
Matrix of
0 ,
K;
( B0 * D = 1. (K,0) implies ex B1 being Matrix of 0 ,K st D * B1 = 1. (K,0) )
assume
B0 * D = 1. (
K,
0)
;
ex B1 being Matrix of 0 ,K st D * B1 = 1. (K,0)
D * (0. (K,0)) = 1. (
K,
0)
by Th15;
hence
ex
B1 being
Matrix of
0 ,
K st
D * B1 = 1. (
K,
0)
;
verum
end;
then A170:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A170, A2);
hence
ex
B2 being
Matrix of
n,
K st
A * B2 = 1. (
K,
n)
by A1;
verum
end;