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