let K be Field; for A being Matrix of K holds (1. (K,(len A))) * A = A
let A be Matrix of K; (1. (K,(len A))) * A = A
set n = len A;
set B = 1. (K,(len A));
A1:
len (1. (K,(len A))) = len A
by MATRIX_0:24;
A2:
width (1. (K,(len A))) = len A
by MATRIX_0:24;
then A3:
len ((1. (K,(len A))) * A) = len (1. (K,(len A)))
by MATRIX_3:def 4;
A4:
now for i, j being Nat st [i,j] in Indices ((1. (K,(len A))) * A) holds
((1. (K,(len A))) * A) * (i,j) = A * (i,j)A5:
dom A = Seg (len A)
by FINSEQ_1:def 3;
let i,
j be
Nat;
( [i,j] in Indices ((1. (K,(len A))) * A) implies ((1. (K,(len A))) * A) * (i,j) = A * (i,j) )assume A6:
[i,j] in Indices ((1. (K,(len A))) * A)
;
((1. (K,(len A))) * A) * (i,j) = A * (i,j)A7:
dom ((1. (K,(len A))) * A) = Seg (len ((1. (K,(len A))) * A))
by FINSEQ_1:def 3;
then A8:
i in Seg (width (1. (K,(len A))))
by A1, A2, A3, A6, ZFMISC_1:87;
then
i in Seg (len (Line ((1. (K,(len A))),i)))
by MATRIX_0:def 7;
then A9:
i in dom (Line ((1. (K,(len A))),i))
by FINSEQ_1:def 3;
A10:
dom (1. (K,(len A))) = Seg (len (1. (K,(len A))))
by FINSEQ_1:def 3;
then A11:
i in dom (1. (K,(len A)))
by A3, A6, A7, ZFMISC_1:87;
then
[i,i] in Indices (1. (K,(len A)))
by A8, ZFMISC_1:87;
then A12:
(Line ((1. (K,(len A))),i)) . i = 1_ K
by MATRIX_3:15;
i in Seg (len (Col (A,j)))
by A2, A8, MATRIX_0:def 8;
then A13:
i in dom (Col (A,j))
by FINSEQ_1:def 3;
A14:
now for k being Nat st k in dom (Line ((1. (K,(len A))),i)) & k <> i holds
(Line ((1. (K,(len A))),i)) . k = 0. Klet k be
Nat;
( k in dom (Line ((1. (K,(len A))),i)) & k <> i implies (Line ((1. (K,(len A))),i)) . k = 0. K )assume that A15:
k in dom (Line ((1. (K,(len A))),i))
and A16:
k <> i
;
(Line ((1. (K,(len A))),i)) . k = 0. K
k in Seg (len (Line ((1. (K,(len A))),i)))
by A15, FINSEQ_1:def 3;
then
k in Seg (width (1. (K,(len A))))
by MATRIX_0:def 7;
then
[i,k] in Indices (1. (K,(len A)))
by A11, ZFMISC_1:87;
hence
(Line ((1. (K,(len A))),i)) . k = 0. K
by A16, MATRIX_3:15;
verum end; thus ((1. (K,(len A))) * A) * (
i,
j) =
(Line ((1. (K,(len A))),i)) "*" (Col (A,j))
by A2, A6, MATRIX_3:def 4
.=
Sum (mlt ((Line ((1. (K,(len A))),i)),(Col (A,j))))
by FVSUM_1:def 9
.=
(Col (A,j)) . i
by A9, A13, A14, A12, MATRIX_3:17
.=
A * (
i,
j)
by A1, A5, A10, A11, MATRIX_0:def 8
;
verum end;
width ((1. (K,(len A))) * A) = width A
by A2, MATRIX_3:def 4;
hence
(1. (K,(len A))) * A = A
by A1, A3, A4, MATRIX_0:21; verum