let K be Ring; for A, B, C being Matrix of K st len A = len B & width A = width B holds
(A + B) + C = A + (B + C)
let A, B, C be Matrix of K; ( len A = len B & width A = width B implies (A + B) + C = A + (B + C) )
assume that
A1:
len A = len B
and
A2:
width A = width B
; (A + B) + C = A + (B + C)
dom A = dom B
by A1, FINSEQ_3:29;
then A3:
Indices B = [:(dom A),(Seg (width A)):]
by A2;
A4:
Indices A = [:(dom A),(Seg (width A)):]
;
A5:
width ((A + B) + C) = width (A + B)
by Def3;
A6:
width (A + B) = width A
by Def3;
A7:
( len (A + (B + C)) = len A & width (A + (B + C)) = width A )
by Def3;
A8:
len (A + B) = len A
by Def3;
A9:
len ((A + B) + C) = len (A + B)
by Def3;
then
dom A = dom ((A + B) + C)
by A8, FINSEQ_3:29;
then A10:
Indices ((A + B) + C) = [:(dom A),(Seg (width A)):]
by A6, A5;
dom A = dom (A + B)
by A8, FINSEQ_3:29;
then A11:
Indices (A + B) = [:(dom A),(Seg (width A)):]
by A6;
now for i, j being Nat st [i,j] in Indices ((A + B) + C) holds
((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((A + B) + C) implies ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j) )assume A12:
[i,j] in Indices ((A + B) + C)
;
((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)hence ((A + B) + C) * (
i,
j) =
((A + B) * (i,j)) + (C * (i,j))
by A11, A10, Def3
.=
((A * (i,j)) + (B * (i,j))) + (C * (i,j))
by A4, A10, A12, Def3
.=
(A * (i,j)) + ((B * (i,j)) + (C * (i,j)))
by RLVECT_1:def 3
.=
(A * (i,j)) + ((B + C) * (i,j))
by A3, A10, A12, Def3
.=
(A + (B + C)) * (
i,
j)
by A4, A10, A12, Def3
;
verum end;
hence
(A + B) + C = A + (B + C)
by A8, A6, A9, A5, A7, MATRIX_0:21; verum