let K be Field; :: thesis: for A being Matrix of K holds A * (1. K,(width A)) = A
let A be Matrix of K; :: thesis: A * (1. K,(width A)) = A
set n = width A;
set B = 1. K,(width A);
A1:
( len (1. K,(width A)) = width A & width (1. K,(width A)) = width A & width A = width A )
by MATRIX_1:25;
then A2:
( len (A * (1. K,(width A))) = len A & width (A * (1. K,(width A))) = width (1. K,(width A)) )
by MATRIX_3:def 4;
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices (A * (1. K,(width A))) implies (A * (1. K,(width A))) * i,j = A * i,j )assume A3:
[i,j] in Indices (A * (1. K,(width A)))
;
:: thesis: (A * (1. K,(width A))) * i,j = A * i,jthen A4:
(
j in Seg (width (1. K,(width A))) &
j in Seg (width A) )
by A1, A2, ZFMISC_1:106;
then
(
j in dom (1. K,(width A)) &
j in Seg (width A) )
by A1, FINSEQ_1:def 3;
then A5:
[j,j] in Indices (1. K,(width A))
by A1, ZFMISC_1:106;
(
j in Seg (len (Col (1. K,(width A)),j)) &
j in Seg (len (Line A,i)) )
by A1, A4, MATRIX_1:def 8, MATRIX_1:def 9;
then A6:
(
j in dom (Col (1. K,(width A)),j) &
j in dom (Line A,i) )
by FINSEQ_1:def 3;
A7:
(
(Col (1. K,(width A)),j) . j = 1_ K & ( for
k being
Nat st
k in dom (Col (1. K,(width A)),j) &
k <> j holds
(Col (1. K,(width A)),j) . k = 0. K ) )
proof
thus
(Col (1. K,(width A)),j) . j = 1_ K
by A5, MATRIX_3:18;
:: thesis: for k being Nat st k in dom (Col (1. K,(width A)),j) & k <> j holds
(Col (1. K,(width A)),j) . k = 0. K
now let k be
Nat;
:: thesis: ( k in dom (Col (1. K,(width A)),j) & k <> j implies (Col (1. K,(width A)),j) . k = 0. K )assume A8:
(
k in dom (Col (1. K,(width A)),j) &
k <> j )
;
:: thesis: (Col (1. K,(width A)),j) . k = 0. Kthen
k in Seg (len (Col (1. K,(width A)),j))
by FINSEQ_1:def 3;
then
k in Seg (len (1. K,(width A)))
by MATRIX_1:def 9;
then
k in dom (1. K,(width A))
by FINSEQ_1:def 3;
then
[k,j] in Indices (1. K,(width A))
by A4, ZFMISC_1:106;
hence
(Col (1. K,(width A)),j) . k = 0. K
by A8, MATRIX_3:18;
:: thesis: verum end;
hence
for
k being
Nat st
k in dom (Col (1. K,(width A)),j) &
k <> j holds
(Col (1. K,(width A)),j) . k = 0. K
;
:: thesis: verum
end; thus (A * (1. K,(width A))) * i,
j =
(Line A,i) "*" (Col (1. K,(width A)),j)
by A1, A3, MATRIX_3:def 4
.=
(Col (1. K,(width A)),j) "*" (Line A,i)
by FVSUM_1:115
.=
Sum (mlt (Col (1. K,(width A)),j),(Line A,i))
by FVSUM_1:def 10
.=
(Line A,i) . j
by A6, A7, MATRIX_3:19
.=
A * i,
j
by A4, MATRIX_1:def 8
;
:: thesis: verum end;
hence
A * (1. K,(width A)) = A
by A1, A2, MATRIX_1:21; :: thesis: verum