let L be Field; :: thesis: for m, n being Nat st m > 0 holds
for M being Matrix of m,n,L holds (1. L,m) * M = M
let m, n be Nat; :: thesis: ( m > 0 implies for M being Matrix of m,n,L holds (1. L,m) * M = M )
assume A1:
m > 0
; :: thesis: for M being Matrix of m,n,L holds (1. L,m) * M = M
let M be Matrix of m,n,L; :: thesis: (1. L,m) * M = M
set M2 = (1. L,m) * M;
A2: width (1. L,m) =
m
by A1, MATRIX_1:24
.=
len M
by A1, MATRIX_1:24
;
A3:
len M = m
by A1, MATRIX_1:24;
len (1. L,m) = m
by A1, MATRIX_1:24;
then A4:
m = len ((1. L,m) * M)
by A2, MATRIX_3:def 4;
A5:
width M = width ((1. L,m) * M)
by A2, MATRIX_3:def 4;
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices M implies M * i,j = ((1. L,m) * M) * i,j )assume A6:
[i,j] in Indices M
;
:: thesis: M * i,j = ((1. L,m) * M) * i,j dom M =
Seg (len M)
by FINSEQ_1:def 3
.=
dom ((1. L,m) * M)
by A3, A4, FINSEQ_1:def 3
;
then
Indices M = Indices ((1. L,m) * M)
by A2, MATRIX_3:def 4;
then A7:
((1. L,m) * M) * i,
j =
(Line (1. L,m),i) "*" (Col M,j)
by A2, A6, MATRIX_3:def 4
.=
Sum (mlt (Line (1. L,m),i),(Col M,j))
by FVSUM_1:def 10
;
A8:
i in dom M
by A6, ZFMISC_1:106;
Sum (mlt (Line (1. L,m),i),(Col M,j)) = M * i,
j
proof
Sum (mlt (Line (1. L,m),i),(Col M,j)) = (Col M,j) . i
proof
(
i in dom (Line (1. L,m),i) &
i in dom (Col M,j) &
(Line (1. L,m),i) . i = 1. L & ( for
k being
Nat st
k in dom (Line (1. L,m),i) &
k <> i holds
(Line (1. L,m),i) . k = 0. L ) )
proof
A9:
len M = m
by A1, MATRIX_1:24;
len (Line (1. L,m),i) =
width (1. L,m)
by MATRIX_1:def 8
.=
m
by MATRIX_1:25
;
then A10:
dom (Line (1. L,m),i) = Seg m
by FINSEQ_1:def 3;
then A11:
i in dom (Line (1. L,m),i)
by A8, A9, FINSEQ_1:def 3;
len (Col M,j) =
len M
by MATRIX_1:def 9
.=
m
by A1, MATRIX_1:24
;
then A12:
dom (Col M,j) = Seg m
by FINSEQ_1:def 3;
A13:
i in Seg (width (1. L,m))
by A10, A11, MATRIX_1:25;
A14:
Indices (1. L,m) = [:(Seg m),(Seg m):]
by A1, MATRIX_1:24;
then A15:
[i,i] in Indices (1. L,m)
by A10, A11, ZFMISC_1:106;
A16:
(Line (1. L,m),i) . i =
(1. L,m) * i,
i
by A13, MATRIX_1:def 8
.=
1. L
by A15, MATRIX_1:def 12
;
for
k being
Nat st
k in dom (Line (1. L,m),i) &
k <> i holds
(Line (1. L,m),i) . k = 0. L
proof
let k be
Nat;
:: thesis: ( k in dom (Line (1. L,m),i) & k <> i implies (Line (1. L,m),i) . k = 0. L )
assume A17:
(
k in dom (Line (1. L,m),i) &
k <> i )
;
:: thesis: (Line (1. L,m),i) . k = 0. L
then A18:
k in Seg (width (1. L,m))
by A10, MATRIX_1:25;
A19:
[i,k] in Indices (1. L,m)
by A10, A11, A14, A17, ZFMISC_1:106;
(Line (1. L,m),i) . k =
(1. L,m) * i,
k
by A18, MATRIX_1:def 8
.=
0. L
by A17, A19, MATRIX_1:def 12
;
hence
(Line (1. L,m),i) . k = 0. L
;
:: thesis: verum
end;
hence
(
i in dom (Line (1. L,m),i) &
i in dom (Col M,j) &
(Line (1. L,m),i) . i = 1. L & ( for
k being
Nat st
k in dom (Line (1. L,m),i) &
k <> i holds
(Line (1. L,m),i) . k = 0. L ) )
by A8, A9, A10, A12, A16, FINSEQ_1:def 3;
:: thesis: verum
end;
hence
Sum (mlt (Line (1. L,m),i),(Col M,j)) = (Col M,j) . i
by MATRIX_3:19;
:: thesis: verum
end;
hence
Sum (mlt (Line (1. L,m),i),(Col M,j)) = M * i,
j
by A8, MATRIX_1:def 9;
:: thesis: verum
end; hence
M * i,
j = ((1. L,m) * M) * i,
j
by A7;
:: thesis: verum end;
hence
(1. L,m) * M = M
by A3, A4, A5, MATRIX_1:21; :: thesis: verum