let K be Field; for b being Element of K
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let b be Element of K; for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let M1, M2 be Matrix of K; ( len M1 = len M2 & width M1 = width M2 implies b * (M1 + M2) = (b * M1) + (b * M2) )
A1:
( len (b * (M1 + M2)) = len (M1 + M2) & width (b * (M1 + M2)) = width (M1 + M2) )
by MATRIX_3:def 5;
A2:
( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 )
by MATRIX_3:def 3;
A3:
( len (b * M1) = len M1 & width (b * M1) = width M1 )
by MATRIX_3:def 5;
assume A4:
( len M1 = len M2 & width M1 = width M2 )
; b * (M1 + M2) = (b * M1) + (b * M2)
A5:
for i, j being Nat st [i,j] in Indices (b * (M1 + M2)) holds
(b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices (b * (M1 + M2)) implies (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) )
assume A6:
[i,j] in Indices (b * (M1 + M2))
;
(b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)
A7:
Indices M2 = Indices M1
by A4, MATRIX_4:55;
A8:
Indices (b * (M1 + M2)) = Indices (M1 + M2)
by A1, MATRIX_4:55;
A9:
Indices (M1 + M2) = Indices M1
by A2, MATRIX_4:55;
Indices (b * M1) = Indices M1
by A3, MATRIX_4:55;
then ((b * M1) + (b * M2)) * (
i,
j) =
((b * M1) * (i,j)) + ((b * M2) * (i,j))
by A6, A8, A9, MATRIX_3:def 3
.=
(b * (M1 * (i,j))) + ((b * M2) * (i,j))
by A6, A8, A9, MATRIX_3:def 5
.=
(b * (M1 * (i,j))) + (b * (M2 * (i,j)))
by A6, A8, A9, A7, MATRIX_3:def 5
.=
b * ((M1 * (i,j)) + (M2 * (i,j)))
by VECTSP_1:def 7
;
then ((b * M1) + (b * M2)) * (
i,
j) =
b * ((M1 + M2) * (i,j))
by A6, A8, A9, MATRIX_3:def 3
.=
(b * (M1 + M2)) * (
i,
j)
by A6, A8, MATRIX_3:def 5
;
hence
(b * (M1 + M2)) * (
i,
j)
= ((b * M1) + (b * M2)) * (
i,
j)
;
verum
end;
( len ((b * M1) + (b * M2)) = len (b * M1) & width ((b * M1) + (b * M2)) = width (b * M1) )
by MATRIX_3:def 3;
hence
b * (M1 + M2) = (b * M1) + (b * M2)
by A1, A2, A3, A5, MATRIX_0:21; verum