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