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

A2: width (1. (L,m)) = m by A1, MATRIX_0:23

.= len M by A1, MATRIX_0:23 ;

set M2 = (1. (L,m)) * M;

A3: len M = m by A1, MATRIX_0:23;

len (1. (L,m)) = m by A1, MATRIX_0:23;

then A4: m = len ((1. (L,m)) * M) by A2, MATRIX_3:def 4;

hence (1. (L,m)) * M = M by A3, A4, A5, MATRIX_0:21; :: thesis: verum

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

A2: width (1. (L,m)) = m by A1, MATRIX_0:23

.= len M by A1, MATRIX_0:23 ;

set M2 = (1. (L,m)) * M;

A3: len M = m by A1, MATRIX_0:23;

len (1. (L,m)) = m by A1, MATRIX_0:23;

then A4: m = len ((1. (L,m)) * M) by A2, MATRIX_3:def 4;

A5: now :: thesis: for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = ((1. (L,m)) * M) * (i,j)

width M = width ((1. (L,m)) * M)
by A2, MATRIX_3:def 4;M * (i,j) = ((1. (L,m)) * M) * (i,j)

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)

then A7: i in dom M by ZFMISC_1:87;

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 A8: ((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 9 ;

len (Line ((1. (L,m)),i)) = width (1. (L,m)) by MATRIX_0:def 7

.= m by MATRIX_0:24 ;

then A9: dom (Line ((1. (L,m)),i)) = Seg m by FINSEQ_1:def 3;

A10: len M = m by A1, MATRIX_0:23;

then A11: i in dom (Line ((1. (L,m)),i)) by A7, A9, FINSEQ_1:def 3;

A12: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by A1, MATRIX_0:23;

then A13: [i,i] in Indices (1. (L,m)) by A9, A11, ZFMISC_1:87;

A14: for k being Nat st k in dom (Line ((1. (L,m)),i)) & k <> i holds

(Line ((1. (L,m)),i)) . k = 0. L

.= m by A1, MATRIX_0:23 ;

then dom (Col (M,j)) = Seg m by FINSEQ_1:def 3;

then A18: i in dom (Col (M,j)) by A7, A10, FINSEQ_1:def 3;

i in Seg (width (1. (L,m))) by A9, A11, MATRIX_0:24;

then A19: (Line ((1. (L,m)),i)) . i = (1. (L,m)) * (i,i) by MATRIX_0:def 7

.= 1. L by A13, MATRIX_1:def 3 ;

i in dom (Line ((1. (L,m)),i)) by A7, A10, A9, FINSEQ_1:def 3;

then Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) = (Col (M,j)) . i by A19, A14, A18, MATRIX_3:17;

hence M * (i,j) = ((1. (L,m)) * M) * (i,j) by A8, A7, MATRIX_0:def 8; :: thesis: verum

end;assume A6: [i,j] in Indices M ; :: thesis: M * (i,j) = ((1. (L,m)) * M) * (i,j)

then A7: i in dom M by ZFMISC_1:87;

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 A8: ((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 9 ;

len (Line ((1. (L,m)),i)) = width (1. (L,m)) by MATRIX_0:def 7

.= m by MATRIX_0:24 ;

then A9: dom (Line ((1. (L,m)),i)) = Seg m by FINSEQ_1:def 3;

A10: len M = m by A1, MATRIX_0:23;

then A11: i in dom (Line ((1. (L,m)),i)) by A7, A9, FINSEQ_1:def 3;

A12: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by A1, MATRIX_0:23;

then A13: [i,i] in Indices (1. (L,m)) by A9, A11, ZFMISC_1:87;

A14: 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

len (Col (M,j)) =
len M
by MATRIX_0:def 8
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 that

A15: k in dom (Line ((1. (L,m)),i)) and

A16: k <> i ; :: thesis: (Line ((1. (L,m)),i)) . k = 0. L

A17: [i,k] in Indices (1. (L,m)) by A9, A11, A12, A15, ZFMISC_1:87;

k in Seg (width (1. (L,m))) by A9, A15, MATRIX_0:24;

then (Line ((1. (L,m)),i)) . k = (1. (L,m)) * (i,k) by MATRIX_0:def 7

.= 0. L by A16, A17, MATRIX_1:def 3 ;

hence (Line ((1. (L,m)),i)) . k = 0. L ; :: thesis: verum

end;assume that

A15: k in dom (Line ((1. (L,m)),i)) and

A16: k <> i ; :: thesis: (Line ((1. (L,m)),i)) . k = 0. L

A17: [i,k] in Indices (1. (L,m)) by A9, A11, A12, A15, ZFMISC_1:87;

k in Seg (width (1. (L,m))) by A9, A15, MATRIX_0:24;

then (Line ((1. (L,m)),i)) . k = (1. (L,m)) * (i,k) by MATRIX_0:def 7

.= 0. L by A16, A17, MATRIX_1:def 3 ;

hence (Line ((1. (L,m)),i)) . k = 0. L ; :: thesis: verum

.= m by A1, MATRIX_0:23 ;

then dom (Col (M,j)) = Seg m by FINSEQ_1:def 3;

then A18: i in dom (Col (M,j)) by A7, A10, FINSEQ_1:def 3;

i in Seg (width (1. (L,m))) by A9, A11, MATRIX_0:24;

then A19: (Line ((1. (L,m)),i)) . i = (1. (L,m)) * (i,i) by MATRIX_0:def 7

.= 1. L by A13, MATRIX_1:def 3 ;

i in dom (Line ((1. (L,m)),i)) by A7, A10, A9, FINSEQ_1:def 3;

then Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) = (Col (M,j)) . i by A19, A14, A18, MATRIX_3:17;

hence M * (i,j) = ((1. (L,m)) * M) * (i,j) by A8, A7, MATRIX_0:def 8; :: thesis: verum

hence (1. (L,m)) * M = M by A3, A4, A5, MATRIX_0:21; :: thesis: verum