let i be Nat; for K being Field
for A, B, X being Matrix of K st X in Solutions_of (A,B) & i in dom A & Line (A,i) = (width A) |-> (0. K) holds
Line (B,i) = (width B) |-> (0. K)
let K be Field; for A, B, X being Matrix of K st X in Solutions_of (A,B) & i in dom A & Line (A,i) = (width A) |-> (0. K) holds
Line (B,i) = (width B) |-> (0. K)
let A, B, X be Matrix of K; ( X in Solutions_of (A,B) & i in dom A & Line (A,i) = (width A) |-> (0. K) implies Line (B,i) = (width B) |-> (0. K) )
assume that
A1:
X in Solutions_of (A,B)
and
A2:
i in dom A
and
A3:
Line (A,i) = (width A) |-> (0. K)
; Line (B,i) = (width B) |-> (0. K)
set wB0 = (width B) |-> (0. K);
set LB = Line (B,i);
A4:
len (Line (B,i)) = width B
by CARD_1:def 7;
A5:
ex X1 being Matrix of K st
( X = X1 & len X1 = width A & width X1 = width B & A * X1 = B )
by A1;
A6:
now for k being Nat st 1 <= k & k <= len (Line (B,i)) holds
((width B) |-> (0. K)) . k = (Line (B,i)) . klet k be
Nat;
( 1 <= k & k <= len (Line (B,i)) implies ((width B) |-> (0. K)) . k = (Line (B,i)) . k )assume A7:
( 1
<= k &
k <= len (Line (B,i)) )
;
((width B) |-> (0. K)) . k = (Line (B,i)) . kA8:
k in Seg (width B)
by A4, A7;
len A = len B
by A1, Th33;
then
dom A = Seg (len B)
by FINSEQ_1:def 3;
then
i in dom B
by A2, FINSEQ_1:def 3;
then
[i,k] in Indices B
by A8, ZFMISC_1:87;
then B * (
i,
k) =
(Line (A,i)) "*" (Col (X,k))
by A5, MATRIX_3:def 4
.=
Sum ((0. K) * (Col (X,k)))
by A3, A5, FVSUM_1:66
.=
(0. K) * (Sum (Col (X,k)))
by FVSUM_1:73
.=
0. K
.=
((width B) |-> (0. K)) . k
by A8, FINSEQ_2:57
;
hence
((width B) |-> (0. K)) . k = (Line (B,i)) . k
by A8, MATRIX_0:def 7;
verum end;
len ((width B) |-> (0. K)) = width B
by CARD_1:def 7;
hence
Line (B,i) = (width B) |-> (0. K)
by A4, A6; verum